Interactive Robot Transition Repair With SMT

1 Introduction

Complex robot control software is typically structured as a state machine, where each state encapsulates a feedback controller. Even if each state is correct, the transitions between states depend on parameters that are hard to get right, even for experienced roboticists. It is very common for parameter values to work in simulation but fail in the real world, to work in one physical environment but fail in another, or to work on one robot but fail on another. For example, Figure 1 shows the trajectory of a robotic soccer player as it tries to kick a moving ball. A very small change to its parameter values determines whether or not it succeeds.

Even a simple robot may have a large parameter space, which makes exhaustive-search impractical. Moreover, robot performance is usually non-convex with respect to parameter values, which makes general optimization techniques susceptible to local minima. For some cases, there exist calibration procedures to adjust parameters automatically (e.g., [Holtz and Biswas, 2017]), but these are not general procedures.

Therefore, roboticists usually resort to adjusting parameters manually-a tedious task that can result in poor performance.

However, consider the following observations: a roboticist debugging a robot can frequently identify when something goes wrong, and what the robot should have done instead. When the robot control software is structured as a state machine, this corresponds to identifying when the robot is in the wrong state and what the correct state should be. This is a partial specification of expected behavior: i.e., it does not enumerate a complete sequence of states, the parameters to adjust, how to adjust them, or even identify all errors. In this paper, we show that partial specification of this kind are adequate inputs for an automatic parameter repair procedure.

We present Interactive SMT-based Robot Transition Repair (SRTR). During execution, SRTR logs the execution trace of the transition function. After execution, the roboticist examines the trace and provides a handful of corrections. SRTR then converts the set of corrections and the transition function into a logical formula for a MaxSMT solver. A solution to this MaxSMT problem minimizes adjustments to the parameters, while maximizing the number of satisfied corrections.

Our experimental results demonstrate that SRTR 1) is more computationally tractable than exhaustive parameter search; 2) is scalable; 3) generalizes to unseen situations; and 4) when applied to simple robot soccer attacker, can outperform a more complicated, expert-tuned attacker that won the lower bracket finals at RoboCup 2017.

2 RelatedWork

Finite state machines (FSMs) can specify robot behavior and enable robust autonomy. RoboChart [Miyazawa et al., 2017] uses FSMs to verify liveness, timeliness, and other properties of robots. The HAMQ-INT algorithm [Bai and Russell, 2017] uses reinforcement learning to discover internal transitions and adapt to unexpected scenarios. SRTR also leverages FSMs, but focuses on correcting transition errors that occur when the robot is deployed in a new environment.

Robot behavior can also be repaired by dynamic synthesis of new control structures, such as automatic synthesis of new FSMs [Wong et al., 2014], or synthesis of code from a context-free motion grammar with parameters derived from human-inspired control [Dantam et al., 2013]. When automated synthesis is intractable, a user-generated specification in a domain-specific language can be used to synthesize a plan [Nedunuri et al., 2014]. SRTR assumes that the FSM does not need new states or transitions, but that failures are due to incorrect triggering of the transition function arising from incorrect environment-dependent parameter values.

Robot behaviors rely on environment-dependent parameters for robust and accurate execution. If a precise model of the dependency between parameters and behaviors is available, it may be possible to design a calibration procedure that executes a specific sequence of actions and to recover correct parameter values (e.g.,[Holtz and Biswas, 2017]). If a calibration procedure cannot be designed, but the effect of parameters is well-understood, it may be possible to optimize for the parameters using a functional model [Cano et al., 2016]. Model-based diagnosis can diagnose faulty parameters [Reiter, 1987] if the behavior of the robot in its environment can be formally defined. SRTR can repair parameters even without a descriptive model of the robot's behavior.

Human input can help overcome the limitations of autonomous algorithms [Kamar, 2016; Nashed and Biswas, 2018]. Learning from demonstration (LfD) [Argall et al., 2009] and inverse reinforcement learning (IRL) [Abbeel and Ng, 2011] allow robots to learn new behaviors from human demonstrations. LfD can also overcome model errors by correcting portions of the state space [Meric¸li et al., 2012]. These approaches require demonstrations in the full highdimensional state space of the robot, which can be tedious for users to provide. When human demonstration does not specify why an action was applied to a state, it can be hard to generalize to a new situation. SRTR generalizes to new scenarios since it infers dependencies from the code of the transition function. Furthermore, it requires only a partial specification of correct behavior.

