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   | ¬ φ   | ©   φ   |   φ 1 U φ 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   )  ︸   ︷︷   ︸  φ e  = ⇒   ( φ s i   ∧   φ s t   ∧   φ s g   )  ︸   ︷︷   ︸  φ 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   ∧  i ∈ I α     ( B α i   ) , where  I α   is the index set of environment goals ( B e i   ) or system goals ( B e i   ).  Definition   2   (Controller   Strategy   and   Execution) .   Define   a   controller   as   a   finite-state   machine   A   = ( S, S 0 ,   X   ,   Y , δ, γ X   , γ Y   ) , where   S   is the set of controller states,   S 0   ⊆   S   is the set of initial controller states,   X   and   Y  are sets of propositions described above,   δ   :   S   ×   2 X   →   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   ∈   2 X   , i.e.   s ′   =   δ ( s, z ) ,   γ X   :   S   →   2 X   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   →   2 Y   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   ( s 0 ) , γ Y   ( s 0 ))( γ X   ( s 1 ) , γ Y   ( s 1 )) , . . .   for   s 0   ∈   S 0   and   s i   ∈   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   ⊂   R n , let   R   =   { R 1   . . . R p }   represent a set of disjoint regions whose closure covers   W   , where the open sets   R i   ⊆   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  R i   ∈ 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 ( R i ) ∩ cl ( R j   ) 6 = ∅  ©   π 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   :   R n   ×   R m   →   R n , 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 ′   ∈   R n ,   t   ∈   R ≥ 0   and constant input function   ν   ∈   U   . Given that (1) is Lipschitz continuous with constant   L , the function   β ( r, t ) =   re Lt   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   ⊂   R n   and the bounded space of command inputs   U   ⊂   R m . We denote  [ W   ] η   to be the uniform grid on   W   discretized with resolution   η . This grid is defined as follows:  [ W   ] η   :=   { x   ∈   W   | ∃ k   ∈   Z n   :   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   Y a   describing the robot’s pose, and a set of   locomotion command  propositions   U a   describing the controlled actions taken by the robot. We assume throughout that   U a   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   S a ( τ, η, μ )   is defined by the tuple   ( Q a , V a , δ a , γ Y  a   , γ U  a   ) , where: •   Q a   = [ X ] η   is the set of discretized robot configurations; •   V a   = [ U   ] μ   is the set of discretized robot locomotion commands; •   δ a   :   Q a   ×   V a   →   2 Q a   is a transition relation defined such that, there exists   q a , q ′  a   ∈   Q a   and   v a   ∈   V a ,   q ′  a   ∈   δ a ( q a , v a )  iff there exists   ξ x,ν   with   ν ( t ) =   v a , for all   x   ∈ { x 0   | | x 0   −   q a | ≤   η/ 2 }   and   t   ∈   [0 , τ   ) , such that  | q ′  a   −   ξ x,ν   ( τ   ) | ≤   β ( η/ 2 , τ   ) +   η/ 2;   (3) •   γ Y  a   :   Q a   → Y a   labels each discretized configuration with the associated proposition in   Y a   that evaluates to   True  when the robot is in the given configuration; •   γ U  a   :   V a   → U a   labels each discretized command with the associated proposition in   U a   that evaluates to   True   when the given command is active. Additionally, we define   γ a   :   R →   2 Y a   , a labelling function associating each region to a set of configuration propositions, as   γ a ( R j   ) =   { γ Y  a   ( q a )   |   q a   ∈   [ R j   ] η   } . Finally, we encode the transitions   δ a   as a safety formula   φ a t   defined over   Y a   ∪ © U a   ∪ © Y a   of the form  φ a t   =   ∧  γ Y  a   ( q a   ) ∈Y a  γ U  a   ( v a   ) ∈U a         (   γ Y  a   ( q a )   ∧ ©   γ U  a   ( v a ) )   = ⇒   ∨  γ Y  a   ( q ′  a   ) ∈Y a   :  q ′  a   ∈ δ a   ( q a   ,v a   )  ©   γ Y  a   ( q ′  a )         .  Suppose   Y a   =   { π 0 , π 1 , π 2 } ,   U a   =   { π f wd }   and we start at grid cell   π 0   at   q 0 . Assume that the set of possible successor configurations under this command consists of cells 1 and 2; i.e.   δ a ( q 0 , v 0 ) =   { q 1 , q 2 } , where   γ Y  a   ( q 1 ) =   π 1 ,   γ Y  a   ( q 2 ) =   π 2  and   γ U  a   ( v 0 ) =   π f wd . In this example, we write      (( π 0   ∧ ©   π f wd ) = ⇒ © ( π 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   S a -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   ∈   R n   | { x }   +   ε B   ⊆   R i }  ˆ R ε i   =   { x   ∈   R n   |   x   ∈   R i   +   ε B } .  Here we use   +   to denote the Minkowski set addition and   B   to denote the closed ball in   R n   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   S a -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 ∪ Y a   ∪ U a . We describe in Section 5 our procedure for checking realizability for this formula. The synthesis of a discrete controller   A S a   given the formula   φ e   = ⇒   ( φ s   ∧   φ top t   )   and an abstraction   S a   involves the following steps: (1) computation of the formula   φ a t   from   S a   (Section 2.3); (2) computation of the   S a -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  S a -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   S a , and the   S a -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   s 1 _ occupied   and   s 2 _ 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      ¬ s 1 _ occupied   ∧       ¬ s 2 _ occupied   /   env liveness   ( s 1 _ occupied   = ⇒ © ¬ station _ 1)   /   sys safety   ( s 2 _ occupied   = ⇒ © ¬ station _ 2)   /   sys safety   ( station _ 1 = ⇒ ¬ s 1 _ occupied )   /   env safety   ( station _ 2 = ⇒ ¬ s 2 _ 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 )   ∈   R 2   are the Cartesian robot coordinates. We derive an abstraction   S a   of these dynamics in the configuration space   ( x, y,    ̇ x,    ̇ y )   ∈   W   and obtain the formula   φ abs . With   S a , 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  s 1 _ 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   s 1 _ 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   s 1 _ occupied   and   s 2 _ 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   A S a   = ( S, S 0 ,   X   ,   Y a ,   U a , δ, γ X   , γ Y   , γ U   ) , where   S ,   S 0 ,   X   ,   Y a ,   U a , and  γ X   are as described in Definition 2,   δ   :   S   ×   2 X   →   2 S   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   →   2 Y a  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   →   2 U a   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   ( s 0 ) , γ U   ( s 0 ) , γ Y   ( s 0 ))( γ X   ( s 1 ) , γ U   ( s 1 ) , γ Y   ( s 1 )) , . . . , 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   A S a   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 )   = ⇒   © ¬ r 1 )   has no equivalent counterpart   ˆ φ s t   in the method of Liu et al. (2013). The reason is that both   person   and   r 1   are environment variables, and the fact that the system is required to move   before   r 1   is decided forces   r 1   to be delayed to the next position in the execution. The translation is therefore   (( person   ∧ © ¬ person )   = ⇒   © © ¬ r 1 ) , 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   r 1   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   U a   such that all executions of   A S a   satisfy the specification for all   Y a .   φ abs  is unrealizable if there exists some environment behavior(s) such that no   U a   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 ∪ U a   ∪ Y a   is the set of proposition valuations representing the position in the game; •   θ   ⊆   2 V   is the set of initial positions; •   ρ e   ⊆   2 V   ×   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   ⊆   2 V   ×   2 © U a   ×   2 © Y a   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   ⊆   2 V   ×   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 :  J Pre W K   :=   { v   ∈   2 V   | ∀ v x   ⊆ X   ,   ∃ v u   ⊆ U a ,   ∀ v y   ⊆ Y a   : (( v, v x )   ∈   ρ e ) = ⇒   [(( v, v u , v y   )   ∈   ρ r   ) = ⇒  [(( v, v x , v u , v y   )   ∈   ρ s )   ∧   (( v x , v u , v y   )   ∈   J W K )]] } .  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   V win   based on the   μ -calculus formula Bloem et al. (2012)   V win   =  ν W 1 .   ∧  i s ∈ I s   μ W 2 .   ∨  i e ∈ I e   ν W 3 .N i s i e   , where   N i s i e   = ( B s i s   ∧   Pre W 1 )   ∨   Pre W 2   ∨   ( ¬ B e i e   ∧   Pre W 3 )   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   A S a   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   A c   = ( Q c , Q c  0 ,   X   ,   Y a ,   U a , δ c , γ c  U   , γ c  X   , γ c  Y   ) , where •   Q c   is the set of counterstrategy states; •   Q c  0   ⊆   Q c   is the set of initial counterstrategy states; •   X   ,   Y a   and   U a   are sets of propositions in   AP   ; •   δ c   :   Q c   →   2 Q c  is a nondeterministic transition relation returning the set of counterstrategy states at the next position in the sequence given the current state; •   γ c  U   :   Q c   →   2 U a   is a labelling function mapping counterstrategy states to the set of locomotion command propositions in   U a   evaluating to   True   for all transitions into that state; •   γ c  X   :   Q c   →   2 X   is a labelling function mapping counterstrategy states to the set of environment propositions in   X  evaluating to   True   in that state, and; •   γ c  Y   :   Q c   →   2 Y a   is a labelling function mapping counterstrategy states to the set of robot configurations in   Y a  evaluating to   True   in that state. We furthermore define   δ c − 1  : 2 Q c  →   Q c   as the inverse transition relation mapping counterstrategy states to a set of predecessors; i.e.   δ c − 1  ( q ′ ) =   { q   ∈   Q c   |   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   A c   from the set of positions that are winning for player 1. We define the enforceable predecessor operator for the counterstrategy   Pre c   as follows:  J Pre c W K   :=   { v   ∈   2 V c  | ∃ v x   ⊆ X   ,   ∀ v u   ⊆ U a ,   ∃ v y   ⊆ Y a   : (( v, v x )   ∈   ρ e )   ∧   [[(( v, v u , v y   )   ∈   ρ r   ) ∧  (( v, v x , v u , v y   )   ∈   ρ s )] = ⇒   (( v x , v u , v y   )   ∈   J W K )] } .  The set of winning positions   V c win   =   X ∪ U a   ∪ Y a   for player 1 may then be computed from the formula   V c win   =  μ W 1 .   ∨  i s   ∈ I s   ν W 2 .   ∧  i e ∈ I e   μ W 3 .N   c i s i e   , where  N   c i s   i e   = ( ¬ B s i s   ∨   Pre c W 1 )   ∧   Pre c W 2   ∧   ( B e i e   ∨   Pre c W 3 ) ,  A counterstrategy is synthesized by storing the sets   N   c i s i e   for each   i s   and   i e   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   i s   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   ∈ Y a   that belong to   N   c i s   i e   for every   v ′  u   ∈ U a . A check is made to determine if a liveness assumption has been fulfilled at   q ; if it has, then a new liveness assumption   i e   is selected. For notational convenience, we define the set of successor values winning for player 1 at a counterstrategy state   q   as  M X   ( q ) =   { v ′  x   ∈ X | ∀ v ′  u   ∈ U a ,   ∃ v ′  y   ∈ Y a   : ( v, v ′  x , v ′  u , v ′  y   )   ∈   N   c i s ( q ) i e   ( 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.   Consider the workspace shown in Figure 2a. Given   X   =   { sen }   where   sen   is the sensor input and   Y   =   { r 1 , r 2 } , we write a specification   φ   requiring the robot to visit   r 2   (lower-left gray region) when   s   is   False , but avoid   r 2   when   sen  is   True . Formally:      r 2   / φ s g      ¬ sen   / φ e g   ( ©   sen   = ⇒ © ¬ r 2)   / φ s t   ( r 2 = ⇒ © ¬ sen )   / φ e t  True   / φ s i  True   / φ e i  The controller satisfying this specification is given in Figure 2b. Given an abstraction where   Y a   =   { x 1 , . . . , x 16 }   is an encoding of the set of 2-D robot configurations, and   U a   =  { N, S, E, W   }   are the robot commands for motion in the four cardinal directions, we derive a new specification   φ abs , where:    ( x 9   ∨   x 13)   /   ˆ φ s g      ¬ sen   / φ e g   ( ©   sen   = ⇒ © ¬ ( x 9   ∨   x 13))   /   ˆ φ s t   (( x 9   ∨   x 13) = ⇒ © ¬ 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   r 1 , while the gray denote   r 2 . (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   A c   whose deadlock states are collected in   Q dead . There exists an execution that eventually reaches a deadlock state   q i dead ; specifically when   ∃ q ′   ∈   δ c ( q i dead ) :   q ′   =   ∅ . We formally state this behavior as   ∨  q j   ∈ δ c − 1   ( q i dead   )     ( ψ 1 ( q j   )   ∧ ©   ψ 2 ( q i 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 )  π   ∧   ∧  π ∈ ( U a   ∪Y a   ) \ ( γ c  U   ( q ) ∪ γ c  Y   ( q ))  ¬ π, ψ 2 ( q ) =   ∧  π ∈ γ c  X   ( q )  π   ∧   ∧  π ∈X \ γ c s   ( 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:  ∧  q j   ∈ δ c − 1   ( q i dead   )     ( ψ 1 ( q j   ) = ⇒ © ¬ ψ 2 ( q i 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   q 0 , q 1 , q 2 , q 3 , q 4 , as pictured in Figures 3a and 3b, starting in cell   x 3   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   x 4   with the sensor   sen   = True :  σ   = ( { ∅ } ,   { ∅ } ,   { x 3 } ) ,   ( { ∅ } ,   { W   } ,   { x 2 } ) ,   ( { ∅ } ,   { W   } ,   { x 1 } ) ,  ( { ∅ } ,   { S } ,   { x 5 } ) ,   ( { s } ,   { ∅ } ,   { ∅ } ) .  where the   i th time step corresponds to   q i . In this execution, the sensor   sen   remains   False   until the robot enters   x 5 , at which point a transition in   φ s t   is violated. Hence   q 4   is a deadlock state. The formula   ( ©   sen   ∧ ¬ x 1   ∧   S ) 1   is extracted by evaluating   ( ψ 1 ( q 4 ) ∧©   ψ 2 ( q 4 )) . The complement of this formula,    (( ¬ x 1 ∧ 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   r 2   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   x 5 . In the example, consider the behavior when the robot starts at   x 7   with   sen   True . The execution of the robot in this case is  σ   = ( { sen } ,   { ∅ } ,   { x 7 } ) ,   ( { sen } ,   { W   } ,   { x 6 } ) ,   ( { sen } ,   { W   } ,   { x 5 } ) ,  ( { sen } ,   { S } ,   { x 9 } ) ,   ( { ∅ } ,   { E } ,   { x 10 } ) ,   ( { ∅ } ,   { N   } ,   { x 6 } ) , . . . .  In this execution,   sen   remains   True   and, as the robot moves toward   r 2 , the environment eventually must set   sen   to   False  to be consistent with the added assumption. When outside of   x 5 , 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   r 1   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   ∨  q j   ∈ δ c − 1   ( q i dead   )   ( © ¬ ψ 2 ( q i dead )   ∧ © ¬ ψ 1 ( q j   ))   by introducing an additional revision on   φ s t  ∧  q j   ∈ δ c − 1   ( q i dead )     ( © ¬ ψ 2 ( q i dead ) = ⇒ ©   ψ 1 ( q j   ) )   .   (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   r 2 . 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   ∧  q j   ∈ δ c − 1   ( q i dead   )   ψ 1 ( q j   ) . If the modified formula is determined to be unrealizable and new deadlock states are found at a state   q j   ∈   δ c − 1  ( q i 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  Q c \ Q dead . 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   Q commit   by adding, via a breadth-first search ( BFS   in line 4), predecessor counterstrategy states from deadlock   Q dead   for which all locomotion commands lead to states in  Q commit . For generating revisions and providing user feedback, we also maintain a mapping   Q reach   :   Q commit   →   2 Q dead  of deadlock states reachable from each   q   ∈   Q commit . 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   Q commit   and   Q reach . The precise condition under which the search terminates is when a   q   ∈   Q c   is found such that:  ∃ q ′   ∈   δ c ( q ) :   q ′   / ∈   Q commit .  Here,   Q commit   plays the role of   Q dead . We therefore replace   Q dead   in the safety revisions (8) and (9) with   Q commit . To be precise, we replace (8) with  ∧  q j   ∈ Q i commit      ψ 1 ( q j   ) = ⇒   ∨  q k   ∈ Q reach ( q i commit   )  © ¬ ψ 2 ( q k )      (10)
Dynamics-Based Reactive Synthesis and Automated Revisions   16 and (9) with  ∧  q j   ∈ Q i commit        ∧  q k   ∈ Q reach ( q i commit   )  ( ©   ψ 2 ( q k ) = ⇒ © ¬ ψ 1 ( q j   ) )     ,   (11) for each   q i commit   ∈   Q commit . Consider the example below.  Algorithm 1   Computing deadlock-committed states.  procedure   commitStates( Q dead ) Initialize   Q new , Q commit , Q reach   to   Q dead  while   Q new   6   =   ∅   do  ( Q new , Q reach )   ←   BFS ( A c , Q commit , Q reach )  5:   Q commit   ←   Q commit   ∪   Q new  end while return   Q commit ,   Q reach  end procedure Example 4.   Starting from the result of Example 3, we compute a set of four deadlock-commit states   Q commit   =  { q 1 , q 2 , q 3 , q 4 }   corresponding to the cells   { x 6 , x 2 , x 1 , x 5 } . We obtain the following   ψ e t   formulas:   (( x 5   ∧   S ) = ⇒ © ¬ sen )   (12)   (( x 1   ∧   S ) = ⇒ © ¬ sen )   (13)   (( x 2   ∧   W   ) = ⇒ © ¬ sen )   (14)   (( x 6   ∧   N   ) = ⇒ © ¬ sen ) ,   (15) and the following   ψ s t   formulas:   ( ©   sen   = ⇒ © ¬ ( x 5   ∧   S ))   (16)   ( ©   sen   = ⇒ © ¬ ( x 1   ∧   S ))   (17)   ( ©   sen   = ⇒ © ¬ ( x 2   ∧   W   ))   (18)   ( ©   sen   = ⇒ © ¬ ( x 6   ∧   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 .  x 16 , the following behavior is possible:  σ   = ( { ∅ } ,   { ∅ } ,   { x 16 } ) ,   ( { ∅ } ,   { N   } ,   { x 12 } ) ,   ( { ∅ } ,   { N   } ,   { x 8 } ) ,  ( { sen } ,   { W   } ,   { x 7 } ) ,   ( { ∅ } ,   { S } ,   { x 11 } ) ,   ( { ∅ } ,   { S } ,   { x 15 } ) ,  ( { ∅ } ,   { E } ,   { x 16 } ) ,   ( { ∅ } ,   { N   } ,   { x 12 } ) , . . . .  In this execution(shown in Figure 4), the robot eventually cycles indefinitely between six cells in the workspace. Whenever the robot visits the cell   x 7 , 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   r 2 . 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   M X   ( 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   ∈   Q c , our goal is to find a subset   Q cut   ⊆   Q c   for which   v ′  x   / ∈   M X   ( q ) , where   M X   ( q )   are the set of environment inputs at a state   q   ∈   Q c   that are winning for player 1. Consequently, for any   q   ∈   Q cut   there are some   v ′  x   ⊆ X  and   v ′  u   ⊆ U a   that lead to a position that is not winning for player 1 (i.e.   v ′  x   / ∈   M X   ( q ) ). One can think of   Q cut   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   Q cut , 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   Q cut   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   Q cut   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   P cut   ⊆   Q cut   for which the robot has safe commands that are winning for the system. We use  Q commit   (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   P cut   as follows:  P cut   =   { q   ∈   Q cut   | ∃ v a   ∈   V a ,   ∃ q ′   ∈   Q commit ,   ∃ q a   ∈   δ a ( v a , γ c  Y   ( q )) :  ∀ π   ∈ Y a , π   ∈   γ Y  a   ( q a )   iff   π   ∈   γ c  Y   ( q ′ ) } .   (20) We then apply the environment liveness assumption      ∨  q i ∈ P cut    ψ 1 ( q i )   ∧   ∧  q j   ∈ δ c   ( q i ,γ c  Y   ( q i ))  © ¬ ψ 2 ( q j   )      .   (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   Q cut   consists of four states,   { q 3 , q 5 , q 6 , q 8 } . Of these,   { q 3 , q 6 , q 8 }   are states in which the robot has an action (move   W   ) taking the robot closer to   r 2   that the environment can prevent. These are found from Example 3 and are collected in   P cut . We also find state   { q 5 } , 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   P cut :    (( x 7   ∧   W   ∧ © ¬ sen )   ∨   ( x 3   ∧   W   ∧ © ¬ sen )   ∨   ( x 7   ∧   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   r 2 ” 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   R i   ∈ R , we mark those deadlock states (if any exist) from whose predecessors there exists a robot command   v a   ∈   V a   (Definition 4) to reach   R i . Those marked deadlock states are collected in the set   P dead ( R i ) , defined formally as:  P dead ( R i ) =   { q   ∈   Q dead   | ∀ q ′   ∈   δ c − 1  ( q ) ,   ∃ v a   ∈   V a ,   ∃ q ′  a   ∈   δ a ( v a , γ c  Y   ( q ′ )) :  ∀ π   ∈ Y a , π   ∈   γ Y  a   ( q ′  a )   iff   π   ∈   γ a ( R i ) } .  In the fixed point computation in Algorithm 1, we keep track of each deadlock state reachable from each state added to  Q commit . We use this stored information to find the distances between each robot configuration in   Q commit . 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   R i   corresponding to a robot configuration that satisfies some deadlock state in   Q dead , 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 ∈ Q commit   , q ′   ∈ Q reach ( q ) ∩ P dead ( R i )  | γ c  Y   ( q )   −   γ c  Y   ( δ c − 1  ( q ′ )) | .   (23) Here,   | v y   |   is the Euclidean norm of the real-valued abstraction state   q a   ∈   Q a   represented by a set of propositions   v y   ⊆ Y a  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  R i   where the distance is greatest, under the constraint that   q ? dead,i   is a deadlock state that is reachable from   q ? i   ∈   Q commit . Note that the distance between the configurations of the two states is:  dist i   =   | γ c  Y   ( q ? i   )   −   γ c  Y   ( δ c − 1  ( q ? dead,i )) | .  The final step is to correlate each unique region   R i   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   ( R i , dist i , ψ 2 ( q ? dead,i )) . The triple can be displayed to the user as follows: “If the robot is within   dist i   of workspace region   R i , 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   dist i   with any environment setting yet still be able to satisfy the revision formulas.  Example 6.   In the result of Example 4, let   q dead   be the deadlock state computed by the counterstrategy corresponding to the configuration   x 9 , and designate   Q commit   =   { q 1 , q 2 , q 3 , q 4 }   as the set of commit states for this deadlock. For workspace region   r 2 ,   P dead ( r 2 ) =   q dead , and   Q reach ( q i ) =   q dead   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  )∣ ∣ ∣ ∣ ∣ }  = ( q 2 , q dead ) ,  where the subscript 2 in the   ?   variables is used to signify the fact that the variables apply to region   r 2 . Assuming   η   = 1 m , the corresponding distance is   dist 2   =   √ 1 2   + 2 2   = 2 . 2 m . 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 . 2 m   of   r 2 , 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   Q commit . 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,   A 1  c   , M X   )   ←   ctrStrategy ( φ abs )  A 0  c   ← False ,   m   ←   0  5:   while   ¬ realiz   ∧   ( A m c   6   =   A m − 1  c   )   do  .   Step 1: Eliminate deadlocks  Q commit   ←   commitStates ( A c )  for all   q i commit   ∈   Q commit   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   R i   ∈ R   do  ( q ? i   , q ? dead )   ←   Eq. (23)  dist i   ← | γ c  Y   ( q ? )   −   γ c  Y   ( q ? dead ) |  20:   print   ( R i , dist i , ψ 2 ( q ? dead,i ))  end for if   user accepts deadlock revisions   then  φ mod   ←   Eq. (6)  ( realiz,   A m c   , M X   )   ←   ctrStrategy ( φ mod )  25:   end if  .   Step 3: Eliminate livelocks  Q cut   ← { q   ∈   Q c   | ∃ v ′  x   / ∈   M X   ( q ) }  P cut   ←   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,   A m c   , M X   )   ←   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   ×   10 6   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   s 1 _ 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   s 2 _ 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   s 1 _ 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:   s 1 _ occupied ; blue:  s 2 _ occupied ). (a) shows a trajectory when the   s 1 _ occupied   sensor is activated. (b) shows a trajectory when the   s 2 _ 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.