Dynamics-Based Reactive Synthesis and Automated Revisions
for High-Level Robot Control
Jonathan A. DeCastro ∗†
Sibley School of Mechanical and Aerospace Engineering, Cornell University, Ithaca, NY 14853, USA
Rüdiger Ehlers
Department of Computer Science, University of Bremen, 28359 Bremen, Germany
Matthias Rungger
Department of Electrical Engineering and Information Technology, Technical University of Munich,
80333 Munich, Germany
Ayça Balkan and Paulo Tabuada
Electrical Engineering Department, University of California, Los Angeles, Los Angeles, CA 90095,
USA
Hadas Kress-Gazit
Sibley School of Mechanical and Aerospace Engineering, Cornell University, Ithaca, NY 14853, USA
Abstract
The aim of this work is to address issues where formal specifications cannot be realized on a given dynamical system
subjected to a changing environment. Such failures occur whenever the dynamics of the system restrict the robot in such
a way that the environment may prevent the robot from progressing safely to its goals. We provide a framework that
automatically synthesizes revisions to such specifications that restrict the assumed behaviors of the environment and the
behaviors of the system. We provide a means for explaining such modifications to the user in a concise, easy-to-understand
manner. Integral to the framework is a new algorithm for synthesizing controllers for reactive specifications that include
a discrete representation of the robot’s dynamics. The new approach is demonstrated with a complex task implemented
using a unicycle model.
∗This work was supported by the NSF Expeditions in Computing project ExCAPE: Expeditions in Computer Augmented Program Engineering [grant
number CCF-1138996].
† Corresponding author; e-mail: jad455@cornell.edu
arXiv:1410.6375v2  [cs.RO]  13 Jan 2016
Dynamics-Based Reactive Synthesis and Automated Revisions
2
1. Introduction
One of the benefits of the formal methods approach to robot mission planning is that it frees users from the burdens
of programming controllers for complicated robot tasks, removing the arduous step of re-validation every time the task
changes; see, e.g. Kloetzer & Belta (2008), Kress-Gazit et al. (2009), Tabuada & Pappas (2006), Wolff et al. (2013),
Wongpiromsarn et al. (2010). Application of provably-correct controllers on fielded systems requires that the correctness
guarantees extend to a possibly complex set of dynamics describing the robot. Recently, tools have been proposed for
generating discrete abstractions for a wide class of nonlinear systems, e.g. Girard et al. (2010), Pola et al. (2008), Reißig
(2011), Zamani et al. (2012). It is natural to exploit such abstractions when synthesizing controllers that are applicable to
complex physical systems. This paper serves to solidify such a synthesis approach.
When composing tasks for applications such as self-driving cars, household robots, and disaster response robots, the user
must specify both the desired system behaviors and any assumptions on the sensed environment. Often, such assumptions
incorporate knowledge of the behavior of humans and other elements in the robot’s physical surroundings. If any of these
assumptions conflict with the specified task in the context of a robot’s dynamics, the specification is considered to be
unrealizable. That is to say, the environment is allowed to work against fulfilment of the specification by the robot assigned
to the task. As the underlying cause for unrealizability is often difficult to determine, automated frameworks for debugging
specifications (Könighofer et al. (2009), Raman & Kress-Gazit (2013)) and generating environment assumptions (Alur
et al. (2013), Fainekos (2011), Li et al. (2011)) have gained attention recently.
This paper seeks to address the problem of realizability of specifications for robots with dynamics by introducing a
novel framework that automatically suggests additions to the specification to resolve unrealizability issues. We do so by
introducing a new synthesis approach that takes a specification agnostic to the dynamics of the robot, and synthesizes a
controller (if possible) for a specific robot, given its discrete abstraction. If it turns out that the specification is unrealizable,
we automatically generate revisions to the specification that render the task realizable with respect to the robot dynamics.
These formulas effectively alter the environment assumptions and robot behaviors. The drawback of generating revisions
independently of the user is that the resulting specifications may fail to capture the original intent of the mission. We
address this by advocating for an means explaining such revisions in a manner that is simple to understand, permitting user
interaction as the revisions are computed.
When considering dynamics, unrealizability can arise as a result of unwanted effects such as overshooting into undesired
regions or an inability to make progress toward goals. Take the following scenario where rooms A and B are separated by
a door:
Visit rooms A and B. Avoid the door if it is closed. Assume that, infinitely often, the door is open.
In the above scenario, the robot must be able to robustly avoid the walls of the workspace (boundaries) and appropriately
react to the door as it opens and closes. If one applies this specification to robot with inertia, the task could fail because
the robot may not be able to stop by the time the door closes, violating the statement “Avoid the door if it is closed.” By
leveraging both the system dynamics and the specification, we could recover by adding the environment assumption “The
door must not close if within 1 meter of it.” In this paper, we explore an automated method for suggesting such revisions.
The remainder of this paper is outlined as follows. In Section 2, we review relevant formal definitions and notation. We
formally state the problem in Section 3, and address related work in the context of the problem in Section 4. In Section 5,
we describe our approach for synthesis for specifications involving discrete abstractions. We present the approach for
generating formulas and user feedback in Section 6. Next, we demonstrate our approach for a complex task carried out by
an abstraction of a unicycle robot model in Section 7. Lastly, we provide a summary in Section 8.
Dynamics-Based Reactive Synthesis and Automated Revisions
3
2. Preliminaries
2.1. Linear Temporal Logic
Linear temporal logic (LTL) formulas are defined over the set AP of atomic propositions in the recursive grammar:
ϕ ::= true | π | ϕ1 ∧ϕ2 | ¬ϕ | ⃝ϕ | ϕ1Uϕ2
where π is an atomic proposition in AP. Respectively, ∧and ¬ are the Boolean operators “conjunction” and “negation”,
and ⃝and U are the temporal operators “next” and “until”. From these operators, the following operators are derived:
“disjunction” ∨, “implication” ⇒, “equivalence” ⇔, “always” □, and “eventually”
□
.
AP consists of a set of environment propositions X describing the state of the discretized robot sensor values and a
set of system propositions Y describing the current pose of the robot in the workspace. For a set of propositions X, let
⃝X = {⃝πi}πi∈X be the set of propositions with the “next” operator. The LTL formulas are evaluated over infinite
sequences σ = σ0σ1σ2 . . . of truth assignments to the propositions in AP. σ is said to satisfy ⃝ϕ, □ϕ, or
□
ϕ if ϕ holds
true in the next position in the sequence, every position, or at some future position(s), respectively. We refer the reader to
Vardi (1996) for a complete definition of the syntax and semantics of LTL formulas.
Definition 1 (Robot Mission Specification). The specifications we consider are LTL formulas of the form:
ϕ := (ϕe
i ∧ϕe
t ∧ϕe
g)
|
{z
}
ϕe
=⇒(ϕs
i ∧ϕs
t ∧ϕs
g)
|
{z
}
ϕs
The formulas ϕα
i , ϕα
t , and ϕα
g are defined over AP, where ϕα
i are formulas for the initial conditions, ϕα
t the allowed
transitions (safety conditions) to be satisfied always, ϕα
g the goals (liveness conditions) to be satisfied infinitely often, and
α = {e, s} (with e for ‘environment’ and s for ‘system’). The liveness guarantees take the form V
i∈Iα □
□
(Bα
i ), where
Iα is the index set of environment goals (Be
i ) or system goals (Be
i ).
Definition
2
(Controller
Strategy
and
Execution). Define
a
controller
as
a
finite-state
machine
A
=
(S, S0, X, Y, δ, γX , γY), where S is the set of controller states, S0 ⊆S is the set of initial controller states, X and Y
are sets of propositions described above, δ : S × 2X →S is a state transition relation providing the next state s′ ∈S given
the next state s ∈S and the current value of the environment input z ∈2X , i.e. s′ = δ(s, z), γX : S →2X is a labelling
function mapping controller states to the set of environment propositions evaluating to True for all transitions into that
state, and γY : S →2Y is a labelling function mapping controller states to the set of robot configuration propositions
evaluating to True in that state.
Consider an infinite execution σ of A, where σ = (γX (s0), γY(s0))(γX (s1), γY(s1)), . . . for s0 ∈S0 and si ∈S,
i > 0. ϕ is deemed realizable if there exists a finite-state machine A such that every execution produced by A satisfies ϕ.
That is, at every i ≥0, there exists an assignment of system variables Y for all possible assignments of the environment
variables X such that σ satisfies ϕ. If there exist some environment behaviors on X for which no such A can be found,
then ϕ is unrealizable.
A discrete controller can be synthesized from a specification follows by solving a two-player game played between the
environment and the system, as described in Bloem et al. (2012).
2.2. Synthesis over a Connectivity Graph
A connectivity graph is an undirected graph describing those workspace regions that are accessible and adjacent to one
another.
Dynamics-Based Reactive Synthesis and Automated Revisions
4
Given a bounded configuration space W ⊂Rn, let R = {R1 . . . Rp} represent a set of disjoint regions whose closure
covers W, where the open sets Ri ⊆W. Let Y be the set of propositions representing the workspace regions over which
the topology model will be specified and πi ∈Y denote a region proposition that evaluates to True when the robot is in
Ri ∈R.
Definition 3 (Topology Model). We define the topology model as a formula ϕtop
t
over Y that encodes the allowed next
regions given the current region. This formula is defined as follows:
ϕtop
t
=
^
πi∈Y
□



πi =⇒
_
πj∈Y:
cl(Ri)∩cl(Rj)̸=∅
⃝πj



,
where cl(·) denotes the closure operation on a set. Note that we also enforce mutual exclusion of regions; that is, the robot
is only allowed to occupy one region at a time.
When combining the user specifications ϕe and ϕs with the topological model, we obtain the formula ϕe
=⇒
(ϕs ∧ϕtop
t
) written over AP top = X ∪Y. A controller A is synthesized if ϕe =⇒(ϕs ∧ϕtop
t
) is realizable.
2.3. Synthesis over Robot Abstractions
Our model of the behavior of the robot is a nonlinear differential equation
˙ξ(t) = f(ξ(t), ν(t))
(1)
given by the function f : Rn × Rm →Rn, where ξ(t) is the continuous state of the robot and ν(t) the command input
of the robot at time t ∈R≥0. We use ξx,ν to denote a trajectory of (1) with initial state x and input signal ν. We impose
the usual regularity assumptions on f that imply the existence and uniqueness of solutions of (1). Moreover, we assume
that (1) is forward-complete (its solution is defined for all t ≥0), see e.g. Angeli & Sontag (1999).
We produce an estimate of the divergence of neighboring trajectories to obtain a conservative over-approximation of
the continuous dynamics operating under a sample-and-hold controller framework. Let β : R≥0 × R≥0 →R≥0 be a
continuous function, that satisfies β(0, 0) = 0 and β(·, t) is strictly increasing for every t ∈R≥0. Let us assume that any
pair of trajectories produced by the robot dynamics (1) satisfy
|ξx,ν(t) −ξx′,ν(t)| ≤β(|x −x′|, t),
(2)
with x, x′ ∈Rn, t ∈R≥0 and constant input function ν ∈U. Given that (1) is Lipschitz continuous with constant L, the
function β(r, t) = reLt satisfies (2).
In constructing a discrete abstraction, we follow the approach in Pola et al. (2008), Reißig (2011), Zamani et al. (2012)
for discretizing the bounded configuration space W ⊂Rn and the bounded space of command inputs U ⊂Rm. We denote
[W]η to be the uniform grid on W discretized with resolution η. This grid is defined as follows:
[W]η := {x ∈W | ∃k ∈Zn : x = kη}.
We introduce the discretization parameters τ, η, µ ∈R>0, where η and µ define, respectively, the discretization of the robot
configuration and command input spaces, and τ represents the sampling time.
We next denote a set of configuration propositions Ya describing the robot’s pose, and a set of locomotion command
propositions Ua describing the controlled actions taken by the robot. We assume throughout that Ua consists of purely robot
Dynamics-Based Reactive Synthesis and Automated Revisions
5
locomotion commands; the set can be generalized to capture other robot actions (e.g. wave hand, activate alarm), but this
extension is omitted in this paper.
Definition 4 (Discrete Abstraction). The discrete abstraction Sa(τ, η, µ) is defined by the tuple (Qa, Va, δa, γY
a , γU
a ),
where:
• Qa = [X]η is the set of discretized robot configurations;
• Va = [U]µ is the set of discretized robot locomotion commands;
• δa : Qa × Va →2Qa is a transition relation defined such that, there exists qa, q′
a ∈Qa and va ∈Va, q′
a ∈δa(qa, va)
iff there exists ξx,ν with ν(t) = va, for all x ∈{x0 | |x0 −qa| ≤η/2} and t ∈[0, τ), such that
|q′
a −ξx,ν(τ)| ≤β(η/2, τ) + η/2;
(3)
• γY
a : Qa →Ya labels each discretized configuration with the associated proposition in Ya that evaluates to True
when the robot is in the given configuration;
• γU
a : Va →Ua labels each discretized command with the associated proposition in Ua that evaluates to True when
the given command is active.
Additionally, we define γa : R →2Ya, a labelling function associating each region to a set of configuration propositions,
as γa(Rj) = {γY
a (qa) | qa ∈[Rj]η}. Finally, we encode the transitions δa as a safety formula ϕa
t defined over Ya ∪⃝Ua ∪
⃝Ya of the form
ϕa
t =
^
γY
a (qa)∈Ya
γU
a (va)∈Ua
□





γY
a (qa) ∧⃝γU
a (va)


=⇒
_
γY
a (q′
a)∈Ya:
q′
a∈δa(qa,va)
⃝γY
a (q′
a)