Domain-specific languages (DSLs) allow users to specify high-level behavior using abstractions such as Instruction Graphs [Mericli et al., 2014]. Unlike DSLs that provide a complete specification of robot behavior, SRTR only requires sparse corrections that partially-specify expected behavior.

DirectFix [Mechtaev et al., 2015] formulates program repair as a MaxSMT problem and deems a program fixed when all tests pass. Physical robots don't have deterministic test cases and user-provided corrections can be contradictory. SRTR uses MaxSMT to minimize changes and maximize the number of satisfied corrections. There are other domains that are not amenable to unit-testing. For example, Tortoise [Weiss et al., 2017] propagates system configuration fixes from the shell to a system configuration specification. However, Tortoise requires a complete fix where SRTR only requires a partial specification.

Programming by example synthesizes programs from a small number of examples [Gulwani, 2011] and can also support noisy data [Devlin et al., 2017] Program templates can help synthesize task and motion plans [Nedunuri et al., 2014]. SRTR does not synthesize new program structure, but focuses on making minimal parameter adjustments using MaxSMT to satisfy user corrections.

3 Background

We use a real-world example to motivate SRTR: a robot soccer attacker that 1) goes to the ball if the ball is stopped, 2) intercepts the ball if it is moving away from the attacker, 3) catches the ball if it is moving toward the attacker, and 4) kicks the ball at the goal once the attacker has control of the ball. Each of these sub-behaviors is a distinct, self-contained feedback controller (e.g., ball interception [Biswas et al., 2014] or omnidirectional time optimal control [Kalm´ar-Nagy et al., 2004]). At each time-step, the attacker 1) switches to a new controller if necessary and 2) invokes the current controller to produce new outputs. We represent the attacker as a robot state machine (RSM), where each state represents a controller (Figure 1a).

In this paper, we assume that the output of each controller is nominally correct: there may be minor performance degradation when environmental factors change, but we assume that they are convergent, and will eventually produce the correct result. However, environmental factors also affect the transition function, which transfers execution from one controller to another. For example, the friction coefficient between the ball and the carpet affects: when the attacker transitions from Intercept to Kick; and the mass of the ball affects when the attacker transitions from Kick to Done. These factors vary from one environment to another. Since transition functions do not have any self-correcting mechanisms, robots are prone to behaving incorrectly when their parameters are incorrect for the given environment.

3.1 Robot State Machines

A robot state machine (RSM) is a discrete-time Mealy machine that is extended with continuous inputs, outputs, and program variables. Formally, an RSM is a 9-tuple 〈S, S0, SF , V, V0, Y,U, T,G〉, where S is the finite set of states, S0 ∈ S is the start state, SF ∈ S is the end state, V ∈ Rm is the set of program variable values, V0 ∈ Rm are the initial values of the program variables, Y ∈ Rn are the continuous inputs, U ∈ Rl are the continuous actuation outputs, T : S × Y × V → S is the transition function, and G : S × Y × V → U × V is the emission function. At each time step t, the RSM first uses the transition function to select a state and then the emission function to run the controller associated with that state. The transition function can only update the current state, whereas the emission function can update program variables and produce outputs.

3.2 Transition Errors

Figure 1b shows two traces of the attacker. In the blue trace, the attacker correctly intercepts the moving ball and kicks it at the goal. But, in the red trace, the attacker fails to kick: it remains stuck in the Intercept state and never transitions to Kick. Over the course of several trials (e.g., a robot soccer game), we may find that the attacker only occasionally fails to kick. When this occurs, it is usually the case that the highlevel structure of the transition function is correct, but that the values of the parameters need to be adjusted. Unfortunately, since there are 11 real-valued parameters in the full attacker RSM, the search space is large.

To efficiently search for new parameter values, we need to reason about the structure of the transition function. To do so, the next section describes how we systematically convert it to a formula in propositional logic, extended with arithmetic operators. This formula encodes the structure of the transition function along with constraints from the user corrections, and allows an SMT solver to efficiently find new parameters to correct the errant transition(s).

4 Interactive Robot Transition Repair

