Hybrid systems exhibit an interaction of discrete control decisions with continuous physical processes and are present at the core of cyberphysical systems. The veri cation task of such systems is challenging. In this paper, we are concerned with abstraction methods of hybrid systems. An abstraction can be used to automate the veri cation of properties such as safety or more complex ones when combined with a model checking algorithm. A tool that automatically computes an abstraction of a given hybrid system with at most polynomial expressiveness is presented. The computed abstraction can be manually re ned to achieve further precision guided by the system designer. The tool is tested over several examples.
Copyright © by the paper's authors. Copying permitted for private and academic purposes. which supposes that the system is partly observable. If a system is diagnosable then it is able to identify the occurrence of a modeled fault using the limited observations [ZYD+18, ZYDG18]. Abstractions of hybrid systems have many use cases such as but not limited to: • Veri cation and automated proving: incorporate abstraction computation for the purpose of automated veri cation in satis ability modulo theory solvers (SMT) for hybrid systems, user-guided theorem proving, model checking, and invariant synthesis techniques. • Design, simulation and speci cation requirements: provide the system designer or architect with veri ed simulation results from the requirements speci cation, piloting numerical simulations and unitary tests. • Provide researchers with insights when modeling complex behaviors.
Related work: The work presented in this paper is inspired from predicate abstraction of hybrid automata introduced in [Tiw08]. The main di erences is the instantiation of the abstraction computation to polynomial hybrid systems and predicates expressed as semi-algebraic sets while providing experimental results and abstraction computation time.
[SW13] addressed computing reachability for non-linear systems with polynomial dynamics. Algorithms are proposed to generate a partitioning of the state space, forming an abstraction that is always sound and in some cases complete. The latter is formulated as an optimization problem, which yields results similar to those obtained by invariant synthesis techniques. The termination of the optimization procedure is generally not guaranteed. The di erence with the author's work is that we propose an algorithm to compute the time bounds used in the abstraction, however no experimental results are provided for this part.
In this paper, a method for generating abstractions of hybrid systems is presented. Qualitative modeling and reasoning are used to compute the abstraction. The contribution of this paper is the development of a tool that computes abstractions of hybrid automata with polynomial expressiveness in terms of the dynamics model. The abstraction computation are evaluated on di erent practical examples. A re nement operation is also de ned and discussed, allowing the user to reach a further precision. The re nement operation will recompute only required information to keep the abstraction sound. Lastly, an abstraction capturing time constraints is proposed which allows one to handle time constraints that can be abstracted at a qualitative level from the hybrid system through the previously de ned abstraction.
The paper is organized as follows. In Section 2 a formal framework for hybrid automata is introduced, then an abstraction of a given hybrid system based on qualitative reasoning is de ned. Afterwards, the main algorithms used in the implemented tool for automatically computing the de ned abstraction are presented. The abstraction computation is then illustrated on di erent practical examples and performances of the computations are evaluated. In the last section, a re nement of the abstraction allowing to achieve a higher precision is discussed. This operation recomputes only needed information to keep the abstraction sound. We also explain how to specialize the produced abstraction as a timed one and propose an algorithm to compute it based on ow-pipe construction. 2
Hybrid automata are a mean to model hybrid systems, where each state is twofold with a discrete and a continuous part [Hen96]. The discrete part ranges over a nite domain while the continuous part ranges over the Euclidean space Rn.
De nition 1 (Hybrid automaton). An n-dimensional hybrid automaton (HA) is H = (Q; X; S0; ; F; Inv; ; G; R), where:
X is a set of n real-valued variables whose valuations set is X Rn, S = Q X is the state space of H, whose elements, noted (q; x), are called states.
S0 S is the set of initial states, from which are de ned Q0 = fq j 9x (q; x) 2 S0g, the set of initial modes, and Init(q) = fx j (q; x) 2 S0g the set of initial continuous values in any initial mode q.
is a nite set of events.
F : S ! 2Rn is a mapping assigning to each state (q; x) 2 S a set F (q; x) Rn (the ow) constraining the time derivative x_ of the continuous part of the mode q by x_ 2 F (q; x).
variables in q: 8q 2 Q, fx j (q; x) 2 Sg Inv(q).
G : ! 2X assigns to each transition = (q; ; q0) 2 a nonempty guard set G( ) G( ) Inv(q).
= (q; ; q0).
One can also adopt a relational-based representation and use predicates instead of subsets. Then F (q)(x; x_ ), Inv(q)(x), G( )(x) and R( )(x; x0) being true means x_ 2 F (q; x), x 2 Inv(q), x 2 G( ) and x0 2 R( )(x) respectively. For the rest of the paper, the following is assumed: Assumption 1. Guards in any mode q will be assumed non-intersecting: 8q 2 Q; 8 1 = (q; 1; q1) 2 ; 8 2 = (q; 2; q2) 2 ; ( 1 6= 2 ) G( 1) \ G( 2) = ;).
We now introduce two practical examples of a continuous and a hybrid system that will be adopted throughout the paper.
Example 1 (Continuous System). The brusselator is a mathematical model used for representing chemical reactions with cyclic change of color. The dynamics are nonlinear. The input model holds a single mode q with singleton ow F given by the variables derivatives as:
the (x0; x1) plane) of the trajectories in the studied region are performed and observed in Figure 1. (a) (b)
mostat) modeled as a hybrid automaton with two modes on and o , whose switching is witnessed by events Bon and Bo . The continuous behaviors of each mode are illustrated in Figure 3 with some numerical simulations from randomly generated initial values.
The language of a hybrid automaton are de ned by the set of its trajectories (or semantics) de ned below. De nition 2 (HA semantics). The semantics of a HA H (also called concrete behavior), denoted by [[H]], is the set of all executions, which are labeled by L = and, 8i, (qi; xi) !li (qi+1; xi+1), one of the following is true:
[ R+: (q0; x0) l!0 (q1; x1):::(qi; xi) !li ::: such that (q0; x0) 2 S0 x 2 [80; 90] o x_ = x li = i 2 , = (qi; i; qi+1) 2 , xi 2 G( ) and xi+1 2 R( )(xi); li = di 2 R+, qi = qi+1, xi; xi+1 2 Inv(qi) and 9x : [0; di] ! X continuously di erentiable function, with x(0) = xi, x(di) = xi+1 and 8t 2 (0; di) x_ (t) 2 F (qi; x(t)) and x(t) 2 Inv(qi).
The trace of an execution h, i.e., the sequence of its labels, is a word from L? (or L! for in nite h), denoted as trace(h). We denote the total time duration of h by time(h) 2 R+ [ f+1g, which is calculated as the sum of all time periods in the trace of h: time(h) = P di. The part of execution h = (o ; 80) 0:1!5 (o ; 69) Bon ! (on; 69) 0:!5 (on; 81) Bo! (o ; 81)::: is valid for the thermostat example, thus h 2 [[H]]. Let S = Sq2Q(fqg Inv(q)) S the (in nite) set of invariant satisfying states of H, S0 S0 the subset of invariant satisfying initial states and ! S L S the transition relation de ned by De nition 2. The semantics of H is actually given by the labeled transition system SHt = (S; S0; L; !), i.e., [[H]] is the set of all paths of SHt issued from an initial state. SHt is thus a discretization of H with in nite sets of states and of transition labels. It just abstracts continuous ows by timed transitions retaining only information about the source, the target and the duration of each ow and constitutes the nest (timed) abstraction of H we will consider. The timeless abstraction of SHt is obtained by ignoring also the duration of ows and thus de ned as SH = (S; S0; [ f g; !), obtained from SHt by replacing any timed transition (qi; xi) d!i (qi+1; xi+1) with di 2 R+ by the transition (qi; xi) ! (qi+1; xi+1), that can be considered as a silent transition. It has in nite set of states but nite set of transitions labels. It constitutes the nest timeless abstraction of H we will consider.
Theorem 1 (Correctness and completeness of the semantics). Any concrete behavior of H is timed abstracted into an S0 rooted path in SHt . Conversely, any path in SHt that alternates continuous and discrete transitions (in particular any single transition) abstracts a part of a concrete behavior of H and, if F is a singleton function (i.e., deterministic derivative), any S0 rooted path in SHt abstracts a concrete behavior of H. In this latter case, there is thus no spurious abstract behavior in SHt , which expresses faithfully the behavior of H.
We now formally de ne a hybrid automata abstraction. The abstraction is obtained by partitioning the state space according to the dynamics of each mode of the hybrid system, using qualitative principles and taking into account the guard and reset conditions.
De nition 3 (Continuous space partition). A ( nite) partition P of the space Rn is a nite set of nonempty connected subsets of Rn such that every point x 2 Rn is in one and only one of those subsets. We can write Rn = Up2P p. An element p 2 P is referred to as a partition element and called a region. For a subset E of Rn, we denote by P (E) the subset of regions of P with a nonempty intersection with E.
The smoothness hypothesis we impose over a partition w.r.t. a given continuous dynamics is that any ( nite) path solution of the dynamics crosses only a nite number of times each region, more precisely, 8x : [0; 1] ! Rn a continuously di erentiable function satisfying the ow condition, 8p 2 P a region, x 1(p) is a nite union of intervals. For a HA, it is practical to allow di erent partitions in di erent modes.
De nition 4 (Hybrid state space decomposition). Given a HA H and a set P of partitions of X Rn, we say that P decomposes H if there is a surjective function d : Q ! P which associates to each q 2 Q a partition d(q) 2 P.
The continuous space partition relative to a mode contains the initial and invariant sets and the guards satis ability domains towards other modes and variables reset domains from incoming modes. For q 2 Q and = (q; ; q0) 2 , we denote the regions families d(q)(Init(q)), d(q)(Inv(q)), d(q)(G( )) by dInit(q), dInv(q), dG(q; ) d(q) and, for a region p 2 dG(q; ), we denote d(q0)(R( )(p \ G( ))) by dR(q0; ; p) d(q0). When possible, we try to de ne d such that Init(q), Inv(q), G( ) and R( )(p) are the unions of the regions in those families (if not, those regions families over-approximate them).
De nition 5 (Adjacent regions). Two distinct regions p1; p2 of a partition P of Rn are adjacent if one intersects the boundary of the other: p1 \ p2 6= ; or p1 \ p2 6= ;, where p refers to the closure of p.
De nition 6 (Decomposition-based timeless abstract automaton of a hybrid automaton). Given a hybrid automaton H = (Q; X; S0; ; F; Inv; ; G; R), and a decomposition (P; d) of H, we de ne the timeless abstract ( nite) automaton of H with respect to P as DHP = (QDH ; Q0DH ; DH ; DH ) with: • QDH = f(q; p)jq 2 Q; p 2 d(q)g. • Q0DH = f(q; pInit)jq 2 Q0; pInit 2 dInit(q)g. • DH = [ f g. • ((qi; pk); ; (qj ; pl)) 2 DH i one of the two following conditions is true: { 2 and pk 2 dG(qi; ) and pl 2 dR(qj ; ; pk) where = (qi; ; qj ) 2 . { qi = qj and = and pk; pl 2 dInv(qi) are adjacent regions and 9d 2 R+ and 9x : [0; d] ! X continuously di erentiable function such that 8t 2 (0; d) x_ (t) 2 F (qi; x(t)), 8t 2 [0; d] x(t) 2 Inv(qi), x(0) 2 pk, x(d) 2 pl, 9c 0 c d 8t 2 (0; c) x(t) 2 pk 8t 2 (c; d) x(t) 2 pl and x(c) 2 pk [ pl. abstraction of the execution h given previously in Section 2 is just o
The de ned timeless abstract automaton encodes reachability with adjacent regions of the state space, the events in witnessing mode changes and transitions representing a continuous evolution between adjacent regions in the same mode. Notice that ((qi; pk); ; (qj ; pl)) 2 DH ) 9xk 2 pk 9xl 2 pl (qi; xk) ! (qj ; xl) in SH , the converse being true for 2 . The mapping P de ned by P((q; x)) = (q; p) with p 2 d(q) and x 2 p de nes a surjective timeless abstraction function P : S ! QDH . If the ow condition F is a singleton, P maps any transition of SH to a unique path in DHP. The coarsest timeless abstract automaton is obtained when partitions of P have all a unique region p = X and is thus (Q; Q0; ; ), i.e., the discrete part of H without its continuous part. It corresponds to the coarsest timeless abstraction function ffXgg((q; x)) = q. For our previous thermostat example, this gives (fo ; ong; fo g; fBon; Bo g; f(o ; Bon ; on); (on; Bo ; o )g) and the Bo Bo!n on ! o :::
is timeless abstracted into a Q0DH rooted path in DHP and any transition of DHP abstracts a part of a concrete behavior of H. If the ow condition F is a singleton function then the timeless abstraction function P de nes a trace preserving mapping (still denoted by P) from S0 rooted paths in SH (i.e., timeless executions of H) to Q0DH rooted paths in DHP and thus the language de ned by SH is included in the language de ned by DHP.
Obviously, a path in DHP does not necessarily abstract a concrete behavior of H (as the behaviors parts abstracted by the individual transitions may not connect) which expresses that abstraction creates spurious behaviors. 4
In this section we introduce a tool that automatically computes the previously de ned abstraction of a given hybrid system. The characterization and computation of abstract states and transitions is implemented in C++. The tool requires the following freely available libraries and solvers: • The Boost libraries, mainly for parsing the hybrid automaton input model and generating graphical and textual outputs. • Nlopt, a mathematical optimization library for non linear functions. • Qepcad, for quanti er elimination using cylindrical algebraic decomposition (CAD) solver. • Matplotlib and Graphviz for visualization.
In the previous section, we formally de ned an abstraction DHP of a given hybrid system H according to a partition P. We now show the algorithms to automatically compute it. The computation can be done on the hybrid system modes separately, then a linking operation is performed between the mode abstractions. The main steps are summarized as follows: • For each mode q, compute symbolic representation of abstract states. • For each computed symbolic state st, evaluate the presence of a transition towards abstract states whose concretization is adjacent to the concretization of st.
• Apply the linkage operation. 4.1
Symbolic computation of the abstract states Partitioning rules. Consider a mode q of H. We will apply the single mode abstraction algorithm to compute an abstraction DHfd(q)g of q. In the existing literature, partitions are chosen enough regular and smooth, with regions in any dimension from 1 to n such as (from simpler to more complex) rectangles, zonotopes, polytopes and Taylor models. The choice is often guided by the dynamics and the property one wishes to verify. For example, consider a continuous system with dynamics F . A way to obtain an abstract reachability mapping would be to identify regions of the state space that preserve the sign vector of F , i.e., the derivative signs for each dimension would keep the same value (either negative or positive or null) in the same region. Thus, the regions would be the connected components of the 3n subsets Es of Rn parametrized by sign vectors s 2 f 1; 0; +1gn: Es = fx 2 X j 8i; 1 i n; x_ i < 0 if si = 1; x_ i = 0 if si = 0; x_ i > 0 if si = +1g. Note that in the case of regions expressed as polynomial inequalities, the sets conserving the sign vector are not necessarily connected, in such case we will reason over non connected sets and use invariants (Inv(q)) to separate them. Expressing abstract states. We use semi-algebraic sets to represent regions using (unions of) (in)equalities of polynomials over X. For example, if X contains two variables, we can express a circular set as: (x x0)2 + (y y0)2 < r2 with x0; y0 and r as given rational numbers. Now consider our previous brusselator example. By applying the rules of preservation of the sign vector of F , we obtain 9 abstract states illustrated as colored regions and their intersection boundaries (Figure 4.a). Notice that some generated abstract states could represent non convex sets (region 4 in Figure4a) non-connected sets (Figure 4b). To further partition algorithmically the state-space into connected sets we refer the reader to algorithms in [BPR98]. Computing the abstract states. This computation is implemented in the following way. For a mode q of the hybrid automaton, a stack Stack(q) is initialized with polynomials representing the initial and guard sets, incoming resets and dynamics. The stack is then extended as follows: each predicate from the stack is copied three times and copies are assigned +; and null symbols. The regions expressions are obtained by symbolically computing the cross product of every element in the stack with all the other elements that have a di erent predicate. The rst computation step is symbolic, thus, some regions are not feasible (i.e., are empty sets) (a) (b) example. A rst check is performed to eliminate all empty regions. This is implemented by nding whether or not there exists a solution to the semi-algebraic set representing the region. The evaluation is performed using a quanti er elimination solver applying cylindrical algebraic decomposition and will be discussed in the next section. Abstract states whose region representation admits no solution are simply discarded from the stack. Expressing a transition. Consider an abstract state st whose concrete region is expressed as a semi-algebraic set R. For each region adjacent to R, we evaluate whether some trajectories in R are to cross in bounded time to the considered neighboring region. For our previous brusselator example, consider the two regions: Each one is adjacent to the region B which is their common boundary:
R1 : 1 R2 : 1 4x0 + x20x1 > 0 ^ 3x0 4x0 + x20x1 > 0 ^ 3x0
In a general setting, we express two open regions R1 and R2 adjacent to their common boundary B (of dimension n 1) as R1 : p > 0, R2 : p < 0 and B : p = 0 where p is a polynomial (the reasoning would be the same with for example R2 closed, thus B R2, expressing R2 as p 0 and checking for transition from R2 to R1). We study the orientation of the vector eld F in B. Let ~n = @@xp be the normal vector of p, it points towards p > 0. The presence of a transition in the abstraction DHP of H is computed by evaluating the sign of the projection of F on ~n expressed by the scalar product ~n:F jx on the boundary: 9x 2 X; (p(x) = 0) ^ (~n:F jx > 0). Figure 5 illustates the case of a positive scalar product of the ow vector F with the normal vector over some boundary given by p = 0. If the formula evaluates to true then a transition is added from the abstract states of B to R1 (and also from R2 to B). The analog result holds obviously by replacing ~n:F jx > 0 by ~n:F jx < 0 and exchanging R1 and R2. The procedure is repeated for every abstract state until all transitions are computed. Note that, to be semantically correct, every mode invariant Inv(q) must be explicitly added (i.e., with a boolean ^ operator) to the transition evaluation formula.
Computing the transitions. We perform quanti er elimination using CAD over polynomials to evaluate the true or false value of each transition computed formula. Our tool is interfaced with Qepcad that implements this method [Bro03]. 4.3
Linking the single modes abstractions d(q2)(G), given region R 2 d(q2): To link the modes abstractions together, we express each region belonging to the guard condition for a jump from a mode q1 to a mode q2 in terms of the partition of mode q2. In other words, if there is no reset, we compute d(q1)(G). This is implemented by checking the satis ability of the following constraint for each 9x 2 X; d(q1)(G) ^ d(q2)(R)) (4) If satis ed, a mode change transition is thus added from region G to R. 5
In this section, experimental results are provided from several examples of continuous and hybrid systems. The presented abstractions are automatically generated using the tool. The computations are achieved on a machine equipped with an Intel Core i5-3210M CPU operating at a 2.5 Ghz frequency.
We are interested in the behavior of the brusselator in the rst quadrant of the (x0; x1) plane, thus we add to Inv(q) the constraints: x0 > 0; x1 > 0 as invariants. The system is two-dimensional, hence the computed abstraction according to ow sign vector contains 32 = 9 states. The tool successfully analyzes the example and the abstraction procedure of the model terminates in 3293 milliseconds. The produced abstraction graph is visible in Figure 6a and the computed transitions in the continuous space are illustrated in Figure 6b.
0 1 4x0 +2x20x1 < 0 3x0 x0x1 < 0
2 1 4x0 +2x20x1 < 0 3x0 x0x1 = 0
1 1 4x0 +2x20x1 < 0 3x0 x0x1 > 0
The qualitative simulation shows what behavior of the system is impossible and what behavior is possible. Using a numerical simulator, it would take a number of simulations to show the cyclic behavior of the brusselator. However Figure 6 shows that the rotation direction of the brusselator cycle cannot be counter-clockwise in a single abstraction step and without any further re nements and that is valid for any trajectory in the unbounded (x0 > 0 ^ x1 > 0) domain. Note that state 8 corresponds to the equilibrium point, i.e., in a neighborhood around state 8 no trajectories are to reach it in any time. As a result, trajectories come neither in nor out, thus no outgoing or incoming transitions are associated to state 8.
The previously introduced thermostat is abstracted using our tool within 13340 milliseconds. The abstraction is illustrated in Figure 7. Green states correspond to guard satis ability domain and the blue states are regions interpreted from the other mode and purple states are regions produced if both mode invariants were set to true.
(Mode on, Region 2) (Mode on, Region 0) (Mode on, Region 4) (Mode o , Region 4) (Mode o , Region 1) (Mode o , Region 3)
Observing the abstractions graph we can immediately see that some regions of the state space are time invariants. These regions belong to the mode switching guard condition. The abstract state of the initial set [80; 90] is region 0 in mode o . From state 0 an abstract trajectory exists, a mode change is possible to region 1 in mode on and going back to mode o is possible. The abstraction is su cient to provide a proof that regions 2 and 3 are to be crossed by the system for a mode change to happen. The arrows from the blue regions are transitions computed from the linking step that was presented in the previous section.
An aspect of the produced abstraction is that it can be applied to di erent cases of initial sets without recomputing the whole abstraction. To observe abstract trajectories from two given initial sets Init and Init0, it is only required to compute (Init) and (Init0). This aspect provides time e cient veri cation when studying the hybrid systems behaviors under varying initial sets. If the veri cation was performed numerically, the executions from each initial set should be computed separately.
Performance evaluation. It is important to note that computing the transitions can be parallelized, once the abstract states are computed for a single mode. For the moment this parallelization is not implemented in the presented tool. Parallelizing the computations will have a drastic impact on the computation time of the abstraction and will allow to handle systems with large number of modes rstly and with higher dimensions (i.e., the number of continuous variables involved). 6
The computed abstraction holds reachability information between adjacent regions, however time is not taken into account. So, for example the abstraction cannot be used to determine in how much time does a transition occur thus it cannot be used to verify temporal properties in a quantitative way. Moreover, if the abstraction is to be used for model checking for example, it would be often necessary to add more information to the abstraction for further precision. For these reasons, in this section, we de ne and discuss the re nement operations of the previously produced abstraction by taking into account time constraints. For the moment, re nement is implemented in our tool as a user guided operation however the time constraints on the abstraction is not yet implemented.
1. Find the set of regions fRcomputeg from the previous decomposition that intersect Bnew. 2. For the set of regions fRoldg that do not intersect Bnew, leave their incoming and outgoing transitions intact. Re-express these regions as Rold := Rold ^ pBnew where pBnew is the half space delimited by Bnew containing Rold. 3. Process each region Rcompute intersecting Bnew.
• Find which boundaries (in all dimensions) of Rcompute intersect Bnew. • Compute the newly obtained
regions. • Recompute the in and out transitions relative to those new regions as in Section 4.2. Re ning the abstraction consists in adding further information from the hybrid system to obtain a more precise abstraction. The idea is to split one or more regions into several regions by adding further boundaries to the decomposition. This is applied per mode of the hybrid system. What is important to notice is that many of the previously computed transitions remain valid after a re nement operation. We would only need to algorithmically check for the transitions that require to be recomputed and reevaluated.
The following are the algorithmic steps to perform for a re nement operation. Consider a new boundary region Bnew (typically of dimension n 1) to be added to the abstraction. In order to keep the abstraction sound, the following needs to be performed: Example: Consider adding a new boundary region expressed by Bnew : x1 = 4:5 to the previous decomposition of the brusselator. We illustrate this region in red on Figure 8. By simple observation, we can see that some transitions such as 0 ! 2, 2 ! 1 and 7 ! 4 remain valid in the newly considered decomposition. By applying the previous algorithm, Rcompute will contain the regions 4; 5 and 3. 6.2
Adding time A suitable representation for systems with time constraints is a particular class of hybrid systems called timed automata. In this section we introduce timed automata, propose and discuss an extension of the previous abstraction that adds time bounds associated to regions allowing for a larger class of properties to be veri ed using the timed abstraction.
Timed automata are a sub-class of hybrid automata where the continuous variables, called clocks, have all rst order derivatives equal to one, i.e., time elapses identically for all. C(X) denotes the set of constraints over a clocks set X: either primitive constraints of the form xi op ci, where ci 2 R+ and op 2 f<; ; =; ; >g, or nite conjunctions of primitive constraints. The satis ability set of a constraint is thus a rectangle in Rn+ and we identify C(X) to the set of those rectangles.
(Q; X; S0; ; F; Inv; ; G; R) such that:
S0 Q f0g, or S0 = Q0 f0g with Q0 initial modes set. =
The notation of a timed automaton T is generally simpli ed as T = (Q; X; Q0; ; Inv; ; G; Y ). The semantics [[T ]] of T as a HA can be simpli ed by merging together successive timed transitions between two discrete transitions and summing up their time period labels. An execution is thus a sequence h of alternating time steps (possibly with 0 time period) and discrete steps of the form (q0; x0) d!1 (q0; x0 + d1) !1 (q1; x1) d!2 ::: whose trace trace(h) is the timed word d1 1d2::: 2 R+( R+) and duration is time(h) = P di. Encoding reachability and time constraints. We now show how to abstract a HA into a TA that partly captures the reachability and time constraints at the level of the regions by using state space decomposition. To intuitively introduce this section, consider a partition P of the Rn state space of a continuous system with arbitrary dynamics F , the set of trajectories entering a region p 2 P is in one of these two cases: 1. either at least one of the trajectories ends up trapped inside p for all future times 2. all trajectories exit p to an adjacent region within a bounded time under the continuity assumption In the rst case, no time constraint can be associated to the region p unless a reshaping of p is applied (i.e., via a re nement operation); in the latter, it is possible to compute time constraints satis ed by all trajectories entering and leaving the region p.
De nition 8 (Region time interval and time bounds). Given a continuous system CS, a partition P of Rn and p 2 P one of its regions, we say that Ip = [tmin; tmax], with tmin; tmax 2 R+ [ f+1g, is a region time interval of p for CS if all trajectories of the CS entering p at time t leave p at time t + tmin at least and t + tmax at most. tmin and tmax are lower and upper time bounds of p.
For a hybrid automaton, we denote a time interval relative to the region p in mode q as I(q;p). De nition 9 (Decomposition-based abstract TA of a HA). Given a HA H = (Q; X; S0; ; F; Inv; ; G; R), a decomposition P of H and the timeless abstract automaton DHP = (QDH ; Q0DH ; DH ; DH ) of H with respect to P, we de ne the abstract TA of H with respect to P as T HP = (QDH ; fcg; Q0DH ; DH ; InvT H ; DH ; GT H ; YT H ) with:
InvT H ((q; p)) = [0; tmax] where I(q;p) = [tmin; tmax].
8 = ((q; p); ; (q1; p1)) 2 DH with I(q;p) = [tmin; tmax], GT H ( ) = [tmin; +1) if = and p does not intersect any reset set (i.e., 8 0 = (q0; 0; q) 2 DH p 2= d(q)(R( 0)(G( 0)))) or [0; +1) else.
8 2 DH , YT H ( ) = fcg.
The de ned abstract TA inherits the previously computed reachability relations with adjacent regions. The events in witness mode changes and transitions represent a continuous evolution between adjacent regions in the same mode. Time constraints are added to a state (q; p) for which an interval I(q;p) is computable as non-trivial (i.e., I(q;p) 6= [0; +1)), by using one local clock c (reset at 0 in each state) that measures the sojourn duration t in each state (q; p), i.e., in each region p, and coding these constraints by means of invariant and guard of c in each state. The invariant codes the maximum sojourn duration as the upper time bound of the region p and the guard codes the minimum sojourn duration as the lower time bound of the region p when both entering and leaving the region are not the result of discrete jumps (controlled here directly for the out-transition and by requiring that p does not intersect any reset set for all possible in-transitions). In the thermostat example, consider the partition into two regions associated to the mode o given by the initial state (o ; [80; 90]) and by (o ; [68; 80)). Then we take as time bounds for (o ; [80; 90]) tmin = 0 and tmax = 0:12 (the exact upper bound, i.e., the time for the temperature to decrease from 90 to 80 is Log( 98 )). Thus, we de ne in the abstract TA InvT H ((o ; [80; 90])) = [0; 0:12]. A beginning of one execution of the TA is for example (o ; [80; 90]) 0:0!8 (o ; [68; 80]). A timed abstraction of the thermostat example is illustrated in Figure 9, the timed automaton keeps the same reachability relations between regions that were previously computed while adding the assigned time bounds. To be noted that we applied a split operation in region 0 of mode o to show the initial set [80; 90] and the associated time bounds. and 0 are any strictly positive reals and are used to express the time bounds of a boundary region.
t := 0 (o ; 3)
t_ = 1
t > 0=t := 0 (o ; Init)
timed abstracted into an execution in T HP. If the ow condition F is a singleton function then the abstraction function P de nes a mapping, denoted by Pt, from S0 rooted paths in SHt (i.e., executions of H) to executions in T HP. This mapping is trace preserving once labels are erased from executions traces in T HP and time period labels are added up between two consecutive events labels in both executions traces in SHt and in T HP. This means that, for any execution (q0; x0) !w (qi; xi) 2 [[H]], with w 2 L (where L = [ R+), it exists a unique execution (q0; p0) w!0 (qj ; pj ) 2 [[T HP]], with w0 2 L0 (where L0 = L [ f g), x0 2 p0, qj = qi, xi 2 pj , wj0 = wj (where j is the projection of timed words on words on ) and, for any two successive events wl = wl00 and wm = wm00 of wj , Pl0<k0<m0;wk00 6= wk00 = Pl<k<m wk.
Computing time bounds. Now we discuss how to compute the time bounds of the hybrid system (Def. 8). Finding the exact minimum and maximum sojourn times is not always applicable. Hence, it is rather more practical to consider upper and lower bounds of these sojourn times. To nd a safe upper bound of the maximum sojourn time, the idea is to construct a ow-pipe F low of total duration N t where t is the time step and N 2 N is to be found. F low is initialized from a boundary B of a considered region p. Compute F low(B; t) is a procedure performing set integration initially starting from B and given t. We apply Algorithm 1 to obtain tmax of a region p.
Flow-pipes received considerable attention in the literature, di erent tools exist and were successful in analyzing hybrid automata from linear to polynomial dynamics [FLGD+11, CAS13]. The previous algorithm can Algorithm 1 Computing Time Bounds of a region p be optimized by not considering boundaries for which formula (1) evaluates to f alse. Obviously, unless bounded by T , termination of algorithm 1 is generally not guaranteed. One can check for conditions for which nite time bounds exist and adapt the maximum time horizon T accordingly. For example:
bounds (tmax nite, thus real nonnegative constant) is that 9i 1 i n 8x 2 p x_i 6= 0. 7
In this article, we provided a formal framework for abstracting hybrid automata into discrete-event systems, by decomposing the continuous state space into a nite number of geometric regions, and into timed automata, by adding time constraints approximating safely the sojourn time of trajectories in each region. We implemented the discrete automata abstraction computation into a tool which we tested over several examples to evaluate performances. We proposed a method to re ne the abstraction by further decomposing the state space. Our next work is to extend our tool by implementing both the time constraints computation, and thus the timed automata abstraction, and the abstraction re nement process in the framework of CEGAR (Counter-Example Guided Abstraction Re nement), both being presently done in great part manually. [BPR98]
Saugata Basu, Richard Pollack, and Marie-Francoise Roy. Complexity of computing semi-algebraic descriptions of the connected components of a semi-algebraic set. In Proceedings of the 1998 International Symposium on Symbolic and Algebraic Computation, ISSAC '98, pages 25{29, New York, NY, USA, 1998. ACM.
Christopher W Brown. QEPCAD B: a program for computing with semi-algebraic sets using CADs. ACM SIGSAM Bulletin, 37(4):97{108, 2003.
Xin Chen, Erika Abraham, and Sriram Sankaranarayanan. Flow*: An analyzer for non-linear hybrid systems. In International Conference on Computer Aided Veri cation, pages 258{263. Springer, 2013. [FLGD+11] Goran Frehse, Colas Le Guernic, Alexandre Donze, Scott Cotton, Rajarshi Ray, Olivier Lebeltel, Rodolfo Ripado, Antoine Girard, Thao Dang, and Oded Maler. SpaceEx: Scalable veri cation of hybrid systems. In International Conference on Computer Aided Veri cation, pages 379{395. Springer, 2011.
Thomas A. Henzinger. The theory of hybrid automata. In Proceedings of the 11th Annual Symposium on Logic in Computer Science (LICS), pages 278{292. IEEE Computer Society Press, 1996. Christo er Sloth and Rafael Wisniewski. Complete abstractions of dynamical systems by timed automata. Nonlinear Analysis: Hybrid Systems, 7(1):80{100, 2013.
Ashish Tiwari. Abstractions for hybrid systems. Formal Methods in Systems Design, 32:57{83, 2008. [ZYD+18] [ZYDG18]