.
Suppose Ya = {π0, π1, π2}, Ua = {πfwd} and we start at grid cell π0 at q0. Assume that the set of possible successor
configurations under this command consists of cells 1 and 2; i.e. δa(q0, v0) = {q1, q2}, where γY
a (q1) = π1, γY
a (q2) = π2
and γU
a (v0) = πfwd. In this example, we write □((π0 ∧⃝πfwd) =⇒⃝(π1 ∨π2)) as the corresponding safety formula.
2.4. Ensuring Correctness of the Continuous Behaviors
In the following, we briefly review the rules derived in Fainekos et al. (2009), Fainekos & Pappas (2009), Liu & Ozay
(2014), Liu et al. (2012) for modifying LTL formulas ϕe, ϕs on AP top to account for the behaviors of the continuous
system in between sampling instants. Given the system (1), there exists a constant b ∈R≥0 such that for all ξ(t) ∈W,
u ∈U and t ∈[0, τ), we have
|f(ξ(t), u)| ≤b.
(4)
Through the process of inflation and deflation of physical workspace regions R, we obtain the Sa-strengthened formulas
ˆϕe and ˆϕs. Conservative under-approximations ˇRε
i (where regions are deflated or shrunk) and over-approximations ˆRε
i
(where regions are inflated) may be constructed as follows:
ˇRε
i = {x ∈Rn | {x} + εB ⊆Ri}
ˆRε
i = {x ∈Rn | x ∈Ri + εB}.
Here we use + to denote the Minkowski set addition and B to denote the closed ball in Rn with respect to the infinity norm
| · | with radius τb. Supposing that the formulas ϕe, ϕs are in negated normal form, i.e., the negation only appears in front
Dynamics-Based Reactive Synthesis and Automated Revisions
6
of atomic propositions, we define the Sa-strengthened formulas ˆϕe, ˆϕs by
ˆϕα = ϕα[¬πtop,i/¬γa( ˆRε
i ), πtop,i/γa( ˇRε
i )],
(5)
in which we are replacing the region propositions πtop,i ∈Y with γa( ˇRε
i ) and ¬πtop,i with ¬γa( ˆRε
i ).
By application of Theorem 1 of Liu & Ozay (2014) to the semantics in Fainekos et al. (2009), it is shown that, by
choosing ε ≥bτ, we are assured that the continuous trajectory of (1) satisfies (ϕe ∧ϕa
t ) =⇒ϕs if the sampled-time
execution satisfies ( ˆϕe ∧ϕa
t ) =⇒ˆϕs.
Similar to Liu et al. (2013), we treat the possible non-determinism in the abstraction as adversarial: at each time-step,
the environment assigns values to the environment X. Then, the locomotion command is updated based on this input, and
the abstraction chooses potential successor states to transition into given the current locomotion command. We therefore
treat ϕa
t as a statement on the environment and adopt the formula ( ˆϕe ∧ϕa
t ) =⇒
ˆϕs over AP = X ∪Ya ∪Ua. We
describe in Section 5 our procedure for checking realizability for this formula.
The synthesis of a discrete controller ASa given the formula ϕe =⇒(ϕs ∧ϕtop
t
) and an abstraction Sa involves the
following steps: (1) computation of the formula ϕa
t from Sa (Section 2.3); (2) computation of the Sa-strengthened formulas
ˆϕe, ˆϕs from the original formulas ϕe, ϕs (Section 2.4); and (3) extracting a strategy as is discussed in Section 5.
3. Problem Formulation
Let ϕ be a realizable formula, defined as
ϕ := ϕe =⇒(ϕs ∧ϕtop
t
),
in the set of atomic propositions AP top under the assumption of a topological model ϕtop
t
, where the formulas ϕe and
ϕs are, respectively, the user-defined environment assumptions and system guarantees. Additionally, we require that ϕe is
not falsified by robot behaviors satisfying ϕs (i.e. no trivial behaviors). We refer to ϕ as a general formula. The goal is to
synthesize controllers for such specifications.
Problem 1 (Synthesis under non-deterministic abstractions). Given the subformula ϕa
t for the robot abstraction and the
Sa-strengthened formulas ˆϕe and ˆϕs, synthesize a controller for the robot-specific specification
ϕabs := ( ˆϕe ∧ϕa
t ) =⇒ˆϕs.
in the set of propositions AP.
If ϕabs is unrealizable, determine a set of revisions to the specification that render the new specification realizable. A
revision is a temporal logic formula that may be conjuncted with the original formula. Recall ϕabs is unrealizable if there
exists some environment behavior admissible by the formula ˆϕe ∧ϕa
t such that no system behaviors satisfy ˆϕs.
Problem 2 (Generating revisions). Given a realizable ϕ, an unrealizable ϕabs, an abstraction Sa, and the Sa-strengthened
formulas ˆϕe and ˆϕs, automatically derive a set of formulas for the environment and the system such that
ϕmod := ( ˆϕe ∧ϕa
t ∧ψe
g ∧ψe
t ) =⇒( ˆϕs ∧ψs
t )
(6)
is realizable and ˆϕe ∧ϕa
t ∧ψe
g ∧ψe
t and ˆϕs ∧ψs
t are satisfiable.
If such formulas exist, the user is provided with a suggested liveness assumption ψe
g and suggested set of safety assump-
tions and guarantees, ψe
t and ψs
t , respectively. For each transition formula, a simple-to-interpret statement summarizing
each suggested revision is provided to the user. To illustrate the problem, consider the following example.
Dynamics-Based Reactive Synthesis and Automated Revisions
7
Example 1. Consider a robot tasked with fetching parts in a factory setting, illustrated in Figure 1. Here, stockroom,
station_1 and station_2 are regions in the workspace belonging to Y and s1_occupied and s2_occupied are sensors
belonging to X indicating when the respective region is occupied. The robot is required to visit the stockroom and the two
workstations (system liveness) but avoid visiting those that are occupied (system safety). If the robot is within a workstation,
the environment is required to keep that station unoccupied (environment safety). Also, the workstations are required to
infinitely often be unoccupied (environment liveness).
The general specification ϕ is as follows:
□
□
stockroom ∧□
□
station_1 ∧□
□
station_2
◁sys liveness
□
□
¬s1_occupied ∧□
□
¬s2_occupied
◁env liveness
□(s1_occupied =⇒⃝¬station_1)
◁sys safety
□(s2_occupied =⇒⃝¬station_2)
◁sys safety
□(station_1 =⇒¬s1_occupied)
◁env safety
□(station_2 =⇒¬s2_occupied)
◁env safety
The specification ϕ is realizable. Suppose now we are given a fully-actuated planar robot governed by inertia, described
by the system
¨x = u
¨y = v,
(7)
where (u, v) ∈U are robot commands and (x, y) ∈R2 are the Cartesian robot coordinates. We derive an abstraction Sa of
these dynamics in the configuration space (x, y, ˙x, ˙y) ∈W and obtain the formula ϕabs. With Sa, we want to synthesize
a realizable controller for ϕabs that satisfies the task given an abstraction of these dynamics, with additional restrictions
placed on the behaviors of the environment and the system.
Fig. 1. Resupply example.
Unrealizability can arise from a number of possible causes. One possibility is that the robot’s inertia may prevent it
from avoiding collisions with either one of the workstations upon sensing that it is occupied. Consider the case where
s1_occupied is False and the robot is moving toward station_1. Suppose that, when moving, the robot must pass through
two grid cells to decelerate to a stop. Then, the specification is unrealizable if s1_occupied is allowed to become True
Dynamics-Based Reactive Synthesis and Automated Revisions
8
when the robot is within two grid cells of station_1. This is an example of a deadlock behavior; the environment can force
the system into certain states that have no legal transitions.
Another possibility is that the environment may toggle between states infinitely often, preventing the physical robot
from making progress toward its goals. For instance, suppose the robot is approaching station_1 or station_2 and the
environment toggles the values of s1_occupied and s2_occupied infinitely often. The robot in this case will be always
changing directions, but unable to reach any of its goals before the environment changes once again. This is an example of
a livelock behavior; the robot is prevented from reaching its goals as a result of repeating sequence of environment inputs.
The behavior does not exist in the general formula because the topology graph always allows the robot to either remain in
place or transit to an adjacent region once the environment has moved.
4. Related Work
We present a method that finds appropriate revisions to a specification when the inclusion of discrete abstractions cause
unrealizability of specifications. Our work intersects with two lines of research: synthesis with dynamics, and assumption
mining for reactive synthesis. We address related work in both of these areas below.
Synthesis with Dynamics. Tomlin et al. (2000) were among the first to generate verified controllers preserving safety
and reachability specifications for nonlinear dynamical systems. In their approach, controllers are constructed by posing
the problem as a differential game in hybrid systems (systems with mixed continuous and discrete states) analysis. The
work of Mitchell et al. (2005) made such “reach-avoid” problems tractable through viscosity solutions to time-dependent
partial differential equations.
Progress has been made more recently in developing techniques for synthesis of controllers satisfying specifications with
more expressive requirements than reachability and safety. Namely, Kress-Gazit et al. (2009, 2011) introduce algorithms
for reactive synthesis that take advantage of the bisimulation property allowing high-level controllers to be synthesized
separately from the robot-specific low-level controllers. In order to bridge the gap between the high- and low-levels of
abstraction, tools for automatically synthesizing controllers in the continuous domain based on high-level specifications
have been introduced recently in DeCastro & Kress-Gazit (2014), Fainekos et al. (2006). Bhatia et al. (2010), Maly et al.
(2013) have solved this problem using multi-layered synthesis approaches, where certain parts of the control strategy are
left open for an online planner to complete at runtime.
Another perspective has been to incorporate the dynamics directly into the reactive synthesis process. Rather than
having an additional step for synthesizing continuous controllers that adhere to the behaviors of high-level controller, Liu
et al. (2013) introduce a discrete abstraction of the underlying dynamics (Girard et al. (2010), Reißig (2011), Zamani et al.
(2012)) directly into the synthesis process. The problem of synthesizing controllers using abstractions of physical systems
is well-studied: in provably-correct mission planning, researchers have considered robot dynamics ranging from simple
single or double integrators (Fainekos et al. (2009), Kress-Gazit et al. (2009)) and piecewise linear models (Tumova et al.
(2010), Yordanov et al. (2012)) to nonlinear (Bhatia et al. (2010), Girard et al. (2010), Wolff et al. (2013), Wongpiromsarn
et al. (2010), Zamani et al. (2012)), switched (Liu et al. (2013)) and hybrid systems (Maly et al. (2013)). In Kloetzer & Belta
(2008), non-deterministic abstractions are used to synthesize non-reactive LTL formulas using model checking methods.
LTL synthesis for switched systems was considered in Liu & Ozay (2014), Liu et al. (2013), where the authors propose
methods for computing fine-grained abstractions and switching protocol synthesis for reactive tasks. Our work is inspired
by the nonlinear synthesis methods of Liu et al. (2013), Pola et al. (2008), Zamani et al. (2012). Where our approach differs
is that our synthesis algorithm takes specifications written agnostic to the robot and produces controllers that are applicable
to a given robot platform, given its discrete abstraction. We furthermore explore the case when the dynamics contribute to
the unrealizability of such specifications and supply revisions in such cases.
Dynamics-Based Reactive Synthesis and Automated Revisions
9
Assumption Mining. Unrealizable specifications that are complicated to parse greatly benefit from automated tools
for computing revisions that restrict the environment and system behaviors. Our approach for computing such revisions is
closely related to recent methods described in Fainekos (2011), Li et al. (2011), and Alur et al. (2013). In Fainekos (2011),
a method is devised for determining the cause of unrealizability for non-reactive tasks and providing specification recom-
mendations to the user. In the reactive setting, Li et al. (2011) present a debugging method for unrealizable specifications
based on templates (LTL formulas) mined from an environment counterstrategy. In essence, a counterstrategy captures the
possible behaviors for the environment for which there are no safe system moves that allow it to fulfill its goals. The method
in Alur et al. (2013) generates templates of the form “
□
” and “
□
□” automatically from the counterstrategy, yielding
additional safety and liveness environment statements that remove all execution traces of the counterstrategy. The work
of Li et al. (2014) apply the counterstrategy-based environment assumption mining technique to an early warning system in
human-in-the-loop control systems, demonstrated in an autonomous driving scenario. By removing the behaviors present
in the counterstrategy, the modified environment is restricted in such a way as to permit the system to realize its goals under
the strengthened assumptions, but can sometimes lead to specifications that no longer match the user’s intent.
Finding specific portions of the counterstrategy that lead to unrealizability is in general difficult without additional
information or without post-processing the counterstrategy. Raman & Kress-Gazit (2013) developed algorithms to extract
cores (minimal LTL formulas) for explaining unrealizable specifications. Similar to their work, we aim to identify two types
of counterstrategy behaviors: deadlock and livelock. Where the authors use an “unrolling depth” to discover counterstrategy
states leading to livelock (a cycle of environment inputs locking the robot away from its goals), we apply a similar notion
to finding states leading to deadlock (a counterstrategy state where no further system transitions exist).
Our approach differs from existing works in several other ways. First, we adopt different strategy than Alur et al.
(2013), Li et al. (2011) for computing revisions, that depends on whether deadlock or livelock is being removed from
the counterstrategy. Second, we devise a means for efficiently computing revisions that reduces the number of times a
counterstrategy needs to be synthesized. Lastly, we explain the revisions in a simple-to-understand manner. For example,
the user will be provided with feedback in a structured format: “The specification is realizable as long as a person is not
present when the robot is within 2 meters of the Hallway.”
5. Reactive Synthesis Under Nondeterministic Robot Abstractions
We synthesize reactive controllers by solving a two player game carried out between the environment (player 1) and the
system (player 2) using the fixed-point algorithm described in Bloem et al. (2012). As described in this section, we make
modifications to this algorithm in order to accommodate the adversarial nature of the discrete abstraction and preserve
a mapping between ϕ and ϕabs. We also distinguish the expressive properties of the proposed approach with alternative
approaches (e.g. Liu et al. (2013)).
Definition 5 (Controller Strategies for Non-deterministic Discrete Abstractions). A controller in our abstractions-based
paradigm is a non-deterministic finite-state machine ASa = (S, S0, X, Ya, Ua, δ, γX , γY, γU), where S, S0, X, Ya, Ua, and
γX are as described in Definition 2, δ : S × 2X →2S is a state transition relation providing the set of possible states at the
next position in the sequence given the current controller state and the current value of the environment input, γY : S →2Ya
is a labelling function mapping controller states to a set of possible robot configurations evaluating to True for transitions
into that state, and γU : S →2Ua is a labelling function mapping controller states to a set of possible commands in that
state.
Note that each state captures the possibility of non-determinism in the abstraction, obviating the sets-of-sets definition
for γY. The robot configuration may be regarded as being an additional environment input, but differs in that the value
it takes is not defined until the system chooses a control input. We therefore define an execution as a sequence of moves
made by the environment and system, where the environment gets an extra move once the system has moved; in particular
Dynamics-Based Reactive Synthesis and Automated Revisions
10
σ = (γX (s0), γU(s0), γY(s0))(γX (s1), γU(s1), γY(s1)), . . ., where the robot motion at the current position in the sequence
is a result of the environment input and robot command at the same position.
The three-move formulation is in contrast to the two-move formulation of Liu et al. (2013), where the state of the
dynamical system at the current position in the sequence depends on the environment input and command at the previous
position. Recall that, as we require a controller ASa given the general-purpose formula ϕe
=⇒
(ϕs ∧ϕtop
t
), the
three-move formulation allows for there to be a mapping between the subformulas ϕe, ϕs and ˆϕe, ˆϕs. For example, the
safety guarantee ϕs
t = □((person ∧⃝¬person) =⇒⃝¬r1) has no equivalent counterpart ˆϕs
t in the method of Liu
et al. (2013). The reason is that both person and r1 are environment variables, and the fact that the system is required
to move before r1 is decided forces r1 to be delayed to the next position in the execution. The translation is therefore
□((person ∧⃝¬person)
=⇒
⃝⃝¬r1), which is not in GR(1). Our strategy, on the other hand, allows for the
environment to take an additional move after the system has moved, thereby preserving the mapping without delaying
choosing r1 to the next step.
We are able to assert that ϕabs is realizable if, for all positions in the execution and for all possible valuations of the
environment variables X, there exists a command Ua such that all executions of ASa satisfy the specification for all Ya. ϕabs
is unrealizable if there exists some environment behavior(s) such that no Ua can be found for which all robot configurations
yield executions that satisfy the specification.
In order to determine if ϕabs is realizable, our focus on the GR(1) (generalized reactivity (1)) fragment lends to efficient
solutions, as described in Bloem et al. (2012). Solving the GR(1) game is carried out by first introducing a game structure,
defined as follows.
Definition 6 (Game Structure). A game structure is represented by the tuple G = (V, θ, ρe, ρr, ρs, ϕwin), where:
• V = X ∪Ua ∪Ya is the set of proposition valuations representing the position in the game;
• θ ⊆2V is the set of initial positions;
• ρe ⊆2V × 2⃝X is a transition relation defining the set of environment inputs allowed by ϕe
t at the next position
given the proposition values at the current position in the game;
• ρr ⊆2V × 2⃝Ua × 2⃝Ya is a transition relation derived from the robot formula ϕa
t defining the set of allowed robot
configurations at the next position given the command at the next position and the robot configuration at the current
position in the game;
• ρs ⊆2V × 2⃝V is a transition relation defining the set of commands and robot configurations allowed by ϕs
t at the
next position given the proposition values at the current position in the game; and
• ϕwin is the winning condition.
The algorithm in Bloem et al. (2012) proceeds by considering winning positions that satisfy the system and environment
safety transition relations while leading the system toward its goals. With the robot abstraction, we are faced with the
additional step of ensuring that the positions chosen are safe for all possible robot configurations. We therefore begin by
specifying the following enforceable predecessor operator Pre:
JPreWK := {v ∈2V | ∀vx ⊆X, ∃vu ⊆Ua, ∀vy ⊆Ya :
((v, vx) ∈ρe) =⇒[((v, vu, vy) ∈ρr) =⇒
[((v, vx, vu, vy) ∈ρs) ∧((vx, vu, vy) ∈JWK)]]}.
where JϕK denotes the set of positions for which the formula ϕ evaluates to True. Intuitively, the enforceable predecessor
is a set of positions enforcing that, for all environment inputs satisfying the environment transition relation, there exists a
robot command such that all robot configurations bound to the transitions of the abstraction yields behaviors that remain
safe, as long as the successor positions are taken from the set W.
Dynamics-Based Reactive Synthesis and Automated Revisions
11
We next define a set of winning positions Vwin based on the µ-calculus formula Bloem et al. (2012) Vwin =
νW1. V
is∈Is µW2. W
ie∈Ie νW3.Nisie, where Nisie = (Bs
is ∧PreW1) ∨PreW2 ∨(¬Be
ie ∧PreW3) and ν and µ rep-
resent, respectively, the greatest and least fixpoint operators. This formula ensures that there is a move that places the
system strictly closer to one of its goals or one in which the system prevents one of the environment goals. Note that the
control strategy we derive must be consistent with the physical system. The strategy ASa that we extract from the winning
set of positions is therefore preventing from falsifying the discrete abstraction ϕa
t (for example, those in which the robot is
commanded to move to a configuration beyond W) by choosing only those control actions that also satisfy ϕa
t .
5.1. Counterstrategies for Nondeterministic Robot Abstractions
When a specification is unrealizable, one may synthesize a counterstrategy to find a sequence of environment inputs and
robot configurations that prevent the robot from fulfilling its specification.
Definition 7 (Environment Counterstrategies for Non-deterministic Discrete Abstractions). We define an environment
counterstrategy as a finite-state machine Ac = (Qc, Qc
0, X, Ya, Ua, δc, γc
U, γc
X , γc
Y), where
• Qc is the set of counterstrategy states;
• Qc
0 ⊆Qc is the set of initial counterstrategy states;
• X, Ya and Ua are sets of propositions in AP;
• δc : Qc →2Qc is a nondeterministic transition relation returning the set of counterstrategy states at the next position
in the sequence given the current state;
• γc
U : Qc →2Ua is a labelling function mapping counterstrategy states to the set of locomotion command propositions
in Ua evaluating to True for all transitions into that state;
• γc
X : Qc →2X is a labelling function mapping counterstrategy states to the set of environment propositions in X
evaluating to True in that state, and;
• γc
Y : Qc →2Ya is a labelling function mapping counterstrategy states to the set of robot configurations in Ya
evaluating to True in that state.
We furthermore define δc−1 : 2Qc →Qc as the inverse transition relation mapping counterstrategy states to a set of
predecessors; i.e. δc−1(q′) = {q ∈Qc | q′ ∈δc(q)}.
Our approach to synthesizing counterstrategies resembles that of Könighofer et al. (2009), where we use a fixed point
computation to determine realizability of the specification, then extract a strategy Ac from the set of positions that are
winning for player 1. We define the enforceable predecessor operator for the counterstrategy Prec as follows:
JPrecWK := {v ∈2Vc | ∃vx ⊆X, ∀vu ⊆Ua, ∃vy ⊆Ya :
((v, vx) ∈ρe) ∧[[((v, vu, vy) ∈ρr)∧
((v, vx, vu, vy) ∈ρs)] =⇒((vx, vu, vy) ∈JWK)]}.
The set of winning positions Vc
win = X ∪Ua ∪Ya for player 1 may then be computed from the formula Vc
win =
µW1. W
is∈Is νW2. V
ie∈Ie µW3.N c
isie, where
N c
isie = (¬Bs
is ∨PrecW1) ∧PrecW2 ∧(Be
ie ∨PrecW3),
A counterstrategy is synthesized by storing the sets N c
isie for each is and ie at the last pass of the fixed point operation.
Starting at the initial conditions ϕe
i, ϕs
i, for each state we identify an index is of the liveness guarantee that is currently being
prevented by the counterstrategy. At a particular counterstrategy state q, we determine a successor q′ similar to Könighofer
et al. (2009) as follows. First, given the position v at state q, we fix an assignment of inputs v′
x ∈X. We next determine,
Dynamics-Based Reactive Synthesis and Automated Revisions
12
for this fixed assignment, the set of winning configurations v′
y ∈Ya that belong to N c
isie for every v′
u ∈Ua. A check is
made to determine if a liveness assumption has been fulfilled at q; if it has, then a new liveness assumption ie is selected.
For notational convenience, we define the set of successor values winning for player 1 at a counterstrategy state q as
MX (q) = {v′
x ∈X | ∀v′
u ∈Ua, ∃v′
y ∈Ya : (v, v′
x, v′
u, v′
y) ∈N c
is(q)ie(q), v = γc
X (q) ∪γc
U(q) ∪γc
Y(q)}. This set contains
the set of inputs for which there exist command-configuration combinations that are winning for player 1.
6. Generating Revisions to Unrealizable Specifications
In this section, we formalize our solution strategy for Problem 2. In similar fashion to Alur et al. (2013), Li et al. (2011),
we make use of environment counterstrategies in order to search for environment assumptions that render the specification
realizable. Our approach is outlined as follows: (1) from the specification ϕabs, we synthesize counterstrategies; (2) for
each counterstrategy found, we compute environment and system transition subformulas ψe
t and ψs
t that prevent transitions
to states in the counterstrategy from which the robot has no safe transitions (deadlock); (3) if a counterstrategy is found
that is free of deadlock states, we compute liveness assumptions ψe
g that restrict transitions to cycles of states preventing
the robot from fulfilling its goals (livelock). We introduce the following example to illustrate the major concepts discussed
in this section.
Example 2. ConsidertheworkspaceshowninFigure2a.GivenX = {sen}wheresenisthesensorinputandY = {r1, r2},
we write a specification ϕ requiring the robot to visit r2 (lower-left gray region) when s is False, but avoid r2 when sen
is True. Formally:
□
□
r2
◁ϕs
g
□
□
¬sen
◁ϕe
g
□(⃝sen =⇒⃝¬r2)
◁ϕs
t
□(r2 =⇒⃝¬sen)
◁ϕe
t
True
◁ϕs
i
True
◁ϕe
i
The controller satisfying this specification is given in Figure 2b.
Given an abstraction where Ya = {x1, . . . , x16} is an encoding of the set of 2-D robot configurations, and Ua =
{N, S, E, W} are the robot commands for motion in the four cardinal directions, we derive a new specification ϕabs,
where:
□
□
(x9 ∨x13)
◁ˆϕs
g
□
□
¬sen
◁ϕe
g
□(⃝sen =⇒⃝¬(x9 ∨x13))
◁ˆϕs
t
□((x9 ∨x13) =⇒⃝¬sen)
◁ˆϕe
t
True
◁ˆϕs
i
True
◁ˆϕe
i
The abstraction ϕa
t appears as arrows in the figure.
Dynamics-Based Reactive Synthesis and Automated Revisions
13
(a)
(b)
Fig. 2. 2-D example. (a) shows the workspace map and grid whose cells are labeled with the configuration variable. The white grid cells
denote r1, while the gray denote r2. (b) shows the synthesized controller for ϕ.
6.1. Adding Revisions for Preventing Deadlock
To prevent deadlock, we introduce a scheme to process a counterstrategy and extract a set of environment assumptions that
remove deadlock behaviors. Consider a counterstrategy Ac whose deadlock states are collected in Qdead. There exists an
execution that eventually reaches a deadlock state qi
dead; specifically when ∃q′ ∈δc(qi
dead) : q′ = ∅. We formally state
this behavior as W
qj∈δc−1(qi
dead)
□
ψ1(qj) ∧⃝ψ2(qi
dead)