The SRTR algorithm has four inputs: 1) the transition function, 2) a map from parameters to their values, 3) an execution trace, and 4) a set of user-provided corrections. The result of SRTR is a corrected parameter map that maximizes the number of corrections satisfied and minimizes the changes to the input parameter map. (The tradeoff between these objectives is a hyperparameter.)

SRTR has three major steps. 1) For each user-provided correction, it partially evaluates the transition function for the inputs and variable values at the time of correction, yielding residual transition functions (Section 4.2). 2) Finally, it uses the residual transition functions to formulate an optimization problem for an off-the-shelf MaxSMT solver, for this paper we use Z3 [Bjørner et al., 2015]. The solution to this problem is an adjustment to the parameter values (Section 4.3).

To illustrate the SRTR algorithm, we present as a running example a simplified attacker RSM that is only capable of handling a stationary ball on the field (Figure 2). Therefore, the RSM has four states (Start, GoTo, Kick, and End) and its transition function (Figure 3a) has four parameters (aimMarginp, maxDistp, viewAngp, and kickTimeoutp). From an execution trace of the RSM (Figure 3b), we consider an example where at time-step t = 5, the user identifies that the transition function produces an incorrect result: instead of GoTo, it should have returned Kick. With this example in mind, we present how SRTR uses the transition function code, an execution trace, and a correction to identify that an adjustment to just one of the parameters, maxDistp, is sufficient to satisfy this correction (Figure 3c).

4.1 Transition Functions and SRTR Inputs

To abstract away language-specific details of our repair procedure, we present SRTR for an idealized imperative language that only has features essential for writing transition functions. Figure 4 lists the syntax for a transition function written in SRTR-repairable form using a notation that is close to standard BNF. In general, the transition function consists of sequences of statements comprised of expressions over 1) the current state s, 2) program inputs xy, 3) parameters xp, and 4) program variables xv. Based on computations over these identifiers, the transition function returns the next state. Figure 4 has a list of operators that often appear in transition functions, such as arithmetic and trigonometric functions, but the list is not exhaustive. As a concrete example of a transition function written in repairable form, Figure 3a shows the transition function for the running example: it branches on the current state (s) and returns the next state. The crux of the transition function are the conditions that determine when the transition from GoTo to Kick occur.

A parameter map (P) specifies the parameters of a transition function. Figure 3b shows the parameter map of our example before running SRTR. The output of SRTR will be a set of adjustments to this parameter map.

An execution trace is a sequence of trace elements τt. A trace element records the values of sensor inputs, program variables, and the state at the start of time-step t. Finally, a user-provided correction (ct) specifies the expected state at the end of time-step t. In our example, the attacker should have transitioned to the Kick state after t = 5.

Figure 3b shows the trace element and a user correction for the running example: since the correction c5 refers only to the time-step t = 5, only the relevant trace element τ5 is shown.

4.2 Residual Transition Functions

The goal of SRTR is to adjust the parameters such that for each correction (ct) the transition function produces the corrected next-state instead of the actual state recorded at time t + 1. SRTR first simplifies the problem by specializing the transition function using the state, variables, and inputs recorded at time t. We call this simplified function the residual transition function. Figure 3c shows the residual transition function for the correction at t = 5. Since the state at this time-step (τ5.state) is GoTo, the residual transition function only has the code from the branch that handles this case (i.e., the code from lines 3-13). Furthermore, we substitute the input and variable identifiers with concrete values from the trace element and simplify expressions as much as possible. Therefore, the only identifiers that remain are parameters. This approach is known as partial evaluation [Jones et al., 1993]. At a later step, SRTR translates this residual transition function into a formula for an SMT solver.

A potential problem with this approach is that SMT solvers do not have decision procedures that support trigonometric functions, which occur frequently in RSMs. Our example also uses trigonometric functions in several expressions. Fortunately, most of these trigonometric functions are applied to inputs and variables, thus they are substituted with concrete values in the residual. For example, line 6 calculates sin(robotAngy ) and cos(robotAngy ), but robotAngy is an input. Thus, the residual substitutes the identifier with its value Trace Elements

Figure 4: Syntax of transition functions, traces, and corrections.

