Interactive Robot Transition Repair With SMT
Jarrett Holtz, Arjun Guha, Joydeep Biswas

arXiv:1802.01706v1 [cs.RO] 5 Feb 2018

University of Massachusetts Amherst

Abstract
Complex robot behaviors are often structured as
state machines, where states encapsulate actions
and a transition function switches between states.
Since transitions depend on physical parameters,
when the environment changes, a roboticist has to
painstakingly readjust the parameters to work in
the new environment. We present interactive SMTbased Robot Transition Repair (SRTR): instead of
manually adjusting parameters, we ask the roboticist to identify a few instances where the robot is
in a wrong state and what the right state should be.
A lightweight automated analysis of the transition
function’s source code then 1) identifies adjustable
parameters, 2) converts the transition function into
a system of logical constraints, and 3) formulates
the constraints and user-supplied corrections as a
MaxSMT problem that yields new parameter values. Our evaluation shows that SRTR is effective
on real robots and in simulation. We show that
SRTR finds new parameters 1) quickly, 2) with
only a few corrections, and 3) that the parameters
generalize to new scenarios. We also show that a
simple state machine corrected by SRTR can outperform a more complex, expert-tuned state machine in the real world.

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

Start

Go To

Intercept

Catch

Kick

End

(a) Attacker state machine

(b) Execution traces

Figure 1: A robot soccer attacker a) state machine, with b) successful
(blue) and unsuccessful (red) traces to Intercept a ball (orange) and
Kick at the goal. The green box isolates the error: the successful
trace transitions to Kick, the unsuccessful trace remains in Intercept.

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.
We have the following key insights: a roboticist debugging
a robot can frequently identify when something goes wrong,
and what it 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: the roboticist does not need to enumerate a
complete sequence of states, the parameters to adjust, how to
adjust them, or even identify all errors.
We present SMT-based Robot Transition Repair (SRTR),
an approach to adjusting the parameters of robot state machines that leverages program repair techniques that have
gained traction in programming languages and software engineering research. Specifically, we define the grammar of
a repairable robot transition function as a subset of generalpurpose imperative programming languages. During execution, we log execution traces of the transition function. After
execution, the roboticist examines the execution traces and
corrects a handful of transitions. 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 changes to the parameters, while maxi-

mizing 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 anonymized competition.

2