, where ψ1(q) and ψ2(q) are propositional representations for
the subsets of positions at counterstrategy state q:
ψ1(q) =
^
π∈γc
U(q)∪γc
Y(q)
π ∧
^
π∈(Ua∪Ya)\(γc
U(q)∪γc
Y(q))
¬π,
ψ2(q) =
^
π∈γc
X (q)
π ∧
^
π∈X\γcs(q)
¬π.
In words, φ1(q) captures the command and configuration moves at state q, and ψ2(q) captures the environment input at q.
To remove the environment behaviors in the counterstrategy causing deadlock, we adopt the following formula:
^
qj∈δc−1(qi
dead)
□
ψ1(qj) =⇒⃝¬ψ2(qi
dead)


.
(8)
Before conjuncting each computed formula with ψe
t , a check is made to determine if it falsifies the left-hand side of ϕmod,
i.e. there is no transition that satisfies ˆϕe ∧ϕa
t ∧ψe
t . If this is the case, the formula is discarded and it is not included as a
conjunct in ψe
t .
Example 3. Returning to Example 2, suppose we obtain a counterstrategy containing the states q0, q1, q2, q3, q4, as pictured
in Figures 3a and 3b, starting in cell x3 with sen =False. One of the possible executions in this counterstrategy eventually
Dynamics-Based Reactive Synthesis and Automated Revisions
14
leads the robot to cell x4 with the sensor sen =True:
σ = ({∅}, {∅}, {x3}), ({∅}, {W}, {x2}), ({∅}, {W}, {x1}),
({∅}, {S}, {x5}), ({s}, {∅}, {∅}).
where the ith time step corresponds to qi. In this execution, the sensor sen remains False until the robot enters x5, at
which point a transition in ϕs
t is violated. Hence q4 is a deadlock state. The formula
□
(⃝sen ∧¬x1 ∧S)1 is extracted by
evaluating
□
(ψ1(q4)∧⃝ψ2(q4)). The complement of this formula, □((¬x1∧S) =⇒⃝¬sen), is added as an additional
environment assumption. This assumption negates the behaviors in the counterstrategy for that particular deadlock state.
Being that there is only one deadlock state, we add no further assumptions. Upon adding this revision to the environment
assumptions, we determine that the modified specification is realizable.
(a)
(b)
Fig. 3. (a) shows a partial counterstrategy for Example 3 leading to deadlock; (b) shows a corresponding robot trajectory leading to
deadlock, where the green part of the path denotes where sen =False and the red denotes where sen =True. The cells shaded yellow
indicate configurations in which there are no sequence of commands that avoid reaching r2 eventually.
Notice that the controller synthesized in Example 3 produces executions that satisfy the specification but the system now
assumes that the environment will always turn sen False whenever it reaches x5. In the example, consider the behavior
when the robot starts at x7 with sen True. The execution of the robot in this case is
σ = ({sen}, {∅}, {x7}), ({sen}, {W}, {x6}), ({sen}, {W}, {x5}),
({sen}, {S}, {x9}), ({∅}, {E}, {x10}), ({∅}, {N}, {x6}), . . . .
In this execution, sen remains True and, as the robot moves toward r2, the environment eventually must set sen to False
to be consistent with the added assumption. When outside of x5, the robot follows the same sequence of moves regardless
1 We only make the True action explicit (S in this case), since mutual exclusion disallows the other actions from being activated at the same time.
Dynamics-Based Reactive Synthesis and Automated Revisions
15
of the environment. Note that the controller for the original, realizable specification ϕ (Figure 2b) does not exhibit this
behavior because there is no imposition on how the environment must behave based on the robot’s configuration. In that
case, if sen is True, the robot waits in r1 until sen becomes False.
We remove such behaviors by disallowing a system transition whenever the same conditions found for the deadlock
state hold at the state previous to deadlock. The idea is to force the system to react conservatively to the newly-added
environment revision as if it were a deadlock state. Thus, when the robot is at a configuration previous to the deadlock state
and the deadlock conditions hold currently, it will be forbidden from entering the configuration prior to deadlock. On the
other hand, when the environment is not currently producing the same conditions as at deadlock, ψe
t forces the environment
to “play fair” with the robot by not producing those conditions in the next step once the robot has made its move.
Formally, we disallow the behavior W
qj∈δc−1(qi
dead)
□
(⃝¬ψ2(qi
dead) ∧⃝¬ψ1(qj)) by introducing an additional
revision on ϕs
t
^
qj∈δc−1(qi
dead)
□
⃝¬ψ2(qi
dead) =⇒⃝ψ1(qj)


.
(9)
Such a revision places a safety restriction on the robot, preventing it from entering a neighboring state to a deadlock
state whenever the environment is set to the same value for which deadlock occurs. Doing this produces a specification
that makes the system’s behavior conservative; we are strengthening the conditions under which the robot may enter the
neighboring state, when in fact the robot is not in any true danger of violating the original safety guarantees in ϕ until it
reaches r2. Nonetheless, if the specification is realizable, the system will be able to react to the environment as long as the
actions/configurations are not included in those specified in V
qj∈δc−1(qi
dead) ψ1(qj).
If the modified formula is determined to be unrealizable and new deadlock states are found at a state qj ∈δc−1(qi
dead),
then we once again return to the original set of circumstances specified in Problem 2. We repeat the process in this section
for as many times as required to eliminate deadlock states or when the specification is unrealizable. We may, however,
avoid repeated synthesis of counterstrategies by applying the assumption and guarantee revisions explained above to entire
subtraces of a single counterstrategy (a a finite word of an execution trace for the counterstrategy). To do this, we identify
states for which there is no safe command to be taken such that there exists a subtrace that eventually visits states in
Qc\Qdead. The search for deadlock revisions then reduces to a graph search on the counterstrategy, as summarized in
Algorithm 1. The algorithm builds up a set of deadlock-committed states Qcommit by adding, via a breadth-first search
(BFS in line 4), predecessor counterstrategy states from deadlock Qdead for which all locomotion commands lead to states in
Qcommit. For generating revisions and providing user feedback, we also maintain a mapping Qreach : Qcommit →2Qdead
of deadlock states reachable from each q ∈Qcommit. The search continues until a fixed point of states is reached where no
additional deadlock-committed states can be found, at which point BFS returns a tuple containing Qcommit and Qreach.
The precise condition under which the search terminates is when a q ∈Qc is found such that:
∃q′ ∈δc(q) : q′ /∈Qcommit.
Here, Qcommit plays the role of Qdead. We therefore replace Qdead in the safety revisions (8) and (9) with Qcommit. To
be precise, we replace (8) with
^
qj∈Qi
commit
□

ψ1(qj) =⇒
_
qk∈Qreach(qi
commit)
⃝¬ψ2(qk)


(10)
Dynamics-Based Reactive Synthesis and Automated Revisions
16
and (9) with
^
qj∈Qi
commit
□


^
qk∈Qreach(qi
commit)
⃝ψ2(qk) =⇒⃝¬ψ1(qj)