from the trace element (τ5.robotAngy = 0) and simplifies the trigonometric expressions. In contrast, line 8 applies a trigonometric function to a parameter (sin(viewAngp )). This makes viewAngp an unrepairable parameter that cannot appear in the residual transition function. SRTR substitutes unrepairable parameters with their concrete values from the parameter map.

In general, the MakeResidual function of SRTR (lines 1115 in Figure 5) takes a transition function (T), a trace element (τt), and a parameter map (P) and produces a residual transition function by partially evaluating the transition function with respect to the trace element and the unrepairable parameters. We use a simple dataflow analysis to calculate the unrepairable parameters (Unrep(T)) and a canonical partial evaluator (Peval) [Jones et al., 1993].

4.3 Transition Repair as aMaxSMT Problem

Given the procedure for calculating residual transition functions, SRTR proceeds in three steps. 1) It translates each correction ci into an independent formula φi. A solution to φi corresponds to parameter adjustments that satisfy the correction ci. Note however that no solution exists if ci cannot be satisfied. 2) It combines the formulas φ1···n for all corrections c1···n from the previous step into a single formula Φ with independent penalties wi for each sub-formula φi. A solution to Φ corresponds to parameter adjustments that satisfy a subset of the corrections. Any unsatisfiable corrections incur a penalty. 3) Finally, it formulates a MaxSMT problem that minimizes the magnitude of adjustments (‖δj ‖) to the parameters, and the penalty (wi ) of violated sub-formulas.

The CorrectOne function transforms a single correction into a formula. This function 1) calculates the residual transition function (Figure 5, line 18), 2) gets the repairable parameters (line 19), and 3) produces a formula (line 20) with a variable for each repairable parameter. In our running example, the transition function has four parameters, but, as explained in the previous section, the residual has only three parameters since viewAngp is unrepairable. Therefore, the formula that corresponds to this residual (Figure 3c) has three variables (δ1 , δ2 , and δ3 ). Moreover, since the correction (c5) requires the next-state to be Kick, which only occurs when the residual takes the true-branch (line 3 of the residual), the body of the formula is equivalent to the conditional expression (lines 1-2), but with each parameter replaced by the sum of its concrete value (from P) and its adjustment (a δ). For example, the formula replaces aimMarginp by π/50 + δ1 . Therefore, when δ1 = 0, the parameter is unchanged.

The CorrectAll function supports multiple corrections and uses CorrectOne as a subroutine. The function iteratively builds a conjunctive formula Φ, where each clause has a distinct penalty wi and two mutually exclusive cases: either wi = 0 thus the clause has no penalty and the adjustments to the parameters satisfy the ith correction (line 27); or a penalty is incurred (wi = H) and the ith correction is violated. Thus H ∈ R+ is a hyperparameter that induces a tradeoff between satisfying more corrections vs. minimizing the magnitude of the adjustments: large values of H satisfy more corrections with larger adjustments, whereas small values of H satisfy fewer corrections with smaller adjustments. The final formula has m real-valued variables δi for adjustments to the corresponding m repairable parameters xip , and n discrete variables wj that represent the penalty of violating

1 // Takes a transition function T , and returns a partially evaluated residual transition 2 // function T ′ by eliminating identifiers xi using their values ki . 3 def Peval(T,x1 ↦→k1 · · · xn ↦→kn ); 4 5 // Returns the list of repairable parameters of the transition function T 6 def Rep(T); 7 8 // Returns the list of unrepairable parameters of the transition function T 9 def Unrep(T); 10 11 def Residual(T,τt,P): 12 {in=〈 l∀ i=1xiy ↦→ki 〉, vars=〈 m∀ j=1xjv ↦→k′j 〉, state=st ↦→k′′ s } := τt 13 {x1p , · · · , xnp } = Unrep(T) 14 T ′ := Peval(T, l∀ i=1xiy ↦→ki , m∀ j=1xjv ↦→k′j , n∀ k=1xkp ↦→P (xkp ), st ↦→k′′ s ) 15 return T ′ 16 17 def CorrectOne(T,τt,P,ct): 18 T ′ := Residual(T,τt) 19 {x1p , · · · , xmp } := Rep(T) 20 return ∃δ1 , · · · , δm : ct = T ′ (s1, x′1 p + δ1 , · · · , x′m p + δm) 21 22 def CorrectAll(T, P, R, {c1t , · · · , cnt }): 23 {x1p , · · · , xmp } = Rep(T) 24 Φ = true 25 for i ∈ [1 · · · n]: 26 ∃δ1 , · · · , δm : φi = CorrectOne(T,R[t],P,cit ) 27 Φ = Φ∧ (wi = H ⊻ (wi = 0 ∧ φi)) 28 return ∃δ1 , · · · , δm,w1 , · · · ,wn : Φ 29 30 def SRTR(T, P, R,{c1t , · · · , cnt }): 31 assert(CorrectAll(T,P,R,{c1t , · · · , cnt })) 32 minimize(Σi=1wi +Σmj=1 ‖δj ‖) 33 {x1p , · · · , xmp } = Rep(T) 34 return [x1p ↦→P(x1p ) + δ1 , · · · , xmp ↦→P(xmp ) + δm]

