We consider the problem of computing the controllable region of a Linear Hybrid Automaton with controllable and uncontrollable transitions, w.r.t. a reachability objective. We provide an algorithm for the nite-horizon version of the problem, based on computing the set of states that must reach a given non-convex polyhedron while avoiding another one, subject to a polyhedral constraint on the slope of the trajectory.
Hybrid systems are non-linear dynamic systems, characterized by the presence
of continuous and discrete variables. Hybrid automata [
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 transitions; 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 veri cation (i.e.,
1player reachability) for LHAs [
Although the control goal we examine, as a language of in nite 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
computing the may-reach-while-avoiding operator RWAm [
To the best of our knowledge, the reachability control goal was never
considered for LHGs. In the full paper [
A convex polyhedron is a subset of Rn that is the intersection of a nite number of strict and non-strict a ne half-spaces. A polyhedron is the union of a nite number of convex polyhedra. Given an ordered set X = fx1; : : : ; xng 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 X_ to denote the set fx_ 1; : : : ; x_ ng of dotted variables, used to represent the rst derivatives, and X0 to denote the set fx01; : : : ; x0ng 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 di erentiable but for a nite subset of R 0.
De nition 1. A Linear Hybrid Game (LHG) (Loc; X; Edg c; Edg u; Flow ; Inv ; Init ) consists of the following components: (i) a nite set Loc of locations; (ii) a nite set X = fx1; : : : ; xng of real-valued variables; (iii) two sets Edg c; Edg u Loc Poly (X [ X0) Loc of controllable and uncontrollable transitions, respectively; (iv) a mapping Flow : Loc ! CPoly (X_ ), called the ow constraint; (v) a mapping Inv : Loc ! Poly (X), called the invariant; (vi) a mapping Init : Loc ! Poly (X), contained in the invariant, de ning the initial states of the automaton.
A state is a pair hl; vi of a location l and a valuation v 2 Val (X). Transitions describe instantaneous changes of location, in the course of which the variables may change their value. Each transition (l; J; l0) 2 Edg c [ Edg u consists of a source location l, a target location l0, and a jump relation J 2 Poly (X [ X0), that speci es 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 ow constraint attributes to each location a set of valuations over the rst derivatives of the variables, which determines how variables can change over time. We let InvS = Sl2Locflg Inv (l) and InitS = Sl2Locflg Init (l). Notice that InvS and InitS are sets of states. Given a set of states A and a location l, we denote by A l the projection of A on l.
The behavior of an LHG is based on two types of steps: discrete steps
correspond to the Edg component, and produce an instantaneous change in both the
location and the variable valuation; timed steps describe the change of the
variables over time in accordance with the Flow component. A joint step is either a
timed step of in nite duration, or a timed step of nite duration followed by a
discrete step. The controller in uences 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 de nitions are included in the full paper [
The following theorem states the general procedure for solving the reachability
control problem, based on the controllable predecessor operator for reachability
CPreR. For a set of states A, the set CPreR(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 [
The following theorem states that the least xpoint of the operator (X) , T [CPreR(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 [ CPreR(W ), where denotes the least xpoint. If the xpoint is obtained in a nite 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 predecessor 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 , RWAlM(U; V ) contains the set of valuations from which all continuous trajectories of the system reach U while avoiding V 2.
We can now reformulate CPreR by means of the operator RWAlM. 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 CPreR(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 A l while avoiding Bl n A l, thus without giving the environment any chance to take an action leading outside A; (ii) the system reaches a point in Cl n Bl, from where the controller can force the system into A, while avoiding Bl nA l; or (iii) the trajectory exits from the invariant Inv (l) meanwhile avoiding Bl n A l. 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 2 Loc, the projection A l is a polyhedron. Lemma 1. If A
InvS is polyhedral, the following holds: CPreR(A) = InvS \ [ flg
RWAlM A l [ Cl n Bl [ Inv (l); Bl n A l :
l2Loc
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 RWAlm(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 [
In the rest of this section, we consider a xed location l 2 Loc and we omit the l subscript whenever possible. For a polyhedron G and p 2 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 2 G are t-bounded in G. 2 In the temporal logic Ctl, we have RWAM(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 de nition. Now, the content of RWAM(U; V ) can be partitioned into two regions: the rst region is U ; the second region must be t-bounded, because each point in the second region must eventually reach U . If we can nd a polyhedron Over that over-approximates RWAM(U; V ) and such that Over n U is t-bounded, we can use RWAm to re ne it. Precisely, we can use RWAm to identify and remove the points of Over that may leave Over without hitting U rst.
If Over n 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 n U is t-bounded. Then, RWAM(U; V ) = Over n RWAm(Over ; U ).
It can be proved that the set Over , U [ t -bnd (U \ V ) is computable
and satis es the conditions of Theorem 2. The full paper [