Related Work

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 [Yang et al., 2014; 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]. SRTR addresses the problem of repair even when
the dependence of the behaviors on parameters is not explicitly modeled. It automatically discovers such dependencies
by analysis of the source code of the transition function.
Human input can help overcome the limitations of autonomous algorithms [Kamar, 2016; Redacted, 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 high-dimensional
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 source 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.
Automated program repair is an active area of research in
software engineering and programming languages. For example, DirectFix [Mechtaev et al., 2015] formulates program
repair as a MaxSMT problem and deems a program repaired
when all tests pass. Physical robots don’t have deterministic test cases and even user-provided corrections can be contradictory. SRTR uses MaxSMT to minimize changes and
maximize the number of satisfied corrections. There are several other domains that are not amenable to unit-testing. For
example, Tortoise [Weiss et al., 2017] allows the user to fix
system configuration errors using the Unix shell and propagates fixes to a system configuration specification. Whereas
Tortoise requires the user to completely fix the system, SRTR
only requires a partial specification.
Programming by example can synthesize programs from a
small number of examples; the approach has been very effective in domains such as synthesizing string transformations
on spreadsheet data [Gulwani, 2011]. RobustFill [Devlin et
al., 2017] generalizes the approach to also support noisy data.
Program templates can also be used to to synthesize task and
motion plans that satisfy user plan outlines [Nedunuri et al.,
2014]. Unlike these approaches, SRTR does not synthesis
new program structure and focuses on adjusting parameters.
For generalizability, SRTR minimizes the magnitude of adjustments and uses MaxSMT to discard noisy corrections.

3

Background

We use a real-world example to motivation SRTR: a robot
soccer attacker (also called a striker). The attacker must
1) go to the ball if the ball is stopped, 2) intercept the ball
if it is moving away from the attacker, 3) catch the ball if
it is moving toward the attacker, and 4) kick 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 [Kalmár-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 shows the structure of the attacker RSM.
In this paper, we assume that the output of each feedback
controller is nominally correct—while there might be minor
performance degradation of each controller when environmental factors change, we assume that they are convergent,
and hence will eventually result in 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, and the robot’s motor efficiency affect 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 parame-

ters are incorrect for the given environment.
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47

inputs ballLoc : Vector2D , ballVel : Vector2D ,
robotLoc : Vector2D , robotVel : Vector2D ,
robotAng : Float , robotAngVel : Float ,
targetAng : Float ;
variables kickTime : Float ;
parameters kickedThresh , timeoutThresh , aimErrorThresh ,
angleVelThresh , distanceThresh , relativeYThresh ,
relativeVelThresh , alignThresh , offsetThresh ,
catchVelThresh , ivThresh ;
if (s == "START ") {
s = "GOTO"
} else if (s == "KICK ") {
robotHeading = [cos( robotAng ), sin( robotAng )];
if (|| ballVel · robotHeading || > kickedThresh ) {
s = "END"
} else if ( kickTime > timeoutThresh ) {
s = "START"
} else {
s = "KICK" }
} else {
ballToRobot = ballLoc - robotLoc ;
aimError = AngleMod ( targetAng - robotAng );
ballVelTarget = Rotate (ballVel , targetAng );
robotVelTarget = Rotate (robotVel , targetAng );
ballToRobotVel = robotVelTarget - ballVelTarget ;
robotYAxis = [-sin( robotAng }, cos( robotAng )];
ballToRobotY = robotYAxis · ballToRobot ;
ballIntercept = ballLoc +
,→ || ballVel || * UnitVector ( ballToRobot );
interceptOffset = || ballIntercept - robotLoc ||;
interceptVel = ballVel *
,→ ballVel · UnitVector ( ballToRobot );
if ( aimError < aimErrorThresh &&
robotAngVel < angleVelThresh &&
|| ballToRobot || < distanceThresh &&
[0, 1] · ballToRobotVel < relativeYThresh &&
|| ballToRobotVel || < relativeVelThresh &&
|| ballToRobotY || < alignThresh ) {
s = "KICK"
} else if ( interceptOffset < offsetThresh &&
|| ballVel || > catchVelThresh &&
|| interceptVel || / || ballVel || > ivThresh ) {
s = "CATCH"
} else if (|| ballVel || > catchVelThresh ) {
s = " INTERCEPT "
} else {
s = "GOTO" } }

Figure 2: Transition function of an attacker.

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
hS, S0 , SF , V, V0 , Y, U, T, Gi, 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 variables 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.
Figure 2 shows the transition function for the attacker, written in C-style pseudocode. The function depends on the inputs and variables (declared on lines 1–5) and uses them to

Unary Operators
op 1 ::= - | sin | cos | · · ·
Expressions
e ::= k
| s
| xv
| xy
| xp
| op 1 (e)
| e1 op 2 e2

Constants
State
Variables
Inputs
Parameters

Transition Functions
T ::= { m1 ; · · · ; mn }

Binary Operators
op 2 ::= + | - | * | > | · · ·
Statements
m ::= s := e
| xv := e
| if (e) m1 else m2
| { e1 ; · · · ; en }
Parameter Maps
n
P ::= hx1p 7→ k1 · · · xn
p 7→ k i
Traces
R ::= [τ1 · · · τn ]
Corrections
ct ::= s : s ∈ S

Trace Elements
m

n

i=1

j=1

τt ::= {in = h ∀ xiy 7→ ki i, vars = h ∀ xjv 7→ k0j i, state = st 7→ ks00 }

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

perform geometric calculations. The function has 11 different
parameters (lines 6–9) that determine when certain transitions
occur. The figure does not specify the parameters’ values, but
they are global constants. Finally, the transition function uses
a few helpers that we elide: UnitVector scales a vector by
its L2-norm, AngleMod bounds an angle to the range [−π, π),
and Rotate rotates a vector by an angle.

3.2

Transition Errors

Figure 1b shows two traces of the attacker. In the blue trace,
the attacker 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 high-level 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, 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.

4

Interactive Robot Transition Repair

The SRTR algorithm (lines 32–36 of Figure 4) has four inputs: 1) the transition function, 2) a map from parameters
to their values, 3) an execution trace, and 4) a set of userprovided 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) It parses the transition
function code and converts it to an abstract syntax tree for repair (Section 4.1). 2) It uses a lightweight program analysis
to identify parameters that cannot be repaired, and 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).