formula φj corresponding to correction cjt .

Our example (Figure 3c) has one correction and three repairable parameters. Therefore, CorrectAll produces a formula with four variables: a single penalty (w1 ) and the three adjustments discussed above (δ1 , δ2 , and δ3 ). The formula is a single exclusive-or: either the penalty is zero and formula is equivalent to the result of CorrectOne or the penalty is one and the result of CorrectOne is ignored.

Finally, the SRTR function uses CorrectAll as a subroutine and invokes the MaxSMT solver. This function 1) adds the assertion returned by CorrectAll to the solver, 2) directs the solver to minimize the sum of penalties and the sum of the magnitude of parameter changes (line 32 in Figure 5), and 3) returns a map from repairable parameter names to their new values. In our example, the solver calculates that the minimum-cost solution has δ2 = 0.5 with other variables set to zero. i.e., we can satisfy the correction by adjusting maxDistp from 80 to 80.5.

In summary, SRTR adjusts parameters to satisfy userprovided corrections. It is not always possible to find an adjustment that satisfies all corrections. Moreover, there is a tradeoff between making larger adjustments and satisfying more corrections. Therefore, SRTR uses a MaxSMT solver to formulate the parameter adjustment problem. A limitation of this approach is that a parameter may appear in a context cannot be expressed as a formula for the MaxSMT solver. We use a simple analysis to determine which parameters cannot be repaired.

5 Evaluation

We evaluate SRTR in four ways. 1) We compare SRTR to an exhaustive search; 2) We show how the number of corrections affect RSM performance and that SRTR requires only a small number of corrections to perform well; 3) Using three RSMs, we show that SRTR does not over-fit and performs well in new scenarios; and 4) We use SRTR to improve the performance of a real-world robot.

We present three RSMs in this section and measure their success rates as follows. The attacker (Figure 1a) fills the main offensive role in robot soccer. Its success rate is the fraction of the test scenarios where it successfully kicks the ball into the goal. The deflector (Figure 6a) plays a supporting role in robot soccer, performing one-touch passing [Bruce et al., 2008]. Its success rate is the fraction of the test scenarios where it successfully deflects the ball. The docker (Figure 6b) is a non-soccer behavior which drives a differential drive robot to line up and dock with a charging station. Its success rate is the fraction of the test scenarios where it successfully docks with the charging station.

5.1 Comparison To Exhaustive Search

Using the attacker, we compare SRTR to an exhaustive search to show that 1) SRTR is dramatically faster and 2) the adjustments found by SRTR are as good as those found by exhaustive search. To limit the cost of exhaustive search, the experiment only repairs the six parameters that affect transitions into the Kick state; we bound the search space by the physical limits of the parameters; and we discretize the resulting hypercube in parameter space. We evaluate each parameter set using 13 simulated positions and manually specify if the position should transition to the Kick state.

We evaluate the initial parameter values, the SRTRadjusted parameters, and the parameters found by exhaustive search on 20,000 randomly generated scenarios. Table 1 reports the success rate and running time of each approach. SRTR and exhaustive search achieve a comparable success rate. However, SRTR completes in 10 ms whereas exhaustive search takes 1,300 CPU hours (using 100 cores).

5.2 Scalability