,
(11)
for each qi
commit ∈Qcommit. Consider the example below.
Algorithm 1 Computing deadlock-committed states.
procedure commitStates(Qdead)
Initialize Qnew, Qcommit, Qreach to Qdead
while Qnew ̸= ∅do
(Qnew, Qreach) ←BFS(Ac, Qcommit, Qreach)
5:
Qcommit ←Qcommit ∪Qnew
end while
return Qcommit, Qreach
end procedure
Example 4. Starting from the result of Example 3, we compute a set of four deadlock-commit states Qcommit =
{q1, q2, q3, q4} corresponding to the cells {x6, x2, x1, x5}. We obtain the following ψe
t formulas:
□((x5 ∧S) =⇒⃝¬sen)
(12)
□((x1 ∧S) =⇒⃝¬sen)
(13)
□((x2 ∧W) =⇒⃝¬sen)
(14)
□((x6 ∧N) =⇒⃝¬sen),
(15)
and the following ψs
t formulas:
□(⃝sen =⇒⃝¬(x5 ∧S))
(16)
□(⃝sen =⇒⃝¬(x1 ∧S))
(17)
□(⃝sen =⇒⃝¬(x2 ∧W))
(18)
□(⃝sen =⇒⃝¬(x6 ∧N)).
(19)
With these revisions added to ψe
t and ψs
t (highlighted orange in Figure 4, the modified specification eliminates the deadlock
states present in the original counterstrategy. Additionally, note that none of the revisions falsify the environment.
Upon synthesis, we find that a counterstrategy synthesized from this modified specification does not contain deadlock
states. In the next section, we discuss an approach to render the specification realizable by eliminating livelock behaviors.
6.2. Adding revisions for Preventing Livelock
In cases where the environment satisfies its own liveness conditions, the environment may be allowed to play in such a way
that as the system cycles through an infinite sequence of states, the environment always keeps it away from one of its goals.
Consider the behavior of the robot when the above ψe
t and ψs
t formulas (12)–(19) are introduced as revisions. Starting at
Dynamics-Based Reactive Synthesis and Automated Revisions
17
Fig. 4. Map showing configurations for which the revisions ψe
t and ψs
t from Example 4 apply; a counterstrategy execution trace, as
explained in Section 6.2. The green part of the path denotes where sen =False and the red denotes where sen =True.
x16, the following behavior is possible:
σ = ({∅}, {∅}, {x16}), ({∅}, {N}, {x12}), ({∅}, {N}, {x8}),
({sen}, {W}, {x7}), ({∅}, {S}, {x11}), ({∅}, {S}, {x15}),
({∅}, {E}, {x16}), ({∅}, {N}, {x12}), . . . .
In this execution(shown in Figure 4), the robot eventually cycles indefinitely between six cells in the workspace. Whenever
the robot visits the cell x7, the environment activates sen, forcing the robot to move S to avoid violating the safety guarantee
revision in (19). The environment is then able to satisfy its liveness goal (□
□
(¬sen)), while preventing the robot from
achieving its goal of reaching r2.
Once we obtain a counterstrategy free of deadlock states, we generate environment assumptions that remove the
counterstrategy executions that exhibit livelock. The idea is to selectively choose states in the counterstrategy for which the
robot still has winning actions to take and then apply liveness assumptions at those states to ensure that, always eventually,
the robot is allowed to take these actions. We employ the result of the innermost fixed point computation MX (q) stored
when solving the counterstrategy game to find any states for which there exists an assignment of environment inputs that are
not winning for the environment. Note that, for these inputs, there exists a command the robot may take which is winning
for the system. We then prevent the environment from always making such assignments at these counterstrategy states.
Formally, for all q ∈Qc, our goal is to find a subset Qcut ⊆Qc for which v′
x /∈MX (q), where MX (q) are the set of
environment inputs at a state q ∈Qc that are winning for player 1. Consequently, for any q ∈Qcut there are some v′
x ⊆X
and v′
u ⊆Ua that lead to a position that is not winning for player 1 (i.e. v′
x /∈MX (q)). One can think of Qcut as being those
counterstrategy states where it is possible that the environment has been able to “cut away” a command that will allow the
robot to proceed to its next goal by applying some environment input.
Using Qcut, we formulate a set of liveness assumptions that restrict the environment from always behaving in a manner
that prevents the system’s progress toward its goals. Notice that Qcut contains all states for which there is an environment
and system move not in player 1’s strategy; however, not all such moves are necessarily winning for player 2. For instance,
a state in Qcut could yield an environment input that does not allow player 1 to move strictly closer to its goal yet only
allow system moves that place the system further away from its goal.
We therefore form a set Pcut ⊆Qcut for which the robot has safe commands that are winning for the system. We use
Qcommit (from the deadlock counterstrategy) to define the set of states where there exist system moves that lead the system
Dynamics-Based Reactive Synthesis and Automated Revisions
18
closer to its goals. We populate Pcut as follows:
Pcut = {q ∈Qcut | ∃va ∈Va, ∃q′ ∈Qcommit, ∃qa ∈δa(va, γc
Y(q)) :
∀π ∈Ya, π ∈γY
a (qa) iff π ∈γc
Y(q′)}.
(20)
We then apply the environment liveness assumption
□
□
_
qi∈Pcut

ψ1(qi) ∧
^
qj∈δc(qi,γc
Y(qi))
⃝¬ψ2(qj)

.
(21)
This liveness formula disallows the environment from always behaving in a way that denies the system from taking action
that lead it closer to its goals, when the robot is in a configuration where there is such an action to be taken.
Example 5. With the specification ϕabs in Example 2 along with the revision (12)–(19), a counterstrategy is extracted as
pictured in Figure 6. The set Qcut consists of four states, {q3, q5, q6, q8}. Of these, {q3, q6, q8} are states in which the robot
has an action (move W) taking the robot closer to r2 that the environment can prevent. These are found from Example 3
and are collected in Pcut. We also find state {q5}, for which there is an environment move keeping it from immediately
realizing an environment goal (□
□
(¬sen)) but does not lead the system closer to its goal. We apply environment liveness
revisions ψe
g to the set Pcut:
□
□
((x7 ∧W ∧⃝¬sen) ∨(x3 ∧W ∧⃝¬sen) ∨(x7 ∧S ∧⃝¬sen)) .
(22)
The three above formulas correspond to regions appearing as blue regions in Figure 5. Adding this final revision produces
a specification ϕmod that is realizable.
Fig. 5. Map showing regions associated with cut states from Example 5.
6.3. User Feedback
Before modifying the specification with the computed deadlock revisions, we alert the user of the consequences of these
revisions. Given this information, the user may choose to accept these if they are, in fact, consistent with the original design
intent. We provide feedback in the form of statements such as “Keep sensor sen False if the robot enters to within N
meters of r2” instead of raw LTL formulas.
Dynamics-Based Reactive Synthesis and Automated Revisions
19
Fig. 6. Deadlock-free counterstrategy for Example 5.
For the combined environment and system revisions for deadlock, we use the mapping between cells and regions from
the robot abstraction to assist in forming this metric. For each labeled workspace region Ri ∈R, we mark those deadlock
states (if any exist) from whose predecessors there exists a robot command va ∈Va (Definition 4) to reach Ri. Those
marked deadlock states are collected in the set Pdead(Ri), defined formally as:
Pdead(Ri) = {q ∈Qdead | ∀q′ ∈δc−1(q), ∃va ∈Va, ∃q′
a ∈δa(va, γc
Y(q′)) :
∀π ∈Ya, π ∈γY
a (q′
a) iff π ∈γa(Ri)}.
In the fixed point computation in Algorithm 1, we keep track of each deadlock state reachable from each state added to
Qcommit. We use this stored information to find the distances between each robot configuration in Qcommit. Rather than
provide the user with a detailed set of conditions under which the environment would be required to adhere for the generated
revisions to be satisfied, we advocate for simplicity by computing a conservative upper-bound on robot configurations where
the environment restrictions must hold. For each Ri corresponding to a robot configuration that satisfies some deadlock
state in Qdead, we find the relative proximity to a deadlock condition (in terms of physical coordinates) by finding the
maximal pairwise distance between any states affected by the deadlock revisions:
(q⋆
i , q⋆
dead,i) =
arg max
q∈Qcommit,
q′∈Qreach(q)∩Pdead(Ri)
|γc
Y(q) −γc
Y(δc−1(q′))|.
(23)
Here, |vy| is the Euclidean norm of the real-valued abstraction state qa ∈Qa represented by a set of propositions vy ⊆Ya
that are True in that state. The pair of counterstrategy states q⋆
i and q⋆
dead,i are those corresponding to a revision for region
Ri where the distance is greatest, under the constraint that q⋆
dead,i is a deadlock state that is reachable from q⋆
i ∈Qcommit.
Note that the distance between the configurations of the two states is:
disti = |γc
Y(q⋆
i ) −γc
Y(δc−1(q⋆
dead,i))|.
The final step is to correlate each unique region Ri to the environment proposition assignments prevented by the
safety assumption revisions ψe
t . Those prevented assignments are given in the formula ψ2(q⋆
dead,i). That is, the added
Dynamics-Based Reactive Synthesis and Automated Revisions
20
environment assumptions prevent the environment from triggering the combination ψ2(q⋆
dead,i). The data provided to the
user is represented by the triple (Ri, disti, ψ2(q⋆
dead,i)). The triple can be displayed to the user as follows: “If the robot is
within disti of workspace region Ri, then the generated deadlock revisions (for a given counterstrategy) will be satisfied
if the environment is not set to ψ2(q⋆
dead,i).” Note that this metric supplies a sufficient but not necessary condition for
satisfying the revisions. That is, there might be executions where the system enters within disti with any environment
setting yet still be able to satisfy the revision formulas.
Example 6. In the result of Example 4, let qdead be the deadlock state computed by the counterstrategy corresponding to
the configuration x9, and designate Qcommit = {q1, q2, q3, q4} as the set of commit states for this deadlock. For workspace
region r2, Pdead(r2) = qdead, and Qreach(qi) = qdead for i = 1, . . . , 4. We next determine the pair (q⋆
2, q⋆
dead,2) to be
(q⋆
2, q⋆
dead,2) = arg max
(
 
0
1
!
−
 
0
2
! ,

 
0
0
!
−
 
0
2
! ,

 
1
0
!
−
 
0
2
! ,

 
1
1
!
−
 
0
2
!
)
= (q2, qdead),
where the subscript 2 in the ⋆variables is used to signify the fact that the variables apply to region r2. Assuming η = 1m,
the corresponding distance is dist2 =
√
12 + 22 = 2.2m. Finally, reflective of the revisions in (12)–(19), we note the
subformula ψ2(q⋆
dead,2) = sen.
Therefore, the LTL formulas in (12)–(19) are are summarized as: “If the robot enters to within 2.2m of r2, never set
environment variable sen to True.”
6.4. Summary of the Approach
The approach described in Sections 5.1–6.3 may be combined into an automatic approach for synthesis assisted by user
feedback. We outline this process in Algorithm 2. The approach has three main stages: computing revisions for deadlocks,
composing an explanation of the revisions, and computing revisions for livelocks. Realizability is checked at every iteration
of a while loop, terminating either when a specification is realizable or there are no further revisions to be computed (in
this case, the counterstrategies from one iteration to the next will be identical). Revisions for eliminating deadlock in the
counterstrategy are computed by applying (10) and (11) to the deadlock-committed states Qcommit. If these revisions
falsify the environment and system, they are removed. The second step is to provide feedback to the user. Depending on
the user’s response, the revisions are either applied or discarded.
The third step in the approach is to generate revisions for liveness as computed in (21). Once a candidate liveness
assumption is computed, it is checked in Lines 32–39 to ensure that the system’s strategy does not contain a sequence
of moves that cause the new liveness condition to be falsified. In such cases, realizable returns False, and the candidate
liveness is removed. We refer the reader to Algorithm 5 of Raman & Kress-Gazit (2013) for further details. The user may
elect to accept or discard this formula. Note that, if the specification is unrealizable and the counterstrategy is the same
between iterations of the while loop, this means that no revisions have been found that meet the user’s criteria or do not
falsify the specification. In this case, the algorithm terminates with an unrealizable output.
7. Example
In this section, we demonstrate the revision synthesis approach in an example scenario in which revisions to an unrealizable
task specification are computed and added to the specification based on guidance provided by the user. We generate
abstractions using the Pessoa Toolbox.2 For synthesis, we use the Slugs Synthesis Tool, part of the LTLMoP Toolkit;3 the
code used in this paper may be found at https://github.com/jdc1177/slugs.
2 https://sites.google.com/a/cyphylab.ee.ucla.edu/pessoa/
3 https://github.com/LTLMoP/slugs
Dynamics-Based Reactive Synthesis and Automated Revisions
21
Algorithm 2 Synthesizing revisions for an unrealizable specification ϕabs
procedure synthRevisions(ϕabs)
Initialize ψe
t , ψs
t , ψe
g to True
(realiz, A1
c, MX ) ←ctrStrategy(ϕabs)
A0
c ←False, m ←0
5:
while ¬realiz ∧(Am
c ̸= Am−1
c
) do
▷Step 1: Eliminate deadlocks
Qcommit ←commitStates(Ac)
for all qi
commit ∈Qcommit do
ψe
t,cand, ψe
t ←Eq. (10)
10:
ψs
t,cand, ψs
t ←Eq. (11)
if ¬(ϕe ∧ϕa
t ∧ψe
g ∧ψe
t ∧ψe
t,cand) or ¬( ˆϕs ∧ψs
t ∧ψs
t,cand) then
ψe
t ←ψe
t \ψe
t,cand
ψs
t ←ψs
t \ψs
t,cand
end if
15:
end for
▷Step 2: User feedback
for all Ri ∈R do
(q⋆
i , q⋆
dead) ←Eq. (23)
disti ←|γc
Y(q⋆) −γc
Y(q⋆
dead)|
20:
print (Ri, disti, ψ2(q⋆
dead,i))
end for
if user accepts deadlock revisions then
ϕmod ←Eq. (6)
(realiz, Am
c , MX ) ←ctrStrategy(ϕmod)
25:
end if
▷Step 3: Eliminate livelocks
Qcut ←{q ∈Qc | ∃v′
x /∈MX (q)}
Pcut ←Eq. (20)
ψe
g,cand, ψe
g ←Eq. (21)
30:
if ¬(ϕe ∧ϕa
t ∧ψe
g ∧ψe
t ∧ψe
g,cand) then
ψe
g ←ψe
g\ψe
g,cand
else
ϕtry ←Eq. (6)
realiz ←realizable(ϕtry)
35:
if ¬realiz then
ψe
g ←ψe
g\ψe
g,cand
▷System falsifies environment liveness
end if
end if
40:
if user accepts livelock revisions then
ϕmod ←Eq. (6)
(realiz, Am
c , MX ) ←ctrStrategy(ϕmod)
end if
m + +
45:
end while
return ϕmod
end procedure
We return to the factory scenario in Example 1 using the workspace in Figure 1. To carry out this task, we select a robot
described by a unicycle model that is governed by the kinematic relationship:
˙x = v cos θ,
˙y = v sin θ,
˙θ = ω,
Dynamics-Based Reactive Synthesis and Automated Revisions
22
where the x and y are the Cartesian displacements in meters, θ is the orientation angle, and v and ω are, respectively, the
forward and angular velocity inputs to the system. The car model is subjected to the constraint where it may only move
with positive forward velocity (it cannot stop). An abstraction is generated for the three-dimensional configuration space
and two-dimensional input space consisting of 2.2 × 106 states, with the chosen values η = 0.15, µ = 0.2, τ = 0.35.
The general specification is realizable, producing the controller pictured in Figure 7; however the specification ϕabs
(with respect to the unicycle model) is unrealizable. With the approach in Algorithm 2, we compose revisions that render
ϕmod realizable. After a counterstrategy is synthesized, revisions are found for a total of 2040 states in the counterstrategy
(taking 1020 seconds to synthesize on a laptop PC with a dual-core processor and 8GB memory). A metric for these
revisions is generated and the user is prompted with the following:
Deadlock revisions found.
When within 1.32 m of station_1, never set environment variable s1_occupied to True.
Accept? (y/n)
Note that, as our configuration space consists of variables of mixed units, the norm computed in (23) has been projected
onto the Cartesian plane. A second prompt is given:
When within 1.44 meters of station_2, never set environment variable s2_occupied to True.
Accept? (y/n)
At this point, should the user accept both revisions, a new counterstrategy is synthesized containing no deadlock states.
The user is prompted again:
Livelock revisions found.
Accept? (y/n)
This time, the specification is realizable if the user accepts and the resulting execution for the controller is as shown in
Figure 8. The trajectories pictured in the figure represent evolutions of the continuous nonlinear system when commanded
by the synthesized controller. Forward integration is applied to solve the equations of motion using an integration step size
of 0.001 sec. Here ε = 0.3, and the regions are inflated to the extent indicated by the gray border. Note that the system in
the figure infinitely often visits the three regions and is able to react to a change in the environment. In Figure 8a, the system
avoids the region station_1 when s1_occupied becomes True, since this does not happen within 1.32 m of station_1. A
similar result is seen in Figure 8b. These behaviors are consistent with the intended behaviors encoded by the specification
in Example 1.
Fig. 7. Controller for ϕ in Example 1. Edges are labeled with the disjunction of assignments in X that may be assumed for that transition.
Dynamics-Based Reactive Synthesis and Automated Revisions
23
(a)
(b)
Fig. 8. Continuous trajectories for the nonlinear unicycle abstraction in a 5 × 5 workspace, initialized at the lower-left corner of the
workspace. Regions station_1, station_2 and stockroom are shown in green, red, and blue, respectively. Dots along the trajectory
indicate position at each discrete time step (0.35 seconds). Color indicates the state of the environment (red: s1_occupied; blue:
s2_occupied). (a) shows a trajectory when the s1_occupied sensor is activated. (b) shows a trajectory when the s2_occupied sensor is
activated.
8. Conclusions
In this paper, we have described an automatic approach for synthesizing controllers for dynamical systems based on general
specifications that are agnostic to the dynamics. We focus on the case where such specifications are transformed based on
the discrete abstraction for a particular robot, and develop a framework for revising the specification in the case when the
dynamics render the task unrealizable. We introduce a method for automatically generating a set of LTL formulas that,
when added to the original specification, render it realizable. The approach features a mechanism for providing feedback
to the user, giving him or her the freedom to accept or reject any such proposed formula. To facilitate interpretation of such
formulas, the feedback given to the user is metric information that encapulates the required restrictions on the environment
and system behaviors due to the suggested revisions. Future work includes providing a means for suggesting a richer set
of possible revisions to give as feedback to the user, thereby offering him or her a multiplicity of possible options to apply
(e.g. trading off modifying the robot’s behavior vs. restricting the environment). Such an extension will involve mining
more complex formulas from the synthesis game and automatically translating such formulas into easy-to-understand
explanations.
Acknowledgement
The authors thank Salar Moarref, Ufuk Topcu, and Rajeev Alur for insightful discussions relating to synthesis of
counterstrategy-based environment revisions.
References
R. Alur, et al. (2013). ‘Counter-strategy guided refinement of GR(1) temporal logic specifications’. In Formal Methods in Computer-Aided
Design (FMCAD 2013), pp. 26–33.
Dynamics-Based Reactive Synthesis and Automated Revisions
24
D. Angeli & E. D. Sontag (1999). ‘Forward completeness, unboundedness observability, and their Lyapunov characterizations’. Systems
& Control Letters 38(4):209–217.
A. Bhatia, et al. (2010). ‘Sampling-based motion planning with temporal goals’. In IEEE International Conference on Robotics and
Automation (ICRA 2010), pp. 2689–2696. IEEE.
R. Bloem, et al. (2012). ‘Synthesis of reactive (1) designs’. Journal of Computer and System Sciences 78(3):911–938.
J. DeCastro & H. Kress-Gazit (2014). ‘Synthesis of Nonlinear Continuous Controllers for Verifiably-Correct High-Level, Reactive
Behaviors’. International Journal of Robotics Research Accepted.
G. E. Fainekos (2011). ‘Revising Temporal Logic Specifications for Motion Planning’. In Proceedings of the IEEE Conference on
Robotics and Automation.
G. E. Fainekos, et al. (2009). ‘Temporal logic motion planning for dynamic robots’. Automatica 45(2):343 – 352.
G. E. Fainekos, et al. (2006). ‘Translating Temporal Logic to Controller Specifications’. In Proc. of the 45th IEEE Conf. on Decision
and Control (CDC 2006), pp. 899–904.
G. E. Fainekos & G. J. Pappas (2009). ‘Robustness of temporal logic specifications for continuous-time signals’. Theoretical Computer
Science 410(42):4262–4291.
A. Girard, et al. (2010). ‘Approximately bisimilar symbolic models for incrementally stable switched systems’. Automatic Control, IEEE
Transactions on 55(1):116–126.
M. Kloetzer & C. Belta (2008). ‘Dealing with Nondeterminism in Symbolic Control’. In M. Egerstedt & B. Mishra (eds.), Hybrid
Systems: Computation and Control, 11th International Workshop (HSCC 2008), vol. 4981 of Lecture Notes in Computer Science, pp.
287–300. Springer.
R. Könighofer, et al. (2009). ‘Debugging formal specifications using simple counterstrategies’. In Proceedings of 9th International
Conference on Formal Methods in Computer-Aided Design, FMCAD 2009, pp. 152–159.
H. Kress-Gazit, et al. (2009). ‘Temporal Logic based Reactive Mission and Motion Planning’. IEEE Transactions on Robotics 25(6):1370–
1381.
H. Kress-Gazit, et al. (2011). ‘Correct, Reactive Robot Control from Abstraction and Temporal Logic Specifications’. Special Issue of
the IEEE Robotics and Automation Magazine on Formal Methods for Robotics and Automation 18(3):65–74.
W. Li, et al. (2011). ‘Mining assumptions for synthesis’. In 9th IEEE/ACM International Conference on Formal Methods and Models
for Codesign, MEMOCODE 2011, pp. 43–50.
W. Li, et al. (2014). ‘Synthesis for Human-in-the-Loop Control Systems’. In Tools and Algorithms for the Construction and Analysis of
Systems - 20th International Conference, TACAS 2014, pp. 470–484.
J. Liu & N. Ozay (2014). ‘Abstraction, Discretization, and Robustness in Temporal Logic Control of Dynamical Systems’. In Proc. of
the 17th Int. Conf. on Hybrid Systems: Computation and Control (HSCC’14) (to appear).
J. Liu, et al. (2013). ‘Synthesis of Reactive Switching Protocols From Temporal Logic Specifications’. IEEE Trans. Automat. Contr.
58(7):1771–1785.
J. Liu, et al. (2012). ‘Reactive controllers for differentially flat systems with temporal logic constraints’. In Proc. of the 51st IEEE Conf.
on Decision and Control (CDC 2012), pp. 7664–7670.
M. Maly, et al. (2013). ‘Iterative Temporal Motion Planning for Hybrid Systems in Partially Unknown Environments’. In ACM
International Conference on Hybrid Systems: Computation and Control (HSCC), pp. 353–362, Philadelphia, PA, USA. ACM, ACM.
I. M. Mitchell, et al. (2005). ‘A time-dependent Hamilton-Jacobi formulation of reachable sets for continuous dynamic games.’. IEEE
Trans. Automat. Contr. 50(7):947–957.
G. Pola, et al. (2008). ‘Approximately bisimilar symbolic models for nonlinear control systems’. Automatica 44(10):2508–2516.
V. Raman & H. Kress-Gazit (2013). ‘Explaining Impossible High-Level Robot Behaviors’. IEEE Transactions on Robotics 29(1):94–104.
V. Raman & H. Kress-Gazit (2013). ‘Towards Minimal Explanations of Unsynthesizability for High-Level Robot Behaviors’. In Proc.
of the IEEE/RSJ Int. Conf. on Intelligent Robots and Systems (IROS 2013).
G. Reißig (2011). ‘Computing abstractions of nonlinear systems’. IEEE Transactions on Automatic Control 56(11):2583–2598.
Dynamics-Based Reactive Synthesis and Automated Revisions
25
P. Tabuada & G. J. Pappas (2006). ‘Linear Time Logic Control of Discrete-Time Linear Systems’. IEEE Trans. Automat. Contr.
51(12):1862–1877.
C. J. Tomlin, et al. (2000). ‘A Game Theoretic Approach to Controller Design for Hybrid Systems’. Proceedings of IEEE 88:949–969.
J. Tumova, et al. (2010). ‘A symbolic approach to controlling piecewise affine systems’. In 49th IEEE Conference on Decision and
Control (CDC), pp. 4230 –4235.
M. Y. Vardi (1996). ‘An automata-theoretic approach to linear temporal logic’. In Logics for concurrency, pp. 238–266. Springer.
E. M. Wolff, et al. (2013). ‘Automaton-Guided Controller Synthesis for Nonlinear Systems with Temporal Logic’. In Proc. of the
IEEE/RSJ Int. Conf. on Intelligent Robots and Systems (IROS 2013).
T. Wongpiromsarn, et al. (2010). ‘Receding Horizon Control for Temporal Logic Specifications’. In Proc. of the 13th Int. Conf. on Hybrid
Systems: Computation and Control (HSCC’10).
B. Yordanov, et al. (2012). ‘Temporal Logic Control of Discrete-Time Piecewise Affine Systems’. Automatic Control, IEEE Transactions
on 57(6):1491–1504.
M. Zamani, et al. (2012). ‘Symbolic models for nonlinear control systems without stability assumptions’. IEEE Transactions on Automatic
Control 57(7):1804–1809.
Dynamics-Based Reactive Synthesis and Automated Revisions
for High-Level Robot Control
Jonathan A. DeCastro ∗†
Sibley School of Mechanical and Aerospace Engineering, Cornell University, Ithaca, NY 14853, USA
Rüdiger Ehlers
Department of Computer Science, University of Bremen, 28359 Bremen, Germany
Matthias Rungger
Department of Electrical Engineering and Information Technology, Technical University of Munich,
80333 Munich, Germany
Ayça Balkan and Paulo Tabuada
Electrical Engineering Department, University of California, Los Angeles, Los Angeles, CA 90095,
USA
Hadas Kress-Gazit
Sibley School of Mechanical and Aerospace Engineering, Cornell University, Ithaca, NY 14853, USA
Abstract
The aim of this work is to address issues where formal specifications cannot be realized on a given dynamical system
subjected to a changing environment. Such failures occur whenever the dynamics of the system restrict the robot in such
a way that the environment may prevent the robot from progressing safely to its goals. We provide a framework that
automatically synthesizes revisions to such specifications that restrict the assumed behaviors of the environment and the
behaviors of the system. We provide a means for explaining such modifications to the user in a concise, easy-to-understand
manner. Integral to the framework is a new algorithm for synthesizing controllers for reactive specifications that include
a discrete representation of the robot’s dynamics. The new approach is demonstrated with a complex task implemented
using a unicycle model.
∗This work was supported by the NSF Expeditions in Computing project ExCAPE: Expeditions in Computer Augmented Program Engineering [grant
number CCF-1138996].
† Corresponding author; e-mail: jad455@cornell.edu
arXiv:1410.6375v2  [cs.RO]  13 Jan 2016
Dynamics-Based Reactive Synthesis and Automated Revisions
2
1. Introduction
One of the benefits of the formal methods approach to robot mission planning is that it frees users from the burdens
of programming controllers for complicated robot tasks, removing the arduous step of re-validation every time the task
changes; see, e.g. Kloetzer & Belta (2008), Kress-Gazit et al. (2009), Tabuada & Pappas (2006), Wolff et al. (2013),
Wongpiromsarn et al. (2010). Application of provably-correct controllers on fielded systems requires that the correctness
guarantees extend to a possibly complex set of dynamics describing the robot. Recently, tools have been proposed for
generating discrete abstractions for a wide class of nonlinear systems, e.g. Girard et al. (2010), Pola et al. (2008), Reißig
(2011), Zamani et al. (2012). It is natural to exploit such abstractions when synthesizing controllers that are applicable to
complex physical systems. This paper serves to solidify such a synthesis approach.
When composing tasks for applications such as self-driving cars, household robots, and disaster response robots, the user
must specify both the desired system behaviors and any assumptions on the sensed environment. Often, such assumptions
incorporate knowledge of the behavior of humans and other elements in the robot’s physical surroundings. If any of these
assumptions conflict with the specified task in the context of a robot’s dynamics, the specification is considered to be
unrealizable. That is to say, the environment is allowed to work against fulfilment of the specification by the robot assigned
to the task. As the underlying cause for unrealizability is often difficult to determine, automated frameworks for debugging
specifications (Könighofer et al. (2009), Raman & Kress-Gazit (2013)) and generating environment assumptions (Alur
et al. (2013), Fainekos (2011), Li et al. (2011)) have gained attention recently.
This paper seeks to address the problem of realizability of specifications for robots with dynamics by introducing a
novel framework that automatically suggests additions to the specification to resolve unrealizability issues. We do so by
introducing a new synthesis approach that takes a specification agnostic to the dynamics of the robot, and synthesizes a
controller (if possible) for a specific robot, given its discrete abstraction. If it turns out that the specification is unrealizable,
we automatically generate revisions to the specification that render the task realizable with respect to the robot dynamics.
These formulas effectively alter the environment assumptions and robot behaviors. The drawback of generating revisions
independently of the user is that the resulting specifications may fail to capture the original intent of the mission. We
address this by advocating for an means explaining such revisions in a manner that is simple to understand, permitting user
interaction as the revisions are computed.
When considering dynamics, unrealizability can arise as a result of unwanted effects such as overshooting into undesired
regions or an inability to make progress toward goals. Take the following scenario where rooms A and B are separated by
a door:
Visit rooms A and B. Avoid the door if it is closed. Assume that, infinitely often, the door is open.
In the above scenario, the robot must be able to robustly avoid the walls of the workspace (boundaries) and appropriately
react to the door as it opens and closes. If one applies this specification to robot with inertia, the task could fail because
the robot may not be able to stop by the time the door closes, violating the statement “Avoid the door if it is closed.” By
leveraging both the system dynamics and the specification, we could recover by adding the environment assumption “The
door must not close if within 1 meter of it.” In this paper, we explore an automated method for suggesting such revisions.
The remainder of this paper is outlined as follows. In Section 2, we review relevant formal definitions and notation. We
formally state the problem in Section 3, and address related work in the context of the problem in Section 4. In Section 5,
we describe our approach for synthesis for specifications involving discrete abstractions. We present the approach for
generating formulas and user feedback in Section 6. Next, we demonstrate our approach for a complex task carried out by
an abstraction of a unicycle robot model in Section 7. Lastly, we provide a summary in Section 8.
Dynamics-Based Reactive Synthesis and Automated Revisions
3
2. Preliminaries
2.1. Linear Temporal Logic
Linear temporal logic (LTL) formulas are defined over the set AP of atomic propositions in the recursive grammar:
ϕ ::= true | π | ϕ1 ∧ϕ2 | ¬ϕ | ⃝ϕ | ϕ1Uϕ2
where π is an atomic proposition in AP. Respectively, ∧and ¬ are the Boolean operators “conjunction” and “negation”,
and ⃝and U are the temporal operators “next” and “until”. From these operators, the following operators are derived:
“disjunction” ∨, “implication” ⇒, “equivalence” ⇔, “always” □, and “eventually”
□
.
AP consists of a set of environment propositions X describing the state of the discretized robot sensor values and a
set of system propositions Y describing the current pose of the robot in the workspace. For a set of propositions X, let
⃝X = {⃝πi}πi∈X be the set of propositions with the “next” operator. The LTL formulas are evaluated over infinite
sequences σ = σ0σ1σ2 . . . of truth assignments to the propositions in AP. σ is said to satisfy ⃝ϕ, □ϕ, or
□
ϕ if ϕ holds
true in the next position in the sequence, every position, or at some future position(s), respectively. We refer the reader to
Vardi (1996) for a complete definition of the syntax and semantics of LTL formulas.
Definition 1 (Robot Mission Specification). The specifications we consider are LTL formulas of the form:
ϕ := (ϕe
i ∧ϕe
t ∧ϕe
g)
|
{z
}
ϕe
=⇒(ϕs
i ∧ϕs
t ∧ϕs
g)
|
{z
}
ϕs
The formulas ϕα
i , ϕα
t , and ϕα
g are defined over AP, where ϕα
i are formulas for the initial conditions, ϕα
t the allowed
transitions (safety conditions) to be satisfied always, ϕα
g the goals (liveness conditions) to be satisfied infinitely often, and
α = {e, s} (with e for ‘environment’ and s for ‘system’). The liveness guarantees take the form V
i∈Iα □
□
(Bα
i ), where
Iα is the index set of environment goals (Be
i ) or system goals (Be
i ).
Definition
2
(Controller
Strategy
and
Execution). Define
a
controller
as
a
finite-state
machine
A
=
(S, S0, X, Y, δ, γX , γY), where S is the set of controller states, S0 ⊆S is the set of initial controller states, X and Y
are sets of propositions described above, δ : S × 2X →S is a state transition relation providing the next state s′ ∈S given
the next state s ∈S and the current value of the environment input z ∈2X , i.e. s′ = δ(s, z), γX : S →2X is a labelling
function mapping controller states to the set of environment propositions evaluating to True for all transitions into that
state, and γY : S →2Y is a labelling function mapping controller states to the set of robot configuration propositions
evaluating to True in that state.
Consider an infinite execution σ of A, where σ = (γX (s0), γY(s0))(γX (s1), γY(s1)), . . . for s0 ∈S0 and si ∈S,
i > 0. ϕ is deemed realizable if there exists a finite-state machine A such that every execution produced by A satisfies ϕ.
That is, at every i ≥0, there exists an assignment of system variables Y for all possible assignments of the environment
variables X such that σ satisfies ϕ. If there exist some environment behaviors on X for which no such A can be found,
then ϕ is unrealizable.
A discrete controller can be synthesized from a specification follows by solving a two-player game played between the
environment and the system, as described in Bloem et al. (2012).
2.2. Synthesis over a Connectivity Graph
A connectivity graph is an undirected graph describing those workspace regions that are accessible and adjacent to one
another.
Dynamics-Based Reactive Synthesis and Automated Revisions
4
Given a bounded configuration space W ⊂Rn, let R = {R1 . . . Rp} represent a set of disjoint regions whose closure
covers W, where the open sets Ri ⊆W. Let Y be the set of propositions representing the workspace regions over which
the topology model will be specified and πi ∈Y denote a region proposition that evaluates to True when the robot is in
Ri ∈R.
Definition 3 (Topology Model). We define the topology model as a formula ϕtop
t
over Y that encodes the allowed next
regions given the current region. This formula is defined as follows:
ϕtop
t
=
^
πi∈Y
□



πi =⇒
_
πj∈Y:
cl(Ri)∩cl(Rj)̸=∅
⃝πj



,
where cl(·) denotes the closure operation on a set. Note that we also enforce mutual exclusion of regions; that is, the robot
is only allowed to occupy one region at a time.
When combining the user specifications ϕe and ϕs with the topological model, we obtain the formula ϕe
=⇒
(ϕs ∧ϕtop
t
) written over AP top = X ∪Y. A controller A is synthesized if ϕe =⇒(ϕs ∧ϕtop
t
) is realizable.
2.3. Synthesis over Robot Abstractions
Our model of the behavior of the robot is a nonlinear differential equation
˙ξ(t) = f(ξ(t), ν(t))
(1)
given by the function f : Rn × Rm →Rn, where ξ(t) is the continuous state of the robot and ν(t) the command input
of the robot at time t ∈R≥0. We use ξx,ν to denote a trajectory of (1) with initial state x and input signal ν. We impose
the usual regularity assumptions on f that imply the existence and uniqueness of solutions of (1). Moreover, we assume
that (1) is forward-complete (its solution is defined for all t ≥0), see e.g. Angeli & Sontag (1999).
We produce an estimate of the divergence of neighboring trajectories to obtain a conservative over-approximation of
the continuous dynamics operating under a sample-and-hold controller framework. Let β : R≥0 × R≥0 →R≥0 be a
continuous function, that satisfies β(0, 0) = 0 and β(·, t) is strictly increasing for every t ∈R≥0. Let us assume that any
pair of trajectories produced by the robot dynamics (1) satisfy
|ξx,ν(t) −ξx′,ν(t)| ≤β(|x −x′|, t),
(2)
with x, x′ ∈Rn, t ∈R≥0 and constant input function ν ∈U. Given that (1) is Lipschitz continuous with constant L, the
function β(r, t) = reLt satisfies (2).
In constructing a discrete abstraction, we follow the approach in Pola et al. (2008), Reißig (2011), Zamani et al. (2012)
for discretizing the bounded configuration space W ⊂Rn and the bounded space of command inputs U ⊂Rm. We denote
[W]η to be the uniform grid on W discretized with resolution η. This grid is defined as follows:
[W]η := {x ∈W | ∃k ∈Zn : x = kη}.
We introduce the discretization parameters τ, η, µ ∈R>0, where η and µ define, respectively, the discretization of the robot
configuration and command input spaces, and τ represents the sampling time.
We next denote a set of configuration propositions Ya describing the robot’s pose, and a set of locomotion command
propositions Ua describing the controlled actions taken by the robot. We assume throughout that Ua consists of purely robot
Dynamics-Based Reactive Synthesis and Automated Revisions
5
locomotion commands; the set can be generalized to capture other robot actions (e.g. wave hand, activate alarm), but this
extension is omitted in this paper.
Definition 4 (Discrete Abstraction). The discrete abstraction Sa(τ, η, µ) is defined by the tuple (Qa, Va, δa, γY
a , γU
a ),
where:
• Qa = [X]η is the set of discretized robot configurations;
• Va = [U]µ is the set of discretized robot locomotion commands;
• δa : Qa × Va →2Qa is a transition relation defined such that, there exists qa, q′
a ∈Qa and va ∈Va, q′
a ∈δa(qa, va)
iff there exists ξx,ν with ν(t) = va, for all x ∈{x0 | |x0 −qa| ≤η/2} and t ∈[0, τ), such that
|q′
a −ξx,ν(τ)| ≤β(η/2, τ) + η/2;
(3)
• γY
a : Qa →Ya labels each discretized configuration with the associated proposition in Ya that evaluates to True
when the robot is in the given configuration;
• γU
a : Va →Ua labels each discretized command with the associated proposition in Ua that evaluates to True when
the given command is active.
Additionally, we define γa : R →2Ya, a labelling function associating each region to a set of configuration propositions,
as γa(Rj) = {γY
a (qa) | qa ∈[Rj]η}. Finally, we encode the transitions δa as a safety formula ϕa
t defined over Ya ∪⃝Ua ∪
⃝Ya of the form
ϕa
t =
^
γY
a (qa)∈Ya
γU
a (va)∈Ua
□





γY
a (qa) ∧⃝γU
a (va)


=⇒
_
γY
a (q′
a)∈Ya:
q′
a∈δa(qa,va)
⃝γY
a (q′
a)




.
Suppose Ya = {π0, π1, π2}, Ua = {πfwd} and we start at grid cell π0 at q0. Assume that the set of possible successor
configurations under this command consists of cells 1 and 2; i.e. δa(q0, v0) = {q1, q2}, where γY
a (q1) = π1, γY
a (q2) = π2
and γU
a (v0) = πfwd. In this example, we write □((π0 ∧⃝πfwd) =⇒⃝(π1 ∨π2)) as the corresponding safety formula.
2.4. Ensuring Correctness of the Continuous Behaviors
In the following, we briefly review the rules derived in Fainekos et al. (2009), Fainekos & Pappas (2009), Liu & Ozay
(2014), Liu et al. (2012) for modifying LTL formulas ϕe, ϕs on AP top to account for the behaviors of the continuous
system in between sampling instants. Given the system (1), there exists a constant b ∈R≥0 such that for all ξ(t) ∈W,
u ∈U and t ∈[0, τ), we have
|f(ξ(t), u)| ≤b.
(4)
Through the process of inflation and deflation of physical workspace regions R, we obtain the Sa-strengthened formulas
ˆϕe and ˆϕs. Conservative under-approximations ˇRε
i (where regions are deflated or shrunk) and over-approximations ˆRε
i
(where regions are inflated) may be constructed as follows:
ˇRε
i = {x ∈Rn | {x} + εB ⊆Ri}
ˆRε
i = {x ∈Rn | x ∈Ri + εB}.
Here we use + to denote the Minkowski set addition and B to denote the closed ball in Rn with respect to the infinity norm
| · | with radius τb. Supposing that the formulas ϕe, ϕs are in negated normal form, i.e., the negation only appears in front
Dynamics-Based Reactive Synthesis and Automated Revisions
6
of atomic propositions, we define the Sa-strengthened formulas ˆϕe, ˆϕs by
ˆϕα = ϕα[¬πtop,i/¬γa( ˆRε
i ), πtop,i/γa( ˇRε
i )],
(5)
in which we are replacing the region propositions πtop,i ∈Y with γa( ˇRε
i ) and ¬πtop,i with ¬γa( ˆRε
i ).
By application of Theorem 1 of Liu & Ozay (2014) to the semantics in Fainekos et al. (2009), it is shown that, by
choosing ε ≥bτ, we are assured that the continuous trajectory of (1) satisfies (ϕe ∧ϕa
t ) =⇒ϕs if the sampled-time
execution satisfies ( ˆϕe ∧ϕa
t ) =⇒ˆϕs.
Similar to Liu et al. (2013), we treat the possible non-determinism in the abstraction as adversarial: at each time-step,
the environment assigns values to the environment X. Then, the locomotion command is updated based on this input, and
the abstraction chooses potential successor states to transition into given the current locomotion command. We therefore
treat ϕa
t as a statement on the environment and adopt the formula ( ˆϕe ∧ϕa
t ) =⇒
ˆϕs over AP = X ∪Ya ∪Ua. We
describe in Section 5 our procedure for checking realizability for this formula.
The synthesis of a discrete controller ASa given the formula ϕe =⇒(ϕs ∧ϕtop
t
) and an abstraction Sa involves the
following steps: (1) computation of the formula ϕa
t from Sa (Section 2.3); (2) computation of the Sa-strengthened formulas
ˆϕe, ˆϕs from the original formulas ϕe, ϕs (Section 2.4); and (3) extracting a strategy as is discussed in Section 5.
3. Problem Formulation
Let ϕ be a realizable formula, defined as
ϕ := ϕe =⇒(ϕs ∧ϕtop
t
),
in the set of atomic propositions AP top under the assumption of a topological model ϕtop
t
, where the formulas ϕe and
ϕs are, respectively, the user-defined environment assumptions and system guarantees. Additionally, we require that ϕe is
not falsified by robot behaviors satisfying ϕs (i.e. no trivial behaviors). We refer to ϕ as a general formula. The goal is to
synthesize controllers for such specifications.
Problem 1 (Synthesis under non-deterministic abstractions). Given the subformula ϕa
t for the robot abstraction and the
Sa-strengthened formulas ˆϕe and ˆϕs, synthesize a controller for the robot-specific specification
ϕabs := ( ˆϕe ∧ϕa
t ) =⇒ˆϕs.
in the set of propositions AP.
If ϕabs is unrealizable, determine a set of revisions to the specification that render the new specification realizable. A
revision is a temporal logic formula that may be conjuncted with the original formula. Recall ϕabs is unrealizable if there
exists some environment behavior admissible by the formula ˆϕe ∧ϕa
t such that no system behaviors satisfy ˆϕs.
Problem 2 (Generating revisions). Given a realizable ϕ, an unrealizable ϕabs, an abstraction Sa, and the Sa-strengthened
formulas ˆϕe and ˆϕs, automatically derive a set of formulas for the environment and the system such that
ϕmod := ( ˆϕe ∧ϕa
t ∧ψe
g ∧ψe
t ) =⇒( ˆϕs ∧ψs
t )
(6)
is realizable and ˆϕe ∧ϕa
t ∧ψe
g ∧ψe
t and ˆϕs ∧ψs
t are satisfiable.
If such formulas exist, the user is provided with a suggested liveness assumption ψe
g and suggested set of safety assump-
tions and guarantees, ψe
t and ψs
t , respectively. For each transition formula, a simple-to-interpret statement summarizing
each suggested revision is provided to the user. To illustrate the problem, consider the following example.
Dynamics-Based Reactive Synthesis and Automated Revisions
7
Example 1. Consider a robot tasked with fetching parts in a factory setting, illustrated in Figure 1. Here, stockroom,
station_1 and station_2 are regions in the workspace belonging to Y and s1_occupied and s2_occupied are sensors
belonging to X indicating when the respective region is occupied. The robot is required to visit the stockroom and the two
workstations (system liveness) but avoid visiting those that are occupied (system safety). If the robot is within a workstation,
the environment is required to keep that station unoccupied (environment safety). Also, the workstations are required to
infinitely often be unoccupied (environment liveness).
The general specification ϕ is as follows:
□
□
stockroom ∧□
□
station_1 ∧□
□
station_2
◁sys liveness
□
□
¬s1_occupied ∧□
□
¬s2_occupied
◁env liveness
□(s1_occupied =⇒⃝¬station_1)
◁sys safety
□(s2_occupied =⇒⃝¬station_2)
◁sys safety
□(station_1 =⇒¬s1_occupied)
◁env safety
□(station_2 =⇒¬s2_occupied)
◁env safety
The specification ϕ is realizable. Suppose now we are given a fully-actuated planar robot governed by inertia, described
by the system
¨x = u
¨y = v,
(7)
where (u, v) ∈U are robot commands and (x, y) ∈R2 are the Cartesian robot coordinates. We derive an abstraction Sa of
these dynamics in the configuration space (x, y, ˙x, ˙y) ∈W and obtain the formula ϕabs. With Sa, we want to synthesize
a realizable controller for ϕabs that satisfies the task given an abstraction of these dynamics, with additional restrictions
placed on the behaviors of the environment and the system.
Fig. 1. Resupply example.
Unrealizability can arise from a number of possible causes. One possibility is that the robot’s inertia may prevent it
from avoiding collisions with either one of the workstations upon sensing that it is occupied. Consider the case where
s1_occupied is False and the robot is moving toward station_1. Suppose that, when moving, the robot must pass through
two grid cells to decelerate to a stop. Then, the specification is unrealizable if s1_occupied is allowed to become True
Dynamics-Based Reactive Synthesis and Automated Revisions
8
when the robot is within two grid cells of station_1. This is an example of a deadlock behavior; the environment can force
the system into certain states that have no legal transitions.
Another possibility is that the environment may toggle between states infinitely often, preventing the physical robot
from making progress toward its goals. For instance, suppose the robot is approaching station_1 or station_2 and the
environment toggles the values of s1_occupied and s2_occupied infinitely often. The robot in this case will be always
changing directions, but unable to reach any of its goals before the environment changes once again. This is an example of
a livelock behavior; the robot is prevented from reaching its goals as a result of repeating sequence of environment inputs.
The behavior does not exist in the general formula because the topology graph always allows the robot to either remain in
place or transit to an adjacent region once the environment has moved.
4. Related Work
We present a method that finds appropriate revisions to a specification when the inclusion of discrete abstractions cause
unrealizability of specifications. Our work intersects with two lines of research: synthesis with dynamics, and assumption
mining for reactive synthesis. We address related work in both of these areas below.
Synthesis with Dynamics. Tomlin et al. (2000) were among the first to generate verified controllers preserving safety
and reachability specifications for nonlinear dynamical systems. In their approach, controllers are constructed by posing
the problem as a differential game in hybrid systems (systems with mixed continuous and discrete states) analysis. The
work of Mitchell et al. (2005) made such “reach-avoid” problems tractable through viscosity solutions to time-dependent
partial differential equations.
Progress has been made more recently in developing techniques for synthesis of controllers satisfying specifications with
more expressive requirements than reachability and safety. Namely, Kress-Gazit et al. (2009, 2011) introduce algorithms
for reactive synthesis that take advantage of the bisimulation property allowing high-level controllers to be synthesized
separately from the robot-specific low-level controllers. In order to bridge the gap between the high- and low-levels of
abstraction, tools for automatically synthesizing controllers in the continuous domain based on high-level specifications
have been introduced recently in DeCastro & Kress-Gazit (2014), Fainekos et al. (2006). Bhatia et al. (2010), Maly et al.
(2013) have solved this problem using multi-layered synthesis approaches, where certain parts of the control strategy are
left open for an online planner to complete at runtime.
Another perspective has been to incorporate the dynamics directly into the reactive synthesis process. Rather than
having an additional step for synthesizing continuous controllers that adhere to the behaviors of high-level controller, Liu
et al. (2013) introduce a discrete abstraction of the underlying dynamics (Girard et al. (2010), Reißig (2011), Zamani et al.
(2012)) directly into the synthesis process. The problem of synthesizing controllers using abstractions of physical systems
is well-studied: in provably-correct mission planning, researchers have considered robot dynamics ranging from simple
single or double integrators (Fainekos et al. (2009), Kress-Gazit et al. (2009)) and piecewise linear models (Tumova et al.
(2010), Yordanov et al. (2012)) to nonlinear (Bhatia et al. (2010), Girard et al. (2010), Wolff et al. (2013), Wongpiromsarn
et al. (2010), Zamani et al. (2012)), switched (Liu et al. (2013)) and hybrid systems (Maly et al. (2013)). In Kloetzer & Belta
(2008), non-deterministic abstractions are used to synthesize non-reactive LTL formulas using model checking methods.
LTL synthesis for switched systems was considered in Liu & Ozay (2014), Liu et al. (2013), where the authors propose
methods for computing fine-grained abstractions and switching protocol synthesis for reactive tasks. Our work is inspired
by the nonlinear synthesis methods of Liu et al. (2013), Pola et al. (2008), Zamani et al. (2012). Where our approach differs
is that our synthesis algorithm takes specifications written agnostic to the robot and produces controllers that are applicable
to a given robot platform, given its discrete abstraction. We furthermore explore the case when the dynamics contribute to
the unrealizability of such specifications and supply revisions in such cases.
Dynamics-Based Reactive Synthesis and Automated Revisions
9
Assumption Mining. Unrealizable specifications that are complicated to parse greatly benefit from automated tools
for computing revisions that restrict the environment and system behaviors. Our approach for computing such revisions is
closely related to recent methods described in Fainekos (2011), Li et al. (2011), and Alur et al. (2013). In Fainekos (2011),
a method is devised for determining the cause of unrealizability for non-reactive tasks and providing specification recom-
mendations to the user. In the reactive setting, Li et al. (2011) present a debugging method for unrealizable specifications
based on templates (LTL formulas) mined from an environment counterstrategy. In essence, a counterstrategy captures the
possible behaviors for the environment for which there are no safe system moves that allow it to fulfill its goals. The method
in Alur et al. (2013) generates templates of the form “
□
” and “
□
□” automatically from the counterstrategy, yielding
additional safety and liveness environment statements that remove all execution traces of the counterstrategy. The work
of Li et al. (2014) apply the counterstrategy-based environment assumption mining technique to an early warning system in
human-in-the-loop control systems, demonstrated in an autonomous driving scenario. By removing the behaviors present
in the counterstrategy, the modified environment is restricted in such a way as to permit the system to realize its goals under
the strengthened assumptions, but can sometimes lead to specifications that no longer match the user’s intent.
Finding specific portions of the counterstrategy that lead to unrealizability is in general difficult without additional
information or without post-processing the counterstrategy. Raman & Kress-Gazit (2013) developed algorithms to extract
cores (minimal LTL formulas) for explaining unrealizable specifications. Similar to their work, we aim to identify two types
of counterstrategy behaviors: deadlock and livelock. Where the authors use an “unrolling depth” to discover counterstrategy
states leading to livelock (a cycle of environment inputs locking the robot away from its goals), we apply a similar notion
to finding states leading to deadlock (a counterstrategy state where no further system transitions exist).
Our approach differs from existing works in several other ways. First, we adopt different strategy than Alur et al.
(2013), Li et al. (2011) for computing revisions, that depends on whether deadlock or livelock is being removed from
the counterstrategy. Second, we devise a means for efficiently computing revisions that reduces the number of times a
counterstrategy needs to be synthesized. Lastly, we explain the revisions in a simple-to-understand manner. For example,
the user will be provided with feedback in a structured format: “The specification is realizable as long as a person is not
present when the robot is within 2 meters of the Hallway.”
5. Reactive Synthesis Under Nondeterministic Robot Abstractions
We synthesize reactive controllers by solving a two player game carried out between the environment (player 1) and the
system (player 2) using the fixed-point algorithm described in Bloem et al. (2012). As described in this section, we make
modifications to this algorithm in order to accommodate the adversarial nature of the discrete abstraction and preserve
a mapping between ϕ and ϕabs. We also distinguish the expressive properties of the proposed approach with alternative
approaches (e.g. Liu et al. (2013)).
Definition 5 (Controller Strategies for Non-deterministic Discrete Abstractions). A controller in our abstractions-based
paradigm is a non-deterministic finite-state machine ASa = (S, S0, X, Ya, Ua, δ, γX , γY, γU), where S, S0, X, Ya, Ua, and
γX are as described in Definition 2, δ : S × 2X →2S is a state transition relation providing the set of possible states at the
next position in the sequence given the current controller state and the current value of the environment input, γY : S →2Ya
is a labelling function mapping controller states to a set of possible robot configurations evaluating to True for transitions
into that state, and γU : S →2Ua is a labelling function mapping controller states to a set of possible commands in that
state.
Note that each state captures the possibility of non-determinism in the abstraction, obviating the sets-of-sets definition
for γY. The robot configuration may be regarded as being an additional environment input, but differs in that the value
it takes is not defined until the system chooses a control input. We therefore define an execution as a sequence of moves
made by the environment and system, where the environment gets an extra move once the system has moved; in particular
Dynamics-Based Reactive Synthesis and Automated Revisions
10
σ = (γX (s0), γU(s0), γY(s0))(γX (s1), γU(s1), γY(s1)), . . ., where the robot motion at the current position in the sequence
is a result of the environment input and robot command at the same position.
The three-move formulation is in contrast to the two-move formulation of Liu et al. (2013), where the state of the
dynamical system at the current position in the sequence depends on the environment input and command at the previous
position. Recall that, as we require a controller ASa given the general-purpose formula ϕe
=⇒
(ϕs ∧ϕtop
t
), the
three-move formulation allows for there to be a mapping between the subformulas ϕe, ϕs and ˆϕe, ˆϕs. For example, the
safety guarantee ϕs
t = □((person ∧⃝¬person) =⇒⃝¬r1) has no equivalent counterpart ˆϕs
t in the method of Liu
et al. (2013). The reason is that both person and r1 are environment variables, and the fact that the system is required
to move before r1 is decided forces r1 to be delayed to the next position in the execution. The translation is therefore
□((person ∧⃝¬person)
=⇒
⃝⃝¬r1), which is not in GR(1). Our strategy, on the other hand, allows for the
environment to take an additional move after the system has moved, thereby preserving the mapping without delaying
choosing r1 to the next step.
We are able to assert that ϕabs is realizable if, for all positions in the execution and for all possible valuations of the
environment variables X, there exists a command Ua such that all executions of ASa satisfy the specification for all Ya. ϕabs
is unrealizable if there exists some environment behavior(s) such that no Ua can be found for which all robot configurations
yield executions that satisfy the specification.
In order to determine if ϕabs is realizable, our focus on the GR(1) (generalized reactivity (1)) fragment lends to efficient
solutions, as described in Bloem et al. (2012). Solving the GR(1) game is carried out by first introducing a game structure,
defined as follows.
Definition 6 (Game Structure). A game structure is represented by the tuple G = (V, θ, ρe, ρr, ρs, ϕwin), where:
• V = X ∪Ua ∪Ya is the set of proposition valuations representing the position in the game;
• θ ⊆2V is the set of initial positions;
• ρe ⊆2V × 2⃝X is a transition relation defining the set of environment inputs allowed by ϕe
t at the next position
given the proposition values at the current position in the game;
• ρr ⊆2V × 2⃝Ua × 2⃝Ya is a transition relation derived from the robot formula ϕa
t defining the set of allowed robot
configurations at the next position given the command at the next position and the robot configuration at the current
position in the game;
• ρs ⊆2V × 2⃝V is a transition relation defining the set of commands and robot configurations allowed by ϕs
t at the
next position given the proposition values at the current position in the game; and
• ϕwin is the winning condition.
The algorithm in Bloem et al. (2012) proceeds by considering winning positions that satisfy the system and environment
safety transition relations while leading the system toward its goals. With the robot abstraction, we are faced with the
additional step of ensuring that the positions chosen are safe for all possible robot configurations. We therefore begin by
specifying the following enforceable predecessor operator Pre:
JPreWK := {v ∈2V | ∀vx ⊆X, ∃vu ⊆Ua, ∀vy ⊆Ya :
((v, vx) ∈ρe) =⇒[((v, vu, vy) ∈ρr) =⇒
[((v, vx, vu, vy) ∈ρs) ∧((vx, vu, vy) ∈JWK)]]}.
where JϕK denotes the set of positions for which the formula ϕ evaluates to True. Intuitively, the enforceable predecessor
is a set of positions enforcing that, for all environment inputs satisfying the environment transition relation, there exists a
robot command such that all robot configurations bound to the transitions of the abstraction yields behaviors that remain
safe, as long as the successor positions are taken from the set W.
Dynamics-Based Reactive Synthesis and Automated Revisions
11
We next define a set of winning positions Vwin based on the µ-calculus formula Bloem et al. (2012) Vwin =
νW1. V
is∈Is µW2. W
ie∈Ie νW3.Nisie, where Nisie = (Bs
is ∧PreW1) ∨PreW2 ∨(¬Be
ie ∧PreW3) and ν and µ rep-
resent, respectively, the greatest and least fixpoint operators. This formula ensures that there is a move that places the
system strictly closer to one of its goals or one in which the system prevents one of the environment goals. Note that the
control strategy we derive must be consistent with the physical system. The strategy ASa that we extract from the winning
set of positions is therefore preventing from falsifying the discrete abstraction ϕa
t (for example, those in which the robot is
commanded to move to a configuration beyond W) by choosing only those control actions that also satisfy ϕa
t .
5.1. Counterstrategies for Nondeterministic Robot Abstractions
When a specification is unrealizable, one may synthesize a counterstrategy to find a sequence of environment inputs and
robot configurations that prevent the robot from fulfilling its specification.
Definition 7 (Environment Counterstrategies for Non-deterministic Discrete Abstractions). We define an environment
counterstrategy as a finite-state machine Ac = (Qc, Qc
0, X, Ya, Ua, δc, γc
U, γc
X , γc
Y), where
• Qc is the set of counterstrategy states;
• Qc
0 ⊆Qc is the set of initial counterstrategy states;
• X, Ya and Ua are sets of propositions in AP;
• δc : Qc →2Qc is a nondeterministic transition relation returning the set of counterstrategy states at the next position
in the sequence given the current state;
• γc
U : Qc →2Ua is a labelling function mapping counterstrategy states to the set of locomotion command propositions
in Ua evaluating to True for all transitions into that state;
• γc
X : Qc →2X is a labelling function mapping counterstrategy states to the set of environment propositions in X
evaluating to True in that state, and;
• γc
Y : Qc →2Ya is a labelling function mapping counterstrategy states to the set of robot configurations in Ya
evaluating to True in that state.
We furthermore define δc−1 : 2Qc →Qc as the inverse transition relation mapping counterstrategy states to a set of
predecessors; i.e. δc−1(q′) = {q ∈Qc | q′ ∈δc(q)}.
Our approach to synthesizing counterstrategies resembles that of Könighofer et al. (2009), where we use a fixed point
computation to determine realizability of the specification, then extract a strategy Ac from the set of positions that are
winning for player 1. We define the enforceable predecessor operator for the counterstrategy Prec as follows:
JPrecWK := {v ∈2Vc | ∃vx ⊆X, ∀vu ⊆Ua, ∃vy ⊆Ya :
((v, vx) ∈ρe) ∧[[((v, vu, vy) ∈ρr)∧
((v, vx, vu, vy) ∈ρs)] =⇒((vx, vu, vy) ∈JWK)]}.
The set of winning positions Vc
win = X ∪Ua ∪Ya for player 1 may then be computed from the formula Vc
win =
µW1. W
is∈Is νW2. V
ie∈Ie µW3.N c
isie, where
N c
isie = (¬Bs
is ∨PrecW1) ∧PrecW2 ∧(Be
ie ∨PrecW3),
A counterstrategy is synthesized by storing the sets N c
isie for each is and ie at the last pass of the fixed point operation.
Starting at the initial conditions ϕe
i, ϕs
i, for each state we identify an index is of the liveness guarantee that is currently being
prevented by the counterstrategy. At a particular counterstrategy state q, we determine a successor q′ similar to Könighofer
et al. (2009) as follows. First, given the position v at state q, we fix an assignment of inputs v′
x ∈X. We next determine,
Dynamics-Based Reactive Synthesis and Automated Revisions
12
for this fixed assignment, the set of winning configurations v′
y ∈Ya that belong to N c
isie for every v′
u ∈Ua. A check is
made to determine if a liveness assumption has been fulfilled at q; if it has, then a new liveness assumption ie is selected.
For notational convenience, we define the set of successor values winning for player 1 at a counterstrategy state q as
MX (q) = {v′
x ∈X | ∀v′
u ∈Ua, ∃v′
y ∈Ya : (v, v′
x, v′
u, v′
y) ∈N c
is(q)ie(q), v = γc
X (q) ∪γc
U(q) ∪γc
Y(q)}. This set contains
the set of inputs for which there exist command-configuration combinations that are winning for player 1.
6. Generating Revisions to Unrealizable Specifications
In this section, we formalize our solution strategy for Problem 2. In similar fashion to Alur et al. (2013), Li et al. (2011),
we make use of environment counterstrategies in order to search for environment assumptions that render the specification
realizable. Our approach is outlined as follows: (1) from the specification ϕabs, we synthesize counterstrategies; (2) for
each counterstrategy found, we compute environment and system transition subformulas ψe
t and ψs
t that prevent transitions
to states in the counterstrategy from which the robot has no safe transitions (deadlock); (3) if a counterstrategy is found
that is free of deadlock states, we compute liveness assumptions ψe
g that restrict transitions to cycles of states preventing
the robot from fulfilling its goals (livelock). We introduce the following example to illustrate the major concepts discussed
in this section.
Example 2. ConsidertheworkspaceshowninFigure2a.GivenX = {sen}wheresenisthesensorinputandY = {r1, r2},
we write a specification ϕ requiring the robot to visit r2 (lower-left gray region) when s is False, but avoid r2 when sen
is True. Formally:
□
□
r2
◁ϕs
g
□
□
¬sen
◁ϕe
g
□(⃝sen =⇒⃝¬r2)
◁ϕs
t
□(r2 =⇒⃝¬sen)
◁ϕe
t
True
◁ϕs
i
True
◁ϕe
i
The controller satisfying this specification is given in Figure 2b.
Given an abstraction where Ya = {x1, . . . , x16} is an encoding of the set of 2-D robot configurations, and Ua =
{N, S, E, W} are the robot commands for motion in the four cardinal directions, we derive a new specification ϕabs,
where:
□
□
(x9 ∨x13)
◁ˆϕs
g
□
□
¬sen
◁ϕe
g
□(⃝sen =⇒⃝¬(x9 ∨x13))
◁ˆϕs
t
□((x9 ∨x13) =⇒⃝¬sen)
◁ˆϕe
t
True
◁ˆϕs
i
True
◁ˆϕe
i
The abstraction ϕa
t appears as arrows in the figure.
Dynamics-Based Reactive Synthesis and Automated Revisions
13
(a)
(b)
Fig. 2. 2-D example. (a) shows the workspace map and grid whose cells are labeled with the configuration variable. The white grid cells
denote r1, while the gray denote r2. (b) shows the synthesized controller for ϕ.
6.1. Adding Revisions for Preventing Deadlock
To prevent deadlock, we introduce a scheme to process a counterstrategy and extract a set of environment assumptions that
remove deadlock behaviors. Consider a counterstrategy Ac whose deadlock states are collected in Qdead. There exists an
execution that eventually reaches a deadlock state qi
dead; specifically when ∃q′ ∈δc(qi
dead) : q′ = ∅. We formally state
this behavior as W
qj∈δc−1(qi
dead)
□
ψ1(qj) ∧⃝ψ2(qi
dead)


, where ψ1(q) and ψ2(q) are propositional representations for
the subsets of positions at counterstrategy state q:
ψ1(q) =
^
π∈γc
U(q)∪γc
Y(q)
π ∧
^
π∈(Ua∪Ya)\(γc
U(q)∪γc
Y(q))
¬π,
ψ2(q) =
^
π∈γc
X (q)
π ∧
^
π∈X\γcs(q)
¬π.
In words, φ1(q) captures the command and configuration moves at state q, and ψ2(q) captures the environment input at q.
To remove the environment behaviors in the counterstrategy causing deadlock, we adopt the following formula:
^
qj∈δc−1(qi
dead)
□
ψ1(qj) =⇒⃝¬ψ2(qi
dead)


.
(8)
Before conjuncting each computed formula with ψe
t , a check is made to determine if it falsifies the left-hand side of ϕmod,
i.e. there is no transition that satisfies ˆϕe ∧ϕa
t ∧ψe
t . If this is the case, the formula is discarded and it is not included as a
conjunct in ψe
t .
Example 3. Returning to Example 2, suppose we obtain a counterstrategy containing the states q0, q1, q2, q3, q4, as pictured
in Figures 3a and 3b, starting in cell x3 with sen =False. One of the possible executions in this counterstrategy eventually
Dynamics-Based Reactive Synthesis and Automated Revisions
14
leads the robot to cell x4 with the sensor sen =True:
σ = ({∅}, {∅}, {x3}), ({∅}, {W}, {x2}), ({∅}, {W}, {x1}),
({∅}, {S}, {x5}), ({s}, {∅}, {∅}).
where the ith time step corresponds to qi. In this execution, the sensor sen remains False until the robot enters x5, at
which point a transition in ϕs
t is violated. Hence q4 is a deadlock state. The formula
□
(⃝sen ∧¬x1 ∧S)1 is extracted by
evaluating
□
(ψ1(q4)∧⃝ψ2(q4)). The complement of this formula, □((¬x1∧S) =⇒⃝¬sen), is added as an additional
environment assumption. This assumption negates the behaviors in the counterstrategy for that particular deadlock state.
Being that there is only one deadlock state, we add no further assumptions. Upon adding this revision to the environment
assumptions, we determine that the modified specification is realizable.
(a)
(b)
Fig. 3. (a) shows a partial counterstrategy for Example 3 leading to deadlock; (b) shows a corresponding robot trajectory leading to
deadlock, where the green part of the path denotes where sen =False and the red denotes where sen =True. The cells shaded yellow
indicate configurations in which there are no sequence of commands that avoid reaching r2 eventually.
Notice that the controller synthesized in Example 3 produces executions that satisfy the specification but the system now
assumes that the environment will always turn sen False whenever it reaches x5. In the example, consider the behavior
when the robot starts at x7 with sen True. The execution of the robot in this case is
σ = ({sen}, {∅}, {x7}), ({sen}, {W}, {x6}), ({sen}, {W}, {x5}),
({sen}, {S}, {x9}), ({∅}, {E}, {x10}), ({∅}, {N}, {x6}), . . . .
In this execution, sen remains True and, as the robot moves toward r2, the environment eventually must set sen to False
to be consistent with the added assumption. When outside of x5, the robot follows the same sequence of moves regardless
1 We only make the True action explicit (S in this case), since mutual exclusion disallows the other actions from being activated at the same time.
Dynamics-Based Reactive Synthesis and Automated Revisions
15
of the environment. Note that the controller for the original, realizable specification ϕ (Figure 2b) does not exhibit this
behavior because there is no imposition on how the environment must behave based on the robot’s configuration. In that
case, if sen is True, the robot waits in r1 until sen becomes False.
We remove such behaviors by disallowing a system transition whenever the same conditions found for the deadlock
state hold at the state previous to deadlock. The idea is to force the system to react conservatively to the newly-added
environment revision as if it were a deadlock state. Thus, when the robot is at a configuration previous to the deadlock state
and the deadlock conditions hold currently, it will be forbidden from entering the configuration prior to deadlock. On the
other hand, when the environment is not currently producing the same conditions as at deadlock, ψe
t forces the environment
to “play fair” with the robot by not producing those conditions in the next step once the robot has made its move.
Formally, we disallow the behavior W
qj∈δc−1(qi
dead)
□
(⃝¬ψ2(qi
dead) ∧⃝¬ψ1(qj)) by introducing an additional
revision on ϕs
t
^
qj∈δc−1(qi
dead)
□
⃝¬ψ2(qi
dead) =⇒⃝ψ1(qj)


.
(9)
Such a revision places a safety restriction on the robot, preventing it from entering a neighboring state to a deadlock
state whenever the environment is set to the same value for which deadlock occurs. Doing this produces a specification
that makes the system’s behavior conservative; we are strengthening the conditions under which the robot may enter the
neighboring state, when in fact the robot is not in any true danger of violating the original safety guarantees in ϕ until it
reaches r2. Nonetheless, if the specification is realizable, the system will be able to react to the environment as long as the
actions/configurations are not included in those specified in V
qj∈δc−1(qi
dead) ψ1(qj).
If the modified formula is determined to be unrealizable and new deadlock states are found at a state qj ∈δc−1(qi
dead),
then we once again return to the original set of circumstances specified in Problem 2. We repeat the process in this section
for as many times as required to eliminate deadlock states or when the specification is unrealizable. We may, however,
avoid repeated synthesis of counterstrategies by applying the assumption and guarantee revisions explained above to entire
subtraces of a single counterstrategy (a a finite word of an execution trace for the counterstrategy). To do this, we identify
states for which there is no safe command to be taken such that there exists a subtrace that eventually visits states in
Qc\Qdead. The search for deadlock revisions then reduces to a graph search on the counterstrategy, as summarized in
Algorithm 1. The algorithm builds up a set of deadlock-committed states Qcommit by adding, via a breadth-first search
(BFS in line 4), predecessor counterstrategy states from deadlock Qdead for which all locomotion commands lead to states in
Qcommit. For generating revisions and providing user feedback, we also maintain a mapping Qreach : Qcommit →2Qdead
of deadlock states reachable from each q ∈Qcommit. The search continues until a fixed point of states is reached where no
additional deadlock-committed states can be found, at which point BFS returns a tuple containing Qcommit and Qreach.
The precise condition under which the search terminates is when a q ∈Qc is found such that:
∃q′ ∈δc(q) : q′ /∈Qcommit.
Here, Qcommit plays the role of Qdead. We therefore replace Qdead in the safety revisions (8) and (9) with Qcommit. To
be precise, we replace (8) with
^
qj∈Qi
commit
□

ψ1(qj) =⇒
_
qk∈Qreach(qi
commit)
⃝¬ψ2(qk)


(10)
Dynamics-Based Reactive Synthesis and Automated Revisions
16
and (9) with
^
qj∈Qi
commit
□


^
qk∈Qreach(qi
commit)
⃝ψ2(qk) =⇒⃝¬ψ1(qj)



,
(11)
for each qi
commit ∈Qcommit. Consider the example below.
Algorithm 1 Computing deadlock-committed states.
procedure commitStates(Qdead)
Initialize Qnew, Qcommit, Qreach to Qdead
while Qnew ̸= ∅do
(Qnew, Qreach) ←BFS(Ac, Qcommit, Qreach)
5:
Qcommit ←Qcommit ∪Qnew
end while
return Qcommit, Qreach
end procedure
Example 4. Starting from the result of Example 3, we compute a set of four deadlock-commit states Qcommit =
{q1, q2, q3, q4} corresponding to the cells {x6, x2, x1, x5}. We obtain the following ψe
t formulas:
□((x5 ∧S) =⇒⃝¬sen)
(12)
□((x1 ∧S) =⇒⃝¬sen)
(13)
□((x2 ∧W) =⇒⃝¬sen)
(14)
□((x6 ∧N) =⇒⃝¬sen),
(15)
and the following ψs
t formulas:
□(⃝sen =⇒⃝¬(x5 ∧S))
(16)
□(⃝sen =⇒⃝¬(x1 ∧S))
(17)
□(⃝sen =⇒⃝¬(x2 ∧W))
(18)
□(⃝sen =⇒⃝¬(x6 ∧N)).
(19)
With these revisions added to ψe
t and ψs
t (highlighted orange in Figure 4, the modified specification eliminates the deadlock
states present in the original counterstrategy. Additionally, note that none of the revisions falsify the environment.
Upon synthesis, we find that a counterstrategy synthesized from this modified specification does not contain deadlock
states. In the next section, we discuss an approach to render the specification realizable by eliminating livelock behaviors.
6.2. Adding revisions for Preventing Livelock
In cases where the environment satisfies its own liveness conditions, the environment may be allowed to play in such a way
that as the system cycles through an infinite sequence of states, the environment always keeps it away from one of its goals.
Consider the behavior of the robot when the above ψe
t and ψs
t formulas (12)–(19) are introduced as revisions. Starting at
Dynamics-Based Reactive Synthesis and Automated Revisions
17
Fig. 4. Map showing configurations for which the revisions ψe
t and ψs
t from Example 4 apply; a counterstrategy execution trace, as
explained in Section 6.2. The green part of the path denotes where sen =False and the red denotes where sen =True.
x16, the following behavior is possible:
σ = ({∅}, {∅}, {x16}), ({∅}, {N}, {x12}), ({∅}, {N}, {x8}),
({sen}, {W}, {x7}), ({∅}, {S}, {x11}), ({∅}, {S}, {x15}),
({∅}, {E}, {x16}), ({∅}, {N}, {x12}), . . . .
In this execution(shown in Figure 4), the robot eventually cycles indefinitely between six cells in the workspace. Whenever
the robot visits the cell x7, the environment activates sen, forcing the robot to move S to avoid violating the safety guarantee
revision in (19). The environment is then able to satisfy its liveness goal (□
□
(¬sen)), while preventing the robot from
achieving its goal of reaching r2.
Once we obtain a counterstrategy free of deadlock states, we generate environment assumptions that remove the
counterstrategy executions that exhibit livelock. The idea is to selectively choose states in the counterstrategy for which the
robot still has winning actions to take and then apply liveness assumptions at those states to ensure that, always eventually,
the robot is allowed to take these actions. We employ the result of the innermost fixed point computation MX (q) stored
when solving the counterstrategy game to find any states for which there exists an assignment of environment inputs that are
not winning for the environment. Note that, for these inputs, there exists a command the robot may take which is winning
for the system. We then prevent the environment from always making such assignments at these counterstrategy states.
Formally, for all q ∈Qc, our goal is to find a subset Qcut ⊆Qc for which v′
x /∈MX (q), where MX (q) are the set of
environment inputs at a state q ∈Qc that are winning for player 1. Consequently, for any q ∈Qcut there are some v′
x ⊆X
and v′
u ⊆Ua that lead to a position that is not winning for player 1 (i.e. v′
x /∈MX (q)). One can think of Qcut as being those
counterstrategy states where it is possible that the environment has been able to “cut away” a command that will allow the
robot to proceed to its next goal by applying some environment input.
Using Qcut, we formulate a set of liveness assumptions that restrict the environment from always behaving in a manner
that prevents the system’s progress toward its goals. Notice that Qcut contains all states for which there is an environment
and system move not in player 1’s strategy; however, not all such moves are necessarily winning for player 2. For instance,
a state in Qcut could yield an environment input that does not allow player 1 to move strictly closer to its goal yet only
allow system moves that place the system further away from its goal.
We therefore form a set Pcut ⊆Qcut for which the robot has safe commands that are winning for the system. We use
Qcommit (from the deadlock counterstrategy) to define the set of states where there exist system moves that lead the system
Dynamics-Based Reactive Synthesis and Automated Revisions
18
closer to its goals. We populate Pcut as follows:
Pcut = {q ∈Qcut | ∃va ∈Va, ∃q′ ∈Qcommit, ∃qa ∈δa(va, γc
Y(q)) :
∀π ∈Ya, π ∈γY
a (qa) iff π ∈γc
Y(q′)}.
(20)
We then apply the environment liveness assumption
□
□
_
qi∈Pcut

ψ1(qi) ∧
^
qj∈δc(qi,γc
Y(qi))
⃝¬ψ2(qj)

.
(21)
This liveness formula disallows the environment from always behaving in a way that denies the system from taking action
that lead it closer to its goals, when the robot is in a configuration where there is such an action to be taken.
Example 5. With the specification ϕabs in Example 2 along with the revision (12)–(19), a counterstrategy is extracted as
pictured in Figure 6. The set Qcut consists of four states, {q3, q5, q6, q8}. Of these, {q3, q6, q8} are states in which the robot
has an action (move W) taking the robot closer to r2 that the environment can prevent. These are found from Example 3
and are collected in Pcut. We also find state {q5}, for which there is an environment move keeping it from immediately
realizing an environment goal (□
□
(¬sen)) but does not lead the system closer to its goal. We apply environment liveness
revisions ψe
g to the set Pcut:
□
□
((x7 ∧W ∧⃝¬sen) ∨(x3 ∧W ∧⃝¬sen) ∨(x7 ∧S ∧⃝¬sen)) .
(22)
The three above formulas correspond to regions appearing as blue regions in Figure 5. Adding this final revision produces
a specification ϕmod that is realizable.
Fig. 5. Map showing regions associated with cut states from Example 5.
6.3. User Feedback
Before modifying the specification with the computed deadlock revisions, we alert the user of the consequences of these
revisions. Given this information, the user may choose to accept these if they are, in fact, consistent with the original design
intent. We provide feedback in the form of statements such as “Keep sensor sen False if the robot enters to within N
meters of r2” instead of raw LTL formulas.
Dynamics-Based Reactive Synthesis and Automated Revisions
19
Fig. 6. Deadlock-free counterstrategy for Example 5.
For the combined environment and system revisions for deadlock, we use the mapping between cells and regions from
the robot abstraction to assist in forming this metric. For each labeled workspace region Ri ∈R, we mark those deadlock
states (if any exist) from whose predecessors there exists a robot command va ∈Va (Definition 4) to reach Ri. Those
marked deadlock states are collected in the set Pdead(Ri), defined formally as:
Pdead(Ri) = {q ∈Qdead | ∀q′ ∈δc−1(q), ∃va ∈Va, ∃q′
a ∈δa(va, γc
Y(q′)) :
∀π ∈Ya, π ∈γY
a (q′
a) iff π ∈γa(Ri)}.
In the fixed point computation in Algorithm 1, we keep track of each deadlock state reachable from each state added to
Qcommit. We use this stored information to find the distances between each robot configuration in Qcommit. Rather than
provide the user with a detailed set of conditions under which the environment would be required to adhere for the generated
revisions to be satisfied, we advocate for simplicity by computing a conservative upper-bound on robot configurations where
the environment restrictions must hold. For each Ri corresponding to a robot configuration that satisfies some deadlock
state in Qdead, we find the relative proximity to a deadlock condition (in terms of physical coordinates) by finding the
maximal pairwise distance between any states affected by the deadlock revisions:
(q⋆
i , q⋆
dead,i) =
arg max
q∈Qcommit,
q′∈Qreach(q)∩Pdead(Ri)
|γc
Y(q) −γc
Y(δc−1(q′))|.
(23)
Here, |vy| is the Euclidean norm of the real-valued abstraction state qa ∈Qa represented by a set of propositions vy ⊆Ya
that are True in that state. The pair of counterstrategy states q⋆
i and q⋆
dead,i are those corresponding to a revision for region
Ri where the distance is greatest, under the constraint that q⋆
dead,i is a deadlock state that is reachable from q⋆
i ∈Qcommit.
Note that the distance between the configurations of the two states is:
disti = |γc
Y(q⋆
i ) −γc
Y(δc−1(q⋆
dead,i))|.
The final step is to correlate each unique region Ri to the environment proposition assignments prevented by the
safety assumption revisions ψe
t . Those prevented assignments are given in the formula ψ2(q⋆
dead,i). That is, the added
Dynamics-Based Reactive Synthesis and Automated Revisions
20
environment assumptions prevent the environment from triggering the combination ψ2(q⋆
dead,i). The data provided to the
user is represented by the triple (Ri, disti, ψ2(q⋆
dead,i)). The triple can be displayed to the user as follows: “If the robot is
within disti of workspace region Ri, then the generated deadlock revisions (for a given counterstrategy) will be satisfied
if the environment is not set to ψ2(q⋆
dead,i).” Note that this metric supplies a sufficient but not necessary condition for
satisfying the revisions. That is, there might be executions where the system enters within disti with any environment
setting yet still be able to satisfy the revision formulas.
Example 6. In the result of Example 4, let qdead be the deadlock state computed by the counterstrategy corresponding to
the configuration x9, and designate Qcommit = {q1, q2, q3, q4} as the set of commit states for this deadlock. For workspace
region r2, Pdead(r2) = qdead, and Qreach(qi) = qdead for i = 1, . . . , 4. We next determine the pair (q⋆
2, q⋆
dead,2) to be
(q⋆
2, q⋆
dead,2) = arg max
(
 
0
1
!
−
 
0
2
! ,

 
0
0
!
−
 
0
2
! ,

 
1
0
!
−
 
0
2
! ,

 
1
1
!
−
 
0
2
!
)
= (q2, qdead),
where the subscript 2 in the ⋆variables is used to signify the fact that the variables apply to region r2. Assuming η = 1m,
the corresponding distance is dist2 =
√
12 + 22 = 2.2m. Finally, reflective of the revisions in (12)–(19), we note the
subformula ψ2(q⋆
dead,2) = sen.
Therefore, the LTL formulas in (12)–(19) are are summarized as: “If the robot enters to within 2.2m of r2, never set
environment variable sen to True.”
6.4. Summary of the Approach
The approach described in Sections 5.1–6.3 may be combined into an automatic approach for synthesis assisted by user
feedback. We outline this process in Algorithm 2. The approach has three main stages: computing revisions for deadlocks,
composing an explanation of the revisions, and computing revisions for livelocks. Realizability is checked at every iteration
of a while loop, terminating either when a specification is realizable or there are no further revisions to be computed (in
this case, the counterstrategies from one iteration to the next will be identical). Revisions for eliminating deadlock in the
counterstrategy are computed by applying (10) and (11) to the deadlock-committed states Qcommit. If these revisions
falsify the environment and system, they are removed. The second step is to provide feedback to the user. Depending on
the user’s response, the revisions are either applied or discarded.
The third step in the approach is to generate revisions for liveness as computed in (21). Once a candidate liveness
assumption is computed, it is checked in Lines 32–39 to ensure that the system’s strategy does not contain a sequence
of moves that cause the new liveness condition to be falsified. In such cases, realizable returns False, and the candidate
liveness is removed. We refer the reader to Algorithm 5 of Raman & Kress-Gazit (2013) for further details. The user may
elect to accept or discard this formula. Note that, if the specification is unrealizable and the counterstrategy is the same
between iterations of the while loop, this means that no revisions have been found that meet the user’s criteria or do not
falsify the specification. In this case, the algorithm terminates with an unrealizable output.
7. Example
In this section, we demonstrate the revision synthesis approach in an example scenario in which revisions to an unrealizable
task specification are computed and added to the specification based on guidance provided by the user. We generate
abstractions using the Pessoa Toolbox.2 For synthesis, we use the Slugs Synthesis Tool, part of the LTLMoP Toolkit;3 the
code used in this paper may be found at https://github.com/jdc1177/slugs.
2 https://sites.google.com/a/cyphylab.ee.ucla.edu/pessoa/
3 https://github.com/LTLMoP/slugs
Dynamics-Based Reactive Synthesis and Automated Revisions
21
Algorithm 2 Synthesizing revisions for an unrealizable specification ϕabs
procedure synthRevisions(ϕabs)
Initialize ψe
t , ψs
t , ψe
g to True
(realiz, A1
c, MX ) ←ctrStrategy(ϕabs)
A0
c ←False, m ←0
5:
while ¬realiz ∧(Am
c ̸= Am−1
c
) do
▷Step 1: Eliminate deadlocks
Qcommit ←commitStates(Ac)
for all qi
commit ∈Qcommit do
ψe
t,cand, ψe
t ←Eq. (10)
10:
ψs
t,cand, ψs
t ←Eq. (11)
if ¬(ϕe ∧ϕa
t ∧ψe
g ∧ψe
t ∧ψe
t,cand) or ¬( ˆϕs ∧ψs
t ∧ψs
t,cand) then
ψe
t ←ψe
t \ψe
t,cand
ψs
t ←ψs
t \ψs
t,cand
end if
15:
end for
▷Step 2: User feedback
for all Ri ∈R do
(q⋆
i , q⋆
dead) ←Eq. (23)
disti ←|γc
Y(q⋆) −γc
Y(q⋆
dead)|
20:
print (Ri, disti, ψ2(q⋆
dead,i))
end for
if user accepts deadlock revisions then
ϕmod ←Eq. (6)
(realiz, Am
c , MX ) ←ctrStrategy(ϕmod)
25:
end if
▷Step 3: Eliminate livelocks
Qcut ←{q ∈Qc | ∃v′
x /∈MX (q)}
Pcut ←Eq. (20)
ψe
g,cand, ψe
g ←Eq. (21)
30:
if ¬(ϕe ∧ϕa
t ∧ψe
g ∧ψe
t ∧ψe
g,cand) then
ψe
g ←ψe
g\ψe
g,cand
else
ϕtry ←Eq. (6)
realiz ←realizable(ϕtry)
35:
if ¬realiz then
ψe
g ←ψe
g\ψe
g,cand
▷System falsifies environment liveness
end if
end if
40:
if user accepts livelock revisions then
ϕmod ←Eq. (6)
(realiz, Am
c , MX ) ←ctrStrategy(ϕmod)
end if
m + +
45:
end while
return ϕmod
end procedure
We return to the factory scenario in Example 1 using the workspace in Figure 1. To carry out this task, we select a robot
described by a unicycle model that is governed by the kinematic relationship:
˙x = v cos θ,
˙y = v sin θ,
˙θ = ω,
Dynamics-Based Reactive Synthesis and Automated Revisions
22
where the x and y are the Cartesian displacements in meters, θ is the orientation angle, and v and ω are, respectively, the
forward and angular velocity inputs to the system. The car model is subjected to the constraint where it may only move
with positive forward velocity (it cannot stop). An abstraction is generated for the three-dimensional configuration space
and two-dimensional input space consisting of 2.2 × 106 states, with the chosen values η = 0.15, µ = 0.2, τ = 0.35.
The general specification is realizable, producing the controller pictured in Figure 7; however the specification ϕabs
(with respect to the unicycle model) is unrealizable. With the approach in Algorithm 2, we compose revisions that render
ϕmod realizable. After a counterstrategy is synthesized, revisions are found for a total of 2040 states in the counterstrategy
(taking 1020 seconds to synthesize on a laptop PC with a dual-core processor and 8GB memory). A metric for these
revisions is generated and the user is prompted with the following:
Deadlock revisions found.
When within 1.32 m of station_1, never set environment variable s1_occupied to True.
Accept? (y/n)
Note that, as our configuration space consists of variables of mixed units, the norm computed in (23) has been projected
onto the Cartesian plane. A second prompt is given:
When within 1.44 meters of station_2, never set environment variable s2_occupied to True.
Accept? (y/n)
At this point, should the user accept both revisions, a new counterstrategy is synthesized containing no deadlock states.
The user is prompted again:
Livelock revisions found.
Accept? (y/n)
This time, the specification is realizable if the user accepts and the resulting execution for the controller is as shown in
Figure 8. The trajectories pictured in the figure represent evolutions of the continuous nonlinear system when commanded
by the synthesized controller. Forward integration is applied to solve the equations of motion using an integration step size
of 0.001 sec. Here ε = 0.3, and the regions are inflated to the extent indicated by the gray border. Note that the system in
the figure infinitely often visits the three regions and is able to react to a change in the environment. In Figure 8a, the system
avoids the region station_1 when s1_occupied becomes True, since this does not happen within 1.32 m of station_1. A
similar result is seen in Figure 8b. These behaviors are consistent with the intended behaviors encoded by the specification
in Example 1.
Fig. 7. Controller for ϕ in Example 1. Edges are labeled with the disjunction of assignments in X that may be assumed for that transition.
Dynamics-Based Reactive Synthesis and Automated Revisions
23
(a)
(b)
Fig. 8. Continuous trajectories for the nonlinear unicycle abstraction in a 5 × 5 workspace, initialized at the lower-left corner of the
workspace. Regions station_1, station_2 and stockroom are shown in green, red, and blue, respectively. Dots along the trajectory
indicate position at each discrete time step (0.35 seconds). Color indicates the state of the environment (red: s1_occupied; blue:
s2_occupied). (a) shows a trajectory when the s1_occupied sensor is activated. (b) shows a trajectory when the s2_occupied sensor is
activated.
8. Conclusions
In this paper, we have described an automatic approach for synthesizing controllers for dynamical systems based on general
specifications that are agnostic to the dynamics. We focus on the case where such specifications are transformed based on
the discrete abstraction for a particular robot, and develop a framework for revising the specification in the case when the
dynamics render the task unrealizable. We introduce a method for automatically generating a set of LTL formulas that,
when added to the original specification, render it realizable. The approach features a mechanism for providing feedback
to the user, giving him or her the freedom to accept or reject any such proposed formula. To facilitate interpretation of such
formulas, the feedback given to the user is metric information that encapulates the required restrictions on the environment
and system behaviors due to the suggested revisions. Future work includes providing a means for suggesting a richer set
of possible revisions to give as feedback to the user, thereby offering him or her a multiplicity of possible options to apply
(e.g. trading off modifying the robot’s behavior vs. restricting the environment). Such an extension will involve mining
more complex formulas from the synthesis game and automatically translating such formulas into easy-to-understand
explanations.
Acknowledgement
The authors thank Salar Moarref, Ufuk Topcu, and Rajeev Alur for insightful discussions relating to synthesis of
counterstrategy-based environment revisions.
References
R. Alur, et al. (2013). ‘Counter-strategy guided refinement of GR(1) temporal logic specifications’. In Formal Methods in Computer-Aided
Design (FMCAD 2013), pp. 26–33.
Dynamics-Based Reactive Synthesis and Automated Revisions
24
D. Angeli & E. D. Sontag (1999). ‘Forward completeness, unboundedness observability, and their Lyapunov characterizations’. Systems
& Control Letters 38(4):209–217.
A. Bhatia, et al. (2010). ‘Sampling-based motion planning with temporal goals’. In IEEE International Conference on Robotics and
Automation (ICRA 2010), pp. 2689–2696. IEEE.
R. Bloem, et al. (2012). ‘Synthesis of reactive (1) designs’. Journal of Computer and System Sciences 78(3):911–938.
J. DeCastro & H. Kress-Gazit (2014). ‘Synthesis of Nonlinear Continuous Controllers for Verifiably-Correct High-Level, Reactive
Behaviors’. International Journal of Robotics Research Accepted.
G. E. Fainekos (2011). ‘Revising Temporal Logic Specifications for Motion Planning’. In Proceedings of the IEEE Conference on
Robotics and Automation.
G. E. Fainekos, et al. (2009). ‘Temporal logic motion planning for dynamic robots’. Automatica 45(2):343 – 352.
G. E. Fainekos, et al. (2006). ‘Translating Temporal Logic to Controller Specifications’. In Proc. of the 45th IEEE Conf. on Decision
and Control (CDC 2006), pp. 899–904.
G. E. Fainekos & G. J. Pappas (2009). ‘Robustness of temporal logic specifications for continuous-time signals’. Theoretical Computer
Science 410(42):4262–4291.
A. Girard, et al. (2010). ‘Approximately bisimilar symbolic models for incrementally stable switched systems’. Automatic Control, IEEE
Transactions on 55(1):116–126.
M. Kloetzer & C. Belta (2008). ‘Dealing with Nondeterminism in Symbolic Control’. In M. Egerstedt & B. Mishra (eds.), Hybrid
Systems: Computation and Control, 11th International Workshop (HSCC 2008), vol. 4981 of Lecture Notes in Computer Science, pp.
287–300. Springer.
R. Könighofer, et al. (2009). ‘Debugging formal specifications using simple counterstrategies’. In Proceedings of 9th International
Conference on Formal Methods in Computer-Aided Design, FMCAD 2009, pp. 152–159.
H. Kress-Gazit, et al. (2009). ‘Temporal Logic based Reactive Mission and Motion Planning’. IEEE Transactions on Robotics 25(6):1370–
1381.
H. Kress-Gazit, et al. (2011). ‘Correct, Reactive Robot Control from Abstraction and Temporal Logic Specifications’. Special Issue of
the IEEE Robotics and Automation Magazine on Formal Methods for Robotics and Automation 18(3):65–74.
W. Li, et al. (2011). ‘Mining assumptions for synthesis’. In 9th IEEE/ACM International Conference on Formal Methods and Models
for Codesign, MEMOCODE 2011, pp. 43–50.
W. Li, et al. (2014). ‘Synthesis for Human-in-the-Loop Control Systems’. In Tools and Algorithms for the Construction and Analysis of
Systems - 20th International Conference, TACAS 2014, pp. 470–484.
J. Liu & N. Ozay (2014). ‘Abstraction, Discretization, and Robustness in Temporal Logic Control of Dynamical Systems’. In Proc. of
the 17th Int. Conf. on Hybrid Systems: Computation and Control (HSCC’14) (to appear).
J. Liu, et al. (2013). ‘Synthesis of Reactive Switching Protocols From Temporal Logic Specifications’. IEEE Trans. Automat. Contr.
58(7):1771–1785.
J. Liu, et al. (2012). ‘Reactive controllers for differentially flat systems with temporal logic constraints’. In Proc. of the 51st IEEE Conf.
on Decision and Control (CDC 2012), pp. 7664–7670.
M. Maly, et al. (2013). ‘Iterative Temporal Motion Planning for Hybrid Systems in Partially Unknown Environments’. In ACM
International Conference on Hybrid Systems: Computation and Control (HSCC), pp. 353–362, Philadelphia, PA, USA. ACM, ACM.
I. M. Mitchell, et al. (2005). ‘A time-dependent Hamilton-Jacobi formulation of reachable sets for continuous dynamic games.’. IEEE
Trans. Automat. Contr. 50(7):947–957.
G. Pola, et al. (2008). ‘Approximately bisimilar symbolic models for nonlinear control systems’. Automatica 44(10):2508–2516.
V. Raman & H. Kress-Gazit (2013). ‘Explaining Impossible High-Level Robot Behaviors’. IEEE Transactions on Robotics 29(1):94–104.
V. Raman & H. Kress-Gazit (2013). ‘Towards Minimal Explanations of Unsynthesizability for High-Level Robot Behaviors’. In Proc.
of the IEEE/RSJ Int. Conf. on Intelligent Robots and Systems (IROS 2013).
G. Reißig (2011). ‘Computing abstractions of nonlinear systems’. IEEE Transactions on Automatic Control 56(11):2583–2598.
Dynamics-Based Reactive Synthesis and Automated Revisions
25
P. Tabuada & G. J. Pappas (2006). ‘Linear Time Logic Control of Discrete-Time Linear Systems’. IEEE Trans. Automat. Contr.
51(12):1862–1877.
C. J. Tomlin, et al. (2000). ‘A Game Theoretic Approach to Controller Design for Hybrid Systems’. Proceedings of IEEE 88:949–969.
J. Tumova, et al. (2010). ‘A symbolic approach to controlling piecewise affine systems’. In 49th IEEE Conference on Decision and
Control (CDC), pp. 4230 –4235.
M. Y. Vardi (1996). ‘An automata-theoretic approach to linear temporal logic’. In Logics for concurrency, pp. 238–266. Springer.
E. M. Wolff, et al. (2013). ‘Automaton-Guided Controller Synthesis for Nonlinear Systems with Temporal Logic’. In Proc. of the
IEEE/RSJ Int. Conf. on Intelligent Robots and Systems (IROS 2013).
T. Wongpiromsarn, et al. (2010). ‘Receding Horizon Control for Temporal Logic Specifications’. In Proc. of the 13th Int. Conf. on Hybrid
Systems: Computation and Control (HSCC’10).
B. Yordanov, et al. (2012). ‘Temporal Logic Control of Discrete-Time Piecewise Affine Systems’. Automatic Control, IEEE Transactions
on 57(6):1491–1504.
M. Zamani, et al. (2012). ‘Symbolic models for nonlinear control systems without stability assumptions’. IEEE Transactions on Automatic
Control 57(7):1804–1809.