1

1

n

e

n

1 def Peval(T ,x 7→ k · · · x 7→ k ):
2
3

4
5
6 def Rep(T):
7 // Produces the parameters of T that do not need to be partially evaluated.
8
9 def Unrep(T):
10 // Produces the parameters of T that must be partially evaluated.
11
12 def Residual(T ,τt ,P ):
13

l

m

i=1

j=1
m

{in = h ∀ xiy 7→ ki i, vars = h ∀ xjv 7→ k0j i, state = st 7→ ks00 } := τt
0

l

Peval(T , ∀ xiy
i=1

i

, ∀ xiv
j=1

0i

, st 7→ ks00 )

14

T :=

15

0
{x1p , · · · , xn
p } = Unrep(T )
0
0
T := Peval(T ,x1 7→ P (x1 ), · · · , xn 7→ P (xn ))
return T 0

16

7→ k

7→ k

17
18
19 def CorrectOne(T ,τt ,P ,ct ):
20
21
22

T 0 := Residual(T ,τt )
{x1p , · · · , xm
p } := Rep(T )
1
0m
m
return ∃δ 1 , · · · , δ m : ct = T 0 (s1 , x01
p + δ , · · · , xp + δ )

23
1

n

24 def CorrectAll(T , P , R, {ct , · · · , ct }):
25
26
27
28
29
30
31

{x1p , · · · , xm
p } = Rep(T )
Φ = true
for i ∈ [1 · · · n]:
∃δ 1 , · · · , δ m : φi = CorrectOne(T ,R[t],P ,cit )
Φ = Φ ∧ (wi = H Y (wi = 0 ∧ φi ))
return ∃δ 1 , · · · , δ m , w1 , · · · , wn : Φ
1

n

32 def SRTR(T , P , R,{ct , · · · , ct }):
1
n
33 assert(CorrectAll(T ,P ,R,{ct , · · · , ct }))
34
35
36

cos(θy ) < xp
cos(xp )
θp + π
sin(θp + π)

// 1) Substitute xi with ki in T . 2) Simplify all operations and conditionals
// with immediate arguments until simplification is no longer possible.
return T 0 // partially evaluated T

j
minimize(Σi=1 wi + Σm
j=1 kδ k)
1
m
{xp , · · · , xp } = Rep(T )
m
m
return [x1p 7→ P (x1p ) + δ 1 , · · · , xm
p 7→ P (xp ) + δ ]

Figure 4: The core SRTR algorithm.

3) Finally, it uses the residual transition functions to formulate an optimization problem for an off-the-shelf MaxSMT
solver [Bjørner et al., 2015]. The solution to this problem is
an adjustment to the parameter values (Section 4.3).

4.1

The Language Of Transition Functions

To abstract away language-specific details of our repair procedure, we first parse the source code and convert it into an
idealized imperative language that only has features essential
for writing transition functions (Figure 3). The language has
a special identifier s that refers to the current state and other
identifiers have a subscript to indicate whether they are inputs
(xy ), parameters (xp ), or ordinary variables (xv ). The transition function can read any identifier, but it can only write to
variables and the state. Figure 3 has a list of operators that
often appear in transition functions, such as arithmetic and
trigonometric functions, but the list is not exhaustive. Finally, a transition function (T ) is a block of statements and
a parameter map (P ) assigns values to the parameters in T .
An execution trace is a sequence of trace elements (τt ). A
trace element records the values of sensor inputs, ordinary
variables, and the state at the start of time-step t. In contrast,
a user-provided correction (ct ) specifies the expected state at
the end of time-step t. To repair parameters, SRTR estab-

