Automatic synthesis of switching controllers for linear hybrid systems: Reachability control Massimo Benerecetti and Marco Faella Università di Napoli “Federico II”, Italy Abstract. We consider the problem of computing the controllable re- gion of a Linear Hybrid Automaton with controllable and uncontrollable transitions, w.r.t. a reachability objective. We provide an algorithm for the finite-horizon version of the problem, based on computing the set of states that must reach a given non-convex polyhedron while avoid- ing another one, subject to a polyhedral constraint on the slope of the trajectory. 1 Introduction Hybrid systems are non-linear dynamic systems, characterized by the presence of continuous and discrete variables. Hybrid automata [5] are the most common syntactic variety of hybrid system: a finite set of locations, similar to the states of a finite automaton, represents the value of the discrete variables. The current location, together with the current value of the (continuous) variables, form the instantaneous description of the system. Change of location happens via discrete transitions, and the evolution of the variables is governed by differential inclusions attached to each location. In a Linear Hybrid Automaton (LHA), the allowed differential inclusions are of the type ẋ ∈ P , where ẋ is the vector of the first derivatives of all variables and P ⊆ Rn is a convex polyhedron. Notice that differential inclusions are non-deterministic, allowing for infinitely many solutions with the same starting conditions. We study LHAs whose discrete transitions are partitioned into controllable and uncontrollable ones, giving rise to a 2-player model called Linear Hybrid Game (LHG): on one side the controller, which can only issue controllable tran- sitions; on the other side the environment, which can choose the trajectory of the variables and can take uncontrollable transitions whenever they are enabled. As control goal, we consider reachability, i.e., the objective of reaching a given set of target states. It is easy to show that the reachability control problem is undecidable, being harder than the standard reachability verification (i.e., 1- player reachability) for LHAs [6] . We present the first exact algorithm for 1-step controllability under a reachability objective, namely reaching the target region with at most one discrete transition. In turn, this provides an exact algorithm for bounded-horizon reachability control (i.e., reaching the target within a fixed number of discrete steps), and a semi-algorithm1 for the infinite-horizon case. This extended abstract summarizes the results of [2]. 1 In other words, a procedure that may or may not terminate, and that provides the correct answer whenever it terminates. Although the control goal we examine, as a language of infinite traces, is the dual of safety, the corresponding synthesis problem is not, because our game model is asymmetric: choice of continuous-time trajectories is uncontrollable. Hence, it is not possible to solve the control problem with reachability goal T by exchanging the roles of the two players and then solving the safety control problem with goal T (i.e., the complement of T ). On the one hand, the 1-step safety control problem can be solved by com- puting the may-reach-while-avoiding operator RWAm [3, 4]. Given two sets of states U and V , RWAm (U, V ) collects the states from which there exists a sys- tem trajectory that reaches U while avoiding V at all times. On the other hand, the 1-step reachability control problem requires a different operator, called must- reach-while-avoiding and denoted by RWAM (U, V ). As suggested by its name, such operator computes the set of states from which all system trajectories reach U while avoiding V . The main technical result of this paper is that the first op- erator can be used to compute the latter, once a suitable over-approximation of RWAM (U, V ) is available (Theorem 2). Moreover, we present an effective way to obtain such an over-approximation. To the best of our knowledge, the reachability control goal was never consid- ered for LHGs. In the full paper [2], we present the proofs for all results and an experimental evaluation based on an extension to the tool SpaceEx. 2 The model: Linear hybrid games A convex polyhedron is a subset of Rn that is the intersection of a finite number of strict and non-strict affine half-spaces. A polyhedron is the union of a finite number of convex polyhedra. Given an ordered set X = {x1 , . . . , xn } of variables, a valuation is a function v : X → R. Let Val (X) denote the set of valuations over X. There is an obvious bijection between Val (X) and Rn , allowing us to extend the notion of (convex) polyhedron to sets of valuations. We denote by CPoly(X) (resp., Poly(X)) the set of convex polyhedra (resp., polyhedra) on X. Let A be a set of valuations, states or points in Rn , we denote by A its complement. We use Ẋ to denote the set {ẋ1 , . . . , ẋn } of dotted variables, used to represent the first derivatives, and X 0 to denote the set {x01 , . . . , x0n } of primed variables, used to represent the new values of variables after a transition. A trajectory over X is a function f : R≥0 → Val (X) that is differentiable but for a finite subset of R≥0 . Definition 1. A Linear Hybrid Game (LHG) (Loc, X, Edg c , Edg u , Flow , Inv , Init) consists of the following components: (i) a finite set Loc of locations; (ii) a fi- nite set X = {x1 , . . . , xn } of real-valued variables; (iii) two sets Edg c , Edg u ⊆ Loc × Poly(X ∪ X 0 ) × Loc of controllable and uncontrollable transitions, re- spectively; (iv) a mapping Flow : Loc → CPoly(Ẋ), called the flow constraint; (v) a mapping Inv : Loc → Poly(X), called the invariant; (vi) a mapping Init : Loc → Poly(X), contained in the invariant, defining the initial states of the automaton. A state is a pair hl, vi of a location l and a valuation v ∈ Val (X). Transitions describe instantaneous changes of location, in the course of which the variables may change their value. Each transition (l, J, l0 ) ∈ Edg c ∪ Edg u consists of a source location l, a target location l0 , and a jump relation J ∈ Poly(X ∪ X 0 ), that specifies how the variables may change their value during the transition. The projection of J on X contains the valuations for which the transition is enabled, a.k.a. a guard. The flow constraint attributes to each location a set of valuations over the first derivatives of the variables, S which determines how variables S can change over time. We let InvS = l∈Loc {l} × Inv (l) and InitS = l∈Loc {l} × Init(l). Notice that InvS and InitS are sets of states. Given a set of states A and a location l, we denote by Al the projection of A on l. The behavior of an LHG is based on two types of steps: discrete steps corre- spond to the Edg component, and produce an instantaneous change in both the location and the variable valuation; timed steps describe the change of the vari- ables over time in accordance with the Flow component. A joint step is either a timed step of infinite duration, or a timed step of finite duration followed by a discrete step. The controller influences the system through a strategy. Strategies assign to each controllable transition a possibly non-convex polyhedron, which is contained in the jump relation of the transition. The intended meaning is that the strategy restricts controllable transitions so that they can be taken from a given subset of their original guard and they lead to a given subset of their original set of destinations. Formal definitions are included in the full paper [2]. Reachability control problem. Given an LHG and a set of states T ⊆ InvS , the reachability control problem asks whether there exists a strategy σ such that, for all initial states s ∈ InitS , all runs that start from s and are consistent with σ reach some state in T . We call the above σ a winning strategy. 3 Solving the reachability control problem The following theorem states the general procedure for solving the reachability control problem, based on the controllable predecessor operator for reachability CPre R . For a set of states A, the set CPre R (A) contains all states from which the controller can ensure that the system reaches A within the next joint step. In discrete games, the CPre operator used for solving reachability games is the same as the one used for the safety goal [7]. In both cases, when the operator is applied to a set of states T , it returns the set of states from which Player 1 can force the game into T in one step. In hybrid games, the situation is different: a joint step represents a complex behavior, extending over a (possibly) non-zero time interval. While the CPre for reachability only requires T to be visited once during such interval, CPre for safety requires that the entire behavior constantly remains in T . Hence, we present a novel algorithm for computing CPre R . The following theorem states that the least fixpoint of the operator τ (X) , T ∪CPre R (X) provides a solution of the reachability control problem. Intuitively, each application of τ extends (backward), by adding a single joint step, all the runs compatible with some winning strategy for the controller. Theorem 1. Let T be a polyhedron and W ∗ = µW . T ∪ CPre R (W ), where µ denotes the least fixpoint. If the fixpoint is obtained in a finite number of iterations then the answer to the reachability control problem for target set T is positive if and only if InitS ⊆ W ∗ . Computing the predecessor operator. In order to compute the predeces- sor operator, we introduce the Must Reach While Avoiding operator, denoted by RWAM . Given a location l and two sets of variable valuations U and V , RWAM l (U, V ) contains the set of valuations from which all continuous trajecto- ries of the system reach U while avoiding V 2 . We can now reformulate CPre R by means of the operator RWAM l . Let Bl be the set of states of location l, where the environment can take a discrete transition leading outside A and, similarly, Cl be the set of states of l, where the controller can take a discrete transition leading to A. A state s of location l belongs to CPre R (A) if the controller can force the system into A within one joint step, no matter what the environment does. This occurs if, for every possible trajectory chosen by the environment, one of the following conditions holds: (i) the system reaches Al while avoiding Bl \ Al , thus without giving the environment any chance to take an action leading outside A; (ii) the system reaches a point in Cl \ Bl , from where the controller can force the system into A, while avoiding Bl \Al ; or (iii) the trajectory exits from the invariant Inv (l) meanwhile avoiding Bl \ Al . In this last case, the semantics ensures that, before the trajectory exits from the invariant, the environment will take some discrete transition, which can only lead to A (see well-formedness in the full paper). The following lemma formalizes the above intuition. We say that a set of states A is polyhedral if for all l ∈ Loc, the projection Al is a polyhedron. Lemma 1. If A ⊆ InvS is polyhedral, the following holds: [ CPre R (A) = InvS ∩ {l} × RWAM  l Al ∪ Cl \ Bl ∪ Inv (l), Bl \ Al . l∈Loc Computing RWAM . We show how to compute RWAM based on the operator which is used to solve safety control problems: the May Reach While Avoiding operator RWAm l (U, V ), returning the set of states from which there exists a trajectory that reaches U while avoiding V . In safety control problems, RWAm is used to compute the states from which the environment may reach an unsafe state (in U ) while avoiding the states from which the controller can take a transition to a safe state (in V ). Notice that RWAm is a classical operator, known as Reach [8], Unavoid Pre [1], and flow avoid [9]. We recently gave the first sound and complete algorithm for computing it on LHGs [4]. In the rest of this section, we consider a fixed location l ∈ Loc and we omit the l subscript whenever possible. For a polyhedron G and p ∈ G, we say that p is t-bounded in G if all admissible trajectories starting from p eventually exit from G. We denote by t-bnd (G) the set of points of G that are t-bounded in it, and we say that G is t-bounded if all points p ∈ G are t-bounded in G. 2 In the temporal logic Ctl, we have RWAM (U, V ) ≡ ∀ V U (U ∧ V ). We now show how to relate RWAM and RWAm , by exploiting the following idea. First, notice that all points in U belong to RWAM (U, V ) by definition. Now, the content of RWAM (U, V ) can be partitioned into two regions: the first region is U ; the second region must be t-bounded, because each point in the second region must eventually reach U . If we can find a polyhedron Over that over-approximates RWAM (U, V ) and such that Over \ U is t-bounded, we can use RWAm to refine it. Precisely, we can use RWAm to identify and remove the points of Over that may leave Over without hitting U first. If Over \ U is not t-bounded, the above technique does not work, because RWAm cannot identify (and remove) the points that may remain forever in Over without ever reaching U . This idea is formalized by the following result. Theorem 2. For all disjoint polyhedra U and V , such that V is convex, let Over be a polyhedron such that: (i) RWAM (U, V ) ⊆ Over ⊆ V and (ii) Over \ U is t-bounded. Then, RWAM (U, V ) = Over \ RWAm (Over , U ). It can be proved that the set Over , U ∪ t-bnd (U ∩ V ) is computable and satisfies the conditions of Theorem 2. The full paper [2] also provides an alternative, more efficient, version for Over . In conclusion, the results sketched above provide an effective solution to the bounded-horizon reachability control problem and a semi-algorithm for the infinite-horizon version. References 1. A. Balluchi, L. Benvenuti, T. Villa, H. Wong-Toi, and A. Sangiovanni-Vincentelli, “Controller synthesis for hybrid systems with a lower bound on event separation,” Int. J. of Control, vol. 76, no. 12, pp. 1171–1200, 2003. 2. M. Benerecetti and M. Faella, “Automatic synthesis of switching controllers for linear hybrid systems: Reachability control,” ACM Trans. on Embedded Computing Systems, vol. 16, no. 4, 2017. 3. M. Benerecetti, M. Faella, and S. Minopoli, “Revisiting synthesis of switching con- trollers for linear hybrid systems,” in Proc. of the 50th IEEE Conf. on Decision and Control. IEEE, 2011. 4. ——, “Automatic synthesis of switching controllers for linear hybrid systems: Safety control,” Theoretical Computer Science, vol. 493, pp. 116–138, 2013. 5. T. Henzinger, “The theory of hybrid automata,” in 11th IEEE Symp. Logic in Comp. Sci., 1996, pp. 278–292. 6. T. Henzinger, P. Kopke, A. Puri, and P. Varaiya, “What’s decidable about hybrid automata?” J. of Computer and System Sciences, vol. 57, no. 1, pp. 94 – 124, 1998. 7. O. Maler, “Control from computer science,” Annual Reviews in Control, vol. 26, no. 2, pp. 175–187, 2002. 8. C. Tomlin, J. Lygeros, and S. Shankar Sastry, “A game theoretic approach to con- troller design for hybrid systems,” Proc. of the IEEE, vol. 88, no. 7, pp. 949–970, 2000. 9. H. Wong-Toi, “The synthesis of controllers for linear hybrid automata,” in 36th IEEE Conf. on Decision and Control. San Diego, CA: IEEE, 1997, pp. 4607 – 4612.