Using the attacker, we now show how the number of corrections affects SRTR solver time and success rate. Starting with the same set of initial parameters used in Section 5.1, we first create a training dataset by simulating the attacker in 40 randomly generated scenarios. For each scenario, we provide one correction, thus we have a training set of 40 corrections. Each trial applies SRTR to a subset of these corrections and evaluates the success rate using 150 random test scenarios. We repeat this procedure for each number of corrections N ∈ [1, 40] with 50 randomly chosen subsets of the training set (i.e., 300,000 total trials). Figure 7a shows how the number of corrections affects the success rate. It is possible for a single informative correction to dramatically increase the success rate, or for a particularly under-informative correction to have little effect. Therefore we also report the mean success rate and show the 99% confidence interval in gray. Success rate increases with the number of corrections, and with 23 corrections, the attacker reaches a peak success rate of 87%. Figure 7b shows that the solver time increases linearly with the number of corrections, and remains less than 0.04s with 40 corrections.

5.3 Generalizability

Since SRTR uses a handful of user-provided corrections to adjust parameters, there is a risk that it may over-fit and underperform in new scenarios. We use three RSMs to show that 1) SRTR-adjusted parameters generalize to new scenarios and that 2) SRTR outperforms a domain-expert who has 30 minutes to manually adjust parameters.

Table 2 summarizes the results of this experiment. We evaluate the success rate of the Attacker, Deflector, and Docker RSMs on a test dataset with several thousand test scenarios each. The baseline parameters that we use for these RSMs have a low success rate. We give a domain expert complete access to the RSM code (i.e., the transition and emission functions), and subsequently our simulator for 30 mins. In that time, the expert is able to dramatically increase the success rate of the Deflector, but has minimal impact on the success rate of the Attacker and the Docker. Finally, we apply SRTR using a handful of corrections and the baseline parameters. The SRTR-adjusted parameters perform significantly better than the baseline and domain-expert parameters.

The heat maps in Figure 8 illustrates how parameters found

X

(a) Expert-adjusted parameters. (b) SRTR-adjusted parameters. Figure 8: Attacker success rate with respect to different initial ball positions. The corrections are marked with a cross.

by the domain-expert, and by SRTR generalize to novel scenarios with the Attacker. In both heat maps, the goal is the green bar and the initial position of the Attacker is at the origin. Each coordinate corresponds to an initial position of the ball and for each position we set the ball's initial velocity to 12 uniformly distributed angles. With the expert-adjusted parameters, the Attacker performs well when the ball starts in its immediate vicinity, but performs poorly otherwise. However, with SRTR-adjusted parameters, the Attacker is able to catch or intercept the ball frommost positions on the field. For this result, we required only two corrections and the cross-marks in the figure show the initial position of the ball for both corrections. Therefore, although SRTR only adjusted parameters to account for these two corrections, the result generalized to many other positions on the field.

5.4 Case Study: SRTR In The Real World

To evaluate SRTR in the real world, we follow the same procedure that experts use (summarized in Table 3): we develop the Attacker in a simulator, we adjust parameters until it performs well in simulation, and then we find that it performs poorly in the real world. To evaluate the success rate of the attacker in the real world, we start the ball from 18 positions on the field and repeat each position five times with the same velocity (i.e., 90 trials). The parameters from simulation have a 25% success rate. Using the execution logs of this experiment, we apply SRTR with three corrections. The adjusted parameters increase the success rate to 73%. In practice, an expert would iteratively adjust parameters, so we apply SRTR again with 2 more corrections, which increases the success rate to 86%. Finally, our group has an attacker that we tested and optimized extensively for RoboCup 2017, where it was part of a team that won the lower bracket. This Competition Attacker has additional states to handle special cases that do not occur in our tests. On our tests, the Competition Attacker's success rate is 76%. Therefore, with two iterations of SRTR, the simpler Attacker actually outperforms the Competition Attacker in typical, real-world scenarios.

6 Conclusion

This paper presents SMT-based Robot Transition Repair (SRTR), which is a semi-automatic white-box approach for adjusting the transition parameters of Robot State Machines. We demonstrate that SRTR: 1) increases success rate for multiple behaviors; 2) finds new parameters quickly using a small number of annotations; 3) produces solutions which generalize well to novel situations; and 4) improves performance in a real world robot soccer application.

Acknowledgements

This work is supported in part by AFRL and DARPA agreement #FA8750-16-2-0042, and by NSF grants CCF-1717636 and CNS-1413985.