τ.vars

τ.in

e0

P

θy = 0

1 < xp
−1
θp + π
0

xp 7→ π
xp 7→ π
xp 7→ π
xp 7→ π

Table 1: Examples of residuals and repairable parameters.

lishes constraints that relate the observed initial state, the expected output state, and the other identifiers.

4.2

Residual Transition Functions

SRTR needs to translate the transition function into a logical
formula for the SMT solver. However, solvers do not have decision procedures for non-linear arithmetic and trigonometry,
both of which commonly occur in transition functions.
Partial Evaluation [Jones et al., 1993] is a technique that
specializes programs to work on specific inputs. For example,
if we partially evaluate the program cos(x) + y for x 7→ 0,
we get the program 1 + y. In general, partial evaluation first
substitutes identifiers with concrete values and then simplifies
the program as much as possible. SRTR uses a canonical
partial evaluator for transition functions, which we call Peval
( Figure 4, line 1). The arguments of Peval are a transition
function and a mapping from identifiers to constants.
The Residual function specializes a transition function for
a particular trace element. We call its result a residual transition function. Residual first partially evaluates the transition
function with respect to all the sensor inputs and variable values recorded in the trace element (line 14). This step eliminates most functions that the solver cannot represent, thus the
only identifiers that remain are the parameters and the state.
For example, the first row of Table 1 shows an expression
that uses a trigonometric function. If this expression occurs
in the transition function, its residual after partial evaluation
is a simple inequality that cannot be further simplified.
However, it is possible for the transition function to use a
parameter in a context that the solver cannot represent. For
example, the second row of Table 1 applies a trigonometric
function to a parameter and the first step of Residual simply
yields the original expression. (i.e., Peval(cos(xp )) = cos(xp )).
To address this, Residual calculates the set of parameters that
cannot be repaired (line 15) and partially evaluates once again
with respect to their values in the parameter map (line 16).
Therefore, the final result in this example is −1.
The Residual function uses a pair of auxiliary functions
Rep and Unrep to calculate the set of parameters that can, and
cannot be repaired. These functions perform a lightweight
analysis by mutual recursion over the transition function.
Mutual recursion is necessary because a parameter may not
be repairable even if its immediate context is repairable. For
example, the third row of Table 1 shows an expression with
a repairable parameter thus its residual is θp + π. However,
the fourth row embeds the same expression in a context that
makes it unrepairable, thus the residual is partially evaluated
using the parameter map, yielding 0.

4.3

Transition Repair as a MaxSMT Problem

This section presents how SRTR formulates a MaxSMT
problem in three steps. 1) It translates each correction into

an independent formula. A solution to this formula (if one
exists) corresponds to parameter adjustments that satisfy the
correction. 2) It combines the formulas from the previous
step into a single formula with independent weights for each
sub-formula. A solution to this formula corresponds to parameter adjustments that satisfy a subset of the sub-formulas.
Any sub-formulas that could not be satisfied have a positive
weight. 3) Finally, we formulate a MaxSMT problem that
minimizes the magnitude of adjustments and the weight of
violated sub-formulas.
The CorrectOne function transforms a single correction
into a formula. This function 1) calculates the residual transition function (Figure 4, line 20), 2) gets the repairable parameters (line 21), and 3) produces a formula (line 22) with
a variable δ i that corresponds to an adjustment to the ith repairable parameter. This formula constrains the residual transition function’s output state to be equal to the correction.
Therefore, if the correction differs from the post-state of the
transition function at run-time, the solution to the formula
will have a non-zero adjustment for at least one of the repairable parameters. (i.e., δ i 6= 0 for some i.)
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 weight wi and two mutually exclusive cases: Either 1)
wi = 0 thus the clause has no cost and the adjustments to the
parameters satisfy the ith correction (line 29) or 2) 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 allow more corrections to be satisfied, and
small values of H minimize the magnitude of the 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 cost of violating
formula φj corresponding to correction cjt .
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 weights and the sum of the
magnitude of parameter changes (line 34), and 3) returns a
map from repairable parameter names to their new values.

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), which is
our running example, 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 5a) plays a supporting role in robot soccer, performing one-touch passing [Bruce et al., 2008]. Its success

Start

Setup

Wait

Kick

End

(a) Deflector RSM

S1 Left

S1 Forward

End

Start

S2 Left

S2 Forward

S1 Right

S2 Right

(b) Docker RSM

Figure 5: RSMs used for experiments
Method
Success Rate (%) CPU Time
Initial Parameters
44
—
Exhaustive Search
89 1,300 hr
SRTR
89
10 ms
Table 2: Success rate and CPU time compared to exhaustive search.

rate is the fraction of the test scenarios where it successfully
deflects the ball. The docker (Figure 5b) 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 2
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 N ∈ [1, 40] with 50 randomly chosen subsets of the training set (i.e., 300,000 total
trials). Figure 6a 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 6b shows

0.04

RSM
Solver Time (s)

Success Rate (%)

70

60

0.03

Attacker
Deflector
Docker

0.02

SRTR
Corrections
12
2
5
3
9
3

Params

80

Success Rates (%)
Baseline Expert SRTR
57,600
42
44
89
16,776
1
65
80
5,000
0
0
100
Tests

Table 3: Success rates for baseline, expert, and SRTR parameters.

0.01

50

0.00
0

10

20

30

Number of Corrections

(a) Success Rate

40

0

10

20

30

40

Number of Corrections

(b) Solver Time

Figure 6: Scaling of SRTR with number of corrections. We report
the mean as a line, the 99% confidence interval in grey, inliers in
blue, and outliers in red. Darker points represent more occurrences.

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 overfit 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 3 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 7 illustrates how parameters found
by the domain-expert, nd 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 from most 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 4): we develop
the Attacker in a simulator, we adjust parameters until it performs well in simulation, and then we find that it performs

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

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 anonymized competition,
where it was part of a team that won the lower bracket. This
Competition Attacker has additional states to handle special
casesthat 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.
Trial
Competition Attacker
Parameters from Simulation
Real World SRTR Tuning 1
Real World SRTR Tuning 2

Success Rate (%)
75
24
73
85

Table 4: Attacker success rates on a real robot.

References
[Abbeel and Ng, 2011] Pieter Abbeel and Andrew Y Ng. Inverse reinforcement learning. In Encyclopedia of machine
learning, pages 554–558. Springer, 2011.
[Argall et al., 2009] Brenna D. Argall, Sonia Chernova,
Manuela Veloso, and Brett Browning. A Survey of Robot
Learning From Demonstration. Robotics and Autonomous
Systems, pages 469 – 483, 2009.
[Bai and Russell, 2017] Aijun Bai and Stuart Russell. Efficient Reinforcement Learning with Hierarchies of Machines by Leveraging Internal Transitions. In IEEE International Conference on Robotics and Automation, 2017.
[Biswas et al., 2014] Biswas, Mendoza, Zhu, Choi, Klee,
and Veloso. Opponent-driven planning and execution for
pass, attack, and defense in a multi-robot soccer team.
In International Conference on Autonomous Agents and
Multi-Agent Systems, pages 493–500, 2014.
[Bjørner et al., 2015] Nikolaj Bjørner, Anh-Dung Phan, and
Lars Fleckenstein. νZ-an optimizing SMT solver. In International Conference on Tools and Algorithms for the
Construction and Analysis of Systems, pages 194–199.
Springer, 2015.
[Bruce et al., 2008] James Bruce, Stefan Zickler, Mike Licitra, and Manuela Veloso. CMDragons: Dynamic Passing and Strategy on a Champion Robot Soccer Team. In
IEEE International Conference on Robotics and Automation, pages 4074–4079, 2008.
[Cano et al., 2016] José Cano, Alejandro Bordallo, Vijay
Nagarajan, Subramanian Ramamoorthy, and Sethu Vijayakumar. Automatic configuration of ros applications
for near-optimal performance. In IEEE/RSJ International
Conference on Intelligent Robots and Systems, pages
2217–2223, 2016.
[Dantam et al., 2013] Neil Dantam, Ayonga Hereid, Aaron
Ames, and Mike Stilman. Correct Software Synthesis for
Stable Speed-Controlled Robotic Walking. In Robotics:
Science and Systems, 2013.
[Devlin et al., 2017] Jacob Devlin, Jonathan Uesato, Surya
Bhupatiraju, Rishabh Singh, Abdelrahman Mohammad,
and Pushmeet Kohli. RobustFill: Neural program learning under noisy I/O. In ICML, 2017.
[Gulwani, 2011] Sumit Gulwani. Automating string processing in spreadsheets using input-output examples. In ACM
SIGPLAN Notices, pages 317–330. ACM, 2011.
[Holtz and Biswas, 2017] Jarrett Holtz and Joydeep Biswas.
Automatic Extrinsic Calibration of Depth Sensors with
Ambiguous Environments and Restricted Motion. In
IEEE/RSJ International Conference on Intelligent Robots
and Systems, pages 2235–2240, 2017.
[Jones et al., 1993] Neil D. Jones, Carsten K. Gomad, and
Peter Sestoft. Partial Evaluation and Automatic Program
Generation. Prentice-Hall, Inc., 1993.
[Kalmár-Nagy et al., 2004] Tamás Kalmár-Nagy, Raffaello
D’Andrea, and Pritam Ganguly. Near-Optimal Dynamic

Trajectory Generation and Control of an Omnidirectional
Vehicle. Robotics and Autonomous Systems, pages 47–64,
2004.
[Kamar, 2016] Ece Kamar. Directions in Hybrid Intelligence: Complementing AI Systems with Human Intelligence. In IEEE International Conference on Robotics and
Automation, 2016.
[Mechtaev et al., 2015] Sergey Mechtaev, Jooyong Yi, and
Abhik Roychoudhury. DirectFix: Looking for Simple Program Repairs. In IEEE/ACM International Conference on
Software Engineering, pages 448–458, 2015.
[Meriçli et al., 2012] Çetin Meriçli, Manuela Veloso, and
H Levent Akın. Multi-resolution corrective demonstration
for efficient task execution and refinement. International
Journal of Social Robotics, pages 423–435, 2012.
[Mericli et al., 2014] Cetin Mericli, Steven D. Klee, Jack Paparian, and Manuela Veloso. An Interactive Approach for
Situated Task Specification Through Verbal Instructions.
In Autonomous Agents and Multi-agent Systems, pages
1069–1076, 2014.
[Miyazawa et al., 2017] Alvaro Miyazawa, Pedro Ribeiro,
Wei Li, Ana Cavalcanti, and Jon Timmis. Automatic property checking of robotic applications. In IEEE/RSJ International Conference on Intelligent Robots and Systems,
pages 3869–3876, 2017.
[Nedunuri et al., 2014] Srinivas Nedunuri, Sailesh Prabhu,
Mark Moll, Swarat Chaudhuri, and Lydia E. Kavraki.
SMT-based synthesis of integrated task and motion plans
from plan outlines. In IEEE International Conference on
Robotics and Automation, pages 655–662, 2014.
[Redacted, 2018] Redacted. Human-in-the-loop slam. In
Redacted, 2018.
[Weiss et al., 2017] Aaron Weiss, Arjun Guha, and Yuriy
Brun. Tortoise: Interactive System Configuration Repair. In IEEE/ACM International Conference on Automated Software Engineering, pages 625–636, 2017.
[Wong et al., 2014] Kai Weng Wong, Rädiger Ehlers, and
Hadas Kress-Gazit. Correct High-level Robot Behavior
in Environments with Unexpected Events. In Robotics:
Science and Systems, 2014.
[Yang et al., 2014] Xiangdong Yang, Liao Wu, Jinquan Li,
and Ken Chen. A Minimal Kinematic Model for Serial
Robot Calibration Using POE Formula. Robotics and
Computer-Integrated Manufacturing, pages 326 – 334,
2014.

