Hybridization Based CEGAR for Hybrid Automata with Affine Dynamics
 13 Citations
 1.2k Downloads
Abstract
We consider the problem of safety verification for hybrid systems, whose continuous dynamics in each mode is affine, \(\dot{X}=AX+b\), and invariants and guards are specified using rectangular constraints. We present a counterexample guided abstraction refinement framework (CEGAR), which abstract these hybrid automata into simpler ones with rectangular inclusion dynamics, \(\dot{x} \in \mathcal {I}\), where x is a variable and \(\mathcal {I}\) is an interval in \(\mathbb {R}\). In contrast to existing CEGAR frameworks which consider discrete abstractions, our method provides highly efficient abstraction construction, though modelchecking the abstract system is more expensive. Our CEGAR algorithm has been implemented in a prototype tool called \(\mathtt {HARE}\) (Hybrid AbstractionRefinement Engine), that makes calls to \(\mathtt {SpaceEx}\) to validate abstract counterexamples. We analyze the performance of our tool against standard benchmark examples, and show that its performance is promising when compared to stateoftheart safety verification tools, \(\mathtt {SpaceEx}\), \(\mathtt {PHAVer}\), \(\mathtt {SpaceEx~AGAR}\), and \(\mathtt {HSolver}\).
1 Introduction
The safety verification of cyberphysical systems is a computationally challenging problem that is in general undecidable [1, 3, 21, 25, 33]. Thus, verifying realistic designs often involves crafting an abstract model with simpler dynamics that is amenable to automated analysis. The success of the abstraction based method depends on finding the right abstraction, which can be difficult. One approach that tries to address this issue is the counterexample guided abstraction refinement (CEGAR) technique [9] that tries to automatically discover the right abstraction through a process of progressive refinement based on analyzing spurious counterexamples in abstract models. CEGAR has been found to be useful in a number of contexts [5, 12, 22, 23], including hybrid systems [2, 10, 11, 14, 16, 24, 31, 32].
There are two principal CEGAR approaches in the context of verifying hybrid system that differ primarily on the space of abstract models considered. The first approach [2, 10, 11, 29, 31, 32] tries to abstract hybrid models into finite state, discrete transition systems that have no continuous dynamics. The second approach [14, 24, 27] abstracts a Hybrid Automaton by another Hybrid Automaton with simpler dynamics. Using Hybrid Automata as abstractions has the advantage that constructing abstract models is computationally easier.
In this paper, we present a CEGAR framework for verifying cyberphysical systems, where the concrete and abstract models are both Hybrid Automata. We consider Hybrid Automata with Affine Dynamics and Rectangular Constraints (Affine Hybrid Automata for short) which are a subclass of Hybrid Automata, where invariants, guards, and resets are given by rectangular constraints (conjunctions of constraints comparing variables to constants), but the continuous flow in control locations is given by linear differential equations of the form \(\dot{X} = A X + b\); here X is the vector of continuous variables, A is a rational matrix, and b is a vector of rational numbers. The safety verification problem for such automata is challenging — not only is the problem undecidable, but it is even unknown whether the problem of checking if the states reachable within a time bound t (without taking any discrete transitions) intersects a polyhedral unsafe region is decidable. We abstract such Affine Hybrid Automata by Rectangular Hybrid Automata. Rectangular Hybrid Automata are similar to Affine Hybrid Automata except that the continuous dynamics is given by rectangular differential inclusions (i.e., dynamics of each variable is of the form \(\dot{x} \in [a,b]\)) as opposed to linear differential equations. Our results extend previous Hybrid Automata based CEGAR algorithms [14, 24, 27] to a richer class of hybrid models (from concrete automata that have rectangular dynamics to automata that have affine dynamics).
We establish a few basic results about our CEGAR framework. First we show that any spurious counterexample will be detected during the counterexample validation step. This result is not obvious because it is unknown whether the bounded time reachability problem is decidable for Affine Hybrid Automata. Hence validation cannot be carried out “exactly”. Our proof relies on the observation that the sets computed during counterexample validation are bounded, and uses the fact that continuous time bounded posts of Affine Hybrid Automata can be approximated with arbitrary precision. Next, we show that our refinement algorithm makes progress. More precisely, we prove that any abstract counterexample, if it appears sufficiently many times, is eventually eliminated. Progress is proved by observing that, for a bounded time, linear dynamics can be approximated with arbitrary precision by rectangular dynamics [29].
We have extended our CEGARbased tool \(\mathtt {HARE}\) (Hybrid Abstraction Refinement Engine) to verify Affine Hybrid Automata; the previous \(\mathtt {HARE}\) implementation only handled Rectangular Hybrid Automata. Furthermore, we found existing tools for model checking Rectangular Hybrid Automata (\(\mathtt {HyTech}\) [20], \(\mathtt {PHAVer}\) [18], \(\mathtt {SpaceEx}\) [19], and \(\mathtt {FLOW}{^{*}}\) [8]) inadequate for our purposes (see Sect. 5 for explanations). So we implemented a new model checker for Rectangular Hybrid Automata that uses the Parma Polyhedral Library (\(\mathtt {PPL}\)) [4] and \(\mathtt {Z3}\) [13]. Counterexample validation is carried out by making calls to \(\mathtt {SpaceEx}\) and \(\mathtt {PPL}\).
We have compared the performance of the new version of our tool \(\mathtt {HARE}\) against \(\mathtt {SpaceEx}\) with the \(\mathtt {Supp}\) and \(\mathtt {PHAVer}\) scenarios, \(\mathtt {SpaceEx~AGAR}\) [7], and \(\mathtt {HSolver}\) [29] on standard benchmark examples. \(\mathtt {SpaceEx}\) is the stateoftheart symbolic state space explorer for Affine Hybrid Automata that overapproximates the reachable set, and may occasionally converge to a fixpoint in the process. \(\mathtt {SpaceEx~AGAR}\) is a CEGARbased tool that merges different locations and overapproximates their dynamics. \(\mathtt {HSolver}\) is a another CEGARbased tool that abstracts hybrid automata into finitestate, discrete abstractions (as opposed to other hybrid automata). \(\mathtt {HSolver}\) failed to terminate within a reasonable time on almost all of our examples. The running time of \(\mathtt {HARE}\) was roughly comparable to \(\mathtt {SpaceEx}\) and \(\mathtt {SpaceEx~AGAR}\) (details in Sect. 5), with each tool beating the other on different examples. But we found that \(\mathtt {HARE}\) was more accurate. On quite a few examples, \(\mathtt {SpaceEx}\) (and \(\mathtt {SpaceEx~AGAR}\)) fails to prove safety either because it does not converge to a fixpoint or because it overapproximates the reach set too much. Due to space constrains many details have been omitted, but can be found in [30].
2 Related Work
Doyen et al. consider rectangular abstractions for safety verification of affine hybrid systems in [15]. However, their refinement is not guided by counterexample analysis. Instead, a reachable unsafe location in the abstract system is determined, and the invariant of the corresponding concrete location is split to ensure certain optimality criteria on the resulting rectangular dynamics. This, in general, may not lead to abstract counterexample elimination, as in our CEGAR algorithm. We belive that the refinement algorithms of the two papers are incomparable — one may perform better than the other on certain examples. Empirical evaluations could provide some insights into the merits of the approaches, however, the implementation of the algorithm in [15] was not available for comparison at the time of writing the paper.
Bogomolov et al. consider polyhedral inclusion dynamics as abstract models of affine hybrid systems for CEGAR in [7]. Their abstraction merges the locations, and refinement corresponds to splitting the locations. Hence, the CEGAR loop ends with the original automaton in a finite number of steps, if safety is not proved by then. Our algorithm splits the invariants of the locations, and hence, explores finer abstractions. Our method is orthogonal to that of [7], and can be used in conjunction with [7] to further refine the abstractions.
Nellen et al. use CEGAR in [26] to model check chemical plants controlled by programmable logic controllers. They assume that the dynamics of the system in each location is given by conditional ODEs, and their abstraction consists of choosing a subset of these conditional ODEs. The refinement consists of adding some of these conditional ODEs based on a unsafe location in a counterexample. The methods does not ensure counterexample elimination in successive iterations. Their prototype tool does not automate the refinement step, in that the inputs to the refinements need to be provided manually. Hence, we did not experimentally compare with this tool.
Zutshi et al. propose a CEGARbased search in [34] to find violations of safety properties. Here they consider the problem of finding a concrete counterexample and use CEGAR to guide the search of the same. We instead use CEGAR to prove safety — the absence of such concrete counterexamples.
3 Preliminaries
Numbers. Let \(\mathbb {N}\), \(\mathbb {Q}\), and \(\mathbb {R}\) denote the set of natural, rational, and real numbers, respectively. Similarly, \(\mathbb {N}_+\), \(\mathbb {Q}_+\), and \(\mathbb {R}_+\) are respectively the set of positive natural, rational, and real numbers, and \(\mathbb {Q}_{\ge 0}\) and \(\mathbb {R}_{\ge 0}\) are respectively the set of nonnegative rational and real numbers. For any \(n\in \mathbb {N}\) we define \([n]=\lbrace 0, 1,\ldots , n1\rbrace \).
Sets and Functions. For any sets A and B, \(\vert A\vert \) is the size of A (the number of elements in A), \(\mathcal P(A)\) is the power set of A, \(A\times B\) is the Cartesian product of A and B, and \([A\rightarrow B]\) is the set of all (total) functions from A to B. \(A^B\) is a vector of elements in A indexed by elements in B (we treat an element of \(A^B\) as a function from B to A). In order to make the notations simpler, for any \(n,m\in \mathbb {N}\), by \(A^n\) and \(A^{n\times m}\), we mean \(A^{[n]}\) and \(A^{[n]\times [m]}\). The latter represents matrices of dimension \(n \times m\) with elements from A. For any \(f\in [A\rightarrow B]\) and set \(C\subseteq A\), \(f(C)=\{f(c)\  \ c\in C\}\). Similarly, for any \(\pi =a_1,a_2,\ldots ,a_n\), a sequence of elements in A, we define \(f(\pi )\) to be \(f(a_1),f(a_2),\ldots ,f(a_n)\).
3.1 Hybrid Automata
In this section, we present a hybrid automaton model for representing hybrid systems.
Definition 1

\(\mathtt {Q}\) is a finite nonempty set of (discrete) locations.

\(\mathtt {X}\) is a finite set of variables. A valuation \(\nu \in \mathbb {R}^{\mathtt {X}}\) assigns a value to each variable in \({\mathtt {X}}\). We denote the set of all valuations by \(\mathtt {V}\).

\(\mathtt {I}\in [\mathtt {Q}\rightarrow \mathcal {I}_\circ ^{\mathtt {X}}]\) maps each location q to a closed bounded rectangular region as its invariant. We denote \(\mathtt {I}(q)(x)\) by \(\mathtt {I}(q,x)\).

\(\mathtt {F}\in [\mathtt {Q}\times \mathtt {V}\rightarrow \mathcal P(\mathtt {V})]\) maps each location q and valuation \(\nu \) to a set of possible derivatives of the trajectories in that location and valuation.
 \(\mathtt {E}\) is a finite set of edges e of the form (s, d, g, j, r) where:

\(s,d \in \mathtt {Q}\) are source and destination locations, respectively.

\(g\in \mathcal {I}_\circ ^{\mathtt {X}}\) is guard of e and specifies the set of possible values for each variable in order to traverse e.

\(j\in \mathcal P({\mathtt {X}})\) is the set of variables whose values change after traversing e.

\(r\in \mathcal {I}_\circ ^j\) is reset of e and specifies the set of possible values for each variable in j after traversing e.
We write \(\mathtt {S}e\), \(\mathtt {D}e\), \(\mathtt {G}e\), \(\mathtt {J}e\), and \(\mathtt {R}e\) to denote different elements of an edge e, respectively. Also we denote \((\mathtt {G}e)(x)\) and \((\mathtt {R}e)(x)\) respectively by \(\mathtt {G}(e,x)\) and \(\mathtt {R}(e,x)\).


\(\mathtt {Q}^\mathsf {init},\mathtt {Q}^\mathtt {bad}\subseteq \mathtt {Q}\) are respectively the set of initial and unsafe locations.
For all Hybrid Automata H, we display elements of H by \(\mathtt {Q}_H\), \({\mathtt {X}}_H\), \(\mathtt {I}_H\), \(\mathtt {F}_H\), \(\mathtt {E}_H\), \(\mathtt {S}_H\), \(\mathtt {D}_H\), \(\mathtt {G}_H\), \(\mathtt {J}_H\), \(\mathtt {R}_H\), \(\mathtt {Q}^\mathsf {init}_H\), \(\mathtt {Q}^\mathtt {bad}_H\), and \(\mathtt {V}_H\). We may omit the subscript when it is clear from the context.
We define the semantics of a hybrid automaton by a transition system it represents. Hence, we first define transition systems.
Definition 2
 1.
\(\mathtt {S}\) is a (possibly infinite) set of states,
 2.
\(\mathtt {\Sigma }\) is a (possibly infinite) set of labels,
 3.
\(\rightarrow \subseteq \mathtt {S}\times \mathtt {\Sigma }\times \mathtt {S}\) is a transition relation,
 4.
\(\mathtt {S}^\mathsf {init}\subseteq \mathtt {S}\) is the set of initial states, and
 5.
\(\mathtt {S}^\mathsf {bad}\subseteq \mathtt {S}\) is the set of unsafe states.
We write \(s\mathop {\rightarrow }\limits ^{\alpha }s'\) instead of \((s,\alpha ,s')\in \rightarrow \). Also, we write \(s\rightarrow s'\) as a shorthand for Open image in new window , and \(\rightarrow ^*\) denotes the reflexive transitive closure of \(\rightarrow \). Finally, for any \(s\in \mathtt {S}\) we define \(\mathsf {reach}_T(s)\) to be the set \(\{s'\in \mathtt {S}s\rightarrow ^*s'\}\), and \(\mathsf {reach}(T)\) to be \(\bigcup _{s \in \mathtt {S}^\mathsf {init}}\mathsf {reach}_T(s)\).
For all Transition Systems T, we denote the elements of T by \(\mathtt {S}_T\), \(\mathtt {\Sigma }_T\), \(\rightarrow _T\), \(\mathtt {S}^\mathsf {init}_T\), \(\mathtt {S}^\mathsf {bad}_T\). In addition, whenever it is clear, we drop the subscript T to make the notation simpler.
 1.
An Affine Hybrid Automaton is a Hybrid Automaton in which for every location \(q\in \mathtt {Q}\) there exists a matrix \(M\in \mathbb {Q}^{{\mathtt {X}}^2}\) and a vector \(b\in \mathbb {Q}^{\mathtt {X}}\) such that for every valuation \(\nu \in \mathtt {V}\) we have \(\mathtt {F}(q,\nu )=\{M\nu +b\}\). This is the class of Hybrid Automata we intend to analyse for safety.
 2.
A Rectangular Automaton is a Hybrid Automaton in which for every location \(q\in \mathtt {Q}\) there exists a rectangular region \(f\in \mathcal {I}^{\mathtt {X}}\) such that for every valuation \(\nu \in \mathtt {V}\) we have \(\mathtt {F}(q,\nu )= f\). We may write \(\mathtt {F}(q,x)\) to denote the set of possible flows for variable x at location q. We use this class to represent abstract Hybrid Automata in our CEGAR algorithm.
For a Hybrid Automaton H, a path is defined to be a finite sequence \(e_1,e_2,\ldots , e_n\) of edges in \(\mathtt {E}\) such that \(\mathtt {D}e_i =\mathtt {S}e_{i+1}\) for all \(0< i < n\). A timed path \(\pi \) is a finite sequence of the form \((t_1,e_1), (t_2,e_2), \ldots ,(t_n,e_n)\) such that \(e_1,\ldots ,e_n\) is a path in H and \(t_i\in \mathbb {R}_{\ge 0}\) for all \(0< i\le n\). A run \(\rho \) from \(s_0\) to \(s_n\) is a finite sequence \(s_0, (t_1,e_1), s_1, (t_2,e_2), \ldots , (t_n,e_n), s_n\) such that 1. \((t_1, e_1),\ldots ,(t_n, e_n)\) is a timed path in H, 2. for all \(0\le i\le n\) we have \(s_i\in \mathtt {S}_{\llbracket H\rrbracket }\), and 3. for all \(0 < i \le n\) there exists a state \(s'_i\in \mathtt {S}_{\llbracket H\rrbracket }\) for which \(s_{i1}\mathop {\longrightarrow }\limits ^{t_i}s'_i\mathop {\longrightarrow }\limits ^{e_i}s_i\). We will denote the first and last elements of \(\rho \) respectively by \(\rho _0\) and \(\rho _\mathsf {lst}\).
For any Hybrid Automaton H, the reachability problem asks whether or not H has a run \(\rho \) such that \(\rho _0\in \mathtt {S}^\mathsf {init}_{\llbracket H\rrbracket }\) and \(\rho _\mathsf {lst}\in \mathtt {S}^\mathsf {bad}_{\llbracket H\rrbracket }\). If the answer is positive, we say the H is unsafe. Otherwise, we say the H is safe.

Open image in new window . Discrete post of S in H with respect to e is the set of states reachable from S after taking e.

Open image in new window . Discrete pre of S in H with respect to e is the set of states that can reach a state in S after taking e.

Open image in new window . Continuous post of S in H is the set of states reachable from S in an arbitrary amount of time using dynamics specified for the source states.

Open image in new window . Continuous pre of S in H is the set of states that can reach a state in S in an arbitrary amount of time using dynamics specified for the source states.
4 CEGAR Algorithm for Safety Verification of Affine Hybrid Automata
4.1 TimeBounded Transitions
A step of every CEGAR algorithm is to validate a counterexample of an abstract system returned by the modelchecking phase (Sect. 4.4). We do validation by running the counterexample of the abstract model checker against the concrete Hybrid Automaton. In our discussion, we will assume that for Affine Hybrid Automata one can compute the continuous post of a set of states for an arbitrary amount of time. But this is not completely true. What we can do is to only compute approximations of the continuous post of a set of states. In addition, bounded error approximations can be computed only for a finite amount of time. Hence, we convert a Hybrid Automaton H to another Hybrid Automaton \(H'\) with the same reachability information and with the additional property that in \(H'\), there is no time transition with a label larger than t, for some parameter \(t\in \mathbb {R}_+\). With this transformation, we can compute bounded error approximations of the unbounded time post, since it is actually a continuous post over a bounded time t.
4.2 Abstraction
Input to our algorithm is an Affine Hybrid Automaton C which we call the concrete Hybrid Automaton. The first step is to construct an abstract Hybrid Automaton A which is a Rectangular Automaton. The abstract Hybrid Automaton A is obtained from the concrete Hybrid Automaton C, by splitting the invariant of any location \(q\in \mathtt {Q}_C\) into a finite number of cells of type \(\mathcal {I}_\circ ^{\mathtt {X}}\) and defining an abstract location for each of these cells which overapproximates the linear dynamics in the cell by a rectangular dynamics. Definitions 3 and 4 formalizes the way an abstraction A is constructed from C.
Definition 3
Definition 4
For each concrete location we will have one or more abstract locations. By making invariants of abstract locations small (and thus increasing the number of abstract locations) we want to be able to make behavior of A as close as required to the behavior of C. This requires trajectories to be always able to jump between two abstract locations when they correspond to a single concrete location. But we did not add any such edge to A in Definition 4. Although defining abstract system in this way just imposes an additional initial step to our algorithm, we find it very convenient not to introduce any edge in the abstract Hybrid Automata that corresponds to no edge in the concrete Hybrid Automata. Nonetheless, it is easy to see that if for every location \(q\in \mathtt {Q}_C\), \(\mathtt {E}_C\) contains a trivial edge (i.e. an edge with no guard and no reset) from q to itself, abstracting C using Definition 4 will produce a trivial edge between all abstract locations corresponding to a single concrete location. One can easily add these edges to C in an initial step, so in the rest of this paper, WLOG. we assume every location of C has a trivial self loop. Finally, it is easy to see that these trivial self loops along with Definitions 3 and 4 introduce Zeno behavior in the abstract system (i.e. the abstract system can make an infinite number of discrete transitions in a finite amount of time), but our model checker can easily handle it. In fact since we check for a fixedpoint, we believe our tool is not considerably affected by this type of behavior.
Proposition 5
(OverApproximation). For any Affine Hybrid Automaton C and invariant partition P, \(A = \alpha (C,P)\) is a Rectangular Automaton which overapproximates C, that is, Open image in new window .
It is clear that if A is safe then C is also safe. Also, one can easily see that if P is defined as \(P(q)=\lbrace \mathtt {I}_C(q)\rbrace \) (for all \(q\in \mathtt {Q}_C\)), it is a valid invariant partition of C. It is actually what our algorithm always uses as the initial invariant partitioning (initially we do not partition any invariant).
4.3 Counterexample and Model Checking Rectangular Automata
After an abstract Hybrid Automaton is constructed (initially and after any refinement), we have to model check it. In this section we define the notion of a counterexample and annotation of a counterexample, which we assume is returned by the abstract model checker \(O^\mathtt {RHA}\) when it finds that the input Hybrid Automaton is unsafe.
Definition 6
For any Hybrid Automaton H, a counterexample is a path \(e_1,\ldots ,e_n\) such that \(\mathtt {S}e_1\in \mathtt {Q}^\mathsf {init}\) and \(\mathtt {D}e_n\in \mathtt {Q}^\mathtt {bad}\).
Definition 7
A counterexample \(\pi \) is called valid in H iff H has a run \(\rho \) and \(\rho \) has the same path as \(\pi \). A counterexample that is not valid is called spurious.
Definition 8
Condition 1 means that each \(S_i\) and \(S'_i\) in \(\rho \) are a nonempty set of states. Conditions 2 and 3 mean that sets of states in \(\rho \) are computed using backward reachability. Finally, Condition 4 means that \(S'_n\) is the set of unsafe states in destination of \(e_n\). Note that these conditions completely specify \(S_0\), ..., \(S_n\) and \(S'_0,\ldots ,S'_n\) from \(e_1\), ..., \(e_n\) and H. Also, every \(S_i\) and \(S'_i\) is a subset of states corresponding to exactly one location.
In this paper, we assume to have access to an oracle \(O^\mathtt {RHA}\) that can correctly answer reachability problems when the Hybrid Automata are restricted to be Rectangular Automata. If no unsafe location of A is reachable from an initial location of it, \(O^\mathtt {RHA}(A)\) returns ‘safe’. Otherwise, it returns an annotated counterexample of A.
4.4 Validating Abstract Counterexamples
For any invariant partition P and Affine Hybrid Automaton C, if \(O^\mathtt {RHA}(A)\) (for \(A=\alpha (C,P)\)) returns ‘safe’, we know C is safe. So the algorithm returns C is ‘safe’ and terminates. On the other hand, if \(O^\mathtt {RHA}\) finds A to be unsafe it returns an annotated counterexample \(\rho \) of A. Since A is an overapproximation of C, we cannot be certain at this point that C is also unsafe. More precisely, if \(\pi \) is the path in \(\rho \), we do not know whether \(\gamma _A(\pi )\) is a valid counterexample in C or it is spurious. Therefore, we need to validate \(\rho \) in order to determine if it corresponds to any actual run from an initial location to an unsafe location in C.
Proposition 9
\(R'_n=\emptyset \) in \(\rho '\) implies there exists i such that 1. \(R'_i = \emptyset \), 2. \(R_i \ne \emptyset \), 3. Open image in new window , and 4. \(\mathsf {c\mathsf {post}}_C(R_i)\) and \(\gamma _A(S'_i)\) are nonempty disjoint sets.
Lemma 10
The counterexample \(\pi ' = e'_1, \ldots , e'_n\) of C is valid iff \(R'_n\ne \emptyset \).
Proposition 9 tells us that two sets \(\mathsf {c\mathsf {post}}_{C}(R_i)\) and \(\gamma _A(S'_i)\) are disjoint. Lemma 11 states a stronger result that there is a minimum distance \(\epsilon > 0\) between those two sets, by exploiting the compactness of the two sets.
Lemma 11
There exists \(\epsilon \in \mathbb {R}_+\) such that \(\mathtt {{dist_H}}(\mathsf {c\mathsf {post}}_C(R_i), \gamma _A(S'_i)) > \epsilon \).
4.5 Refinement
Let us fix a concrete automaton C, an invariant partition P, and an abstract automaton \(A = \alpha (C,P)\). Suppose model checking A reveals a counterexample \(\pi \) and its annotation \(\rho \). If \(\rho \) is found to be spurious by the validation algorithm (in Sect. 4.4), then we need to refine the model A by refining the invariant partition P. We will do this by refining the invariant of only a single location of A. In this section we describe how to do this.
Since \(\rho \) is spurious, there is a smallest index i such that \(R'_i = \emptyset \) (where the sets \(R_i,R'_i\) are as defined in Sect. 4.4); we will call this the point of refinement and denote it as \(\mathtt {por}_{C,A}(\rho )\). We will refine the location \((q,p) = \mathtt {D}e_i\) of A by refining its invariant p. We know from Proposition 9, \(\mathsf {c\mathsf {post}}_C(R_i) \cap \gamma _A(S'_i) = \emptyset \). However, the corresponding sets in the abstract system A are not disjoint, that is, \(\mathsf {c\mathsf {post}}_A(\gamma ^{1}_A(R_i)) \cap S'_i \not = \emptyset \). Our refinement strategy is to find a partition for the location (q, p) such that in the refined model \(R = \alpha (C,P')\) (for some \(P'\)), \(S'_i\) is not reachable from \(R_i\). In order to define the actual refinement, and to make this condition precise, we need to introduce some definitions.
Let C, A, \(R_i\), \(S'_i\), and (q, p) be as above. Let us denote by \(C_{q,p}\) the restriction of C to the single location q with invariant p, i.e., \(C_{q,p}\) has only one location q whose flow and invariant is the same as that of (q, p) in A, and only transitions whose source and destination is q. We will say that an invariant partition \(P_r\) of \(C_{q, p}\) separates \(R_i\) from \(S'_i\) iff in the automaton \(A_1 = \alpha (C_{q,p}, P_r)\), \(\mathsf {reach}_{A_1}(\gamma ^{1}_{A_1}(R_i)) \cap \gamma _{A_1}^{1}(\gamma _A(S'_i)) = \emptyset \). In other words, the states corresponding to \(S'_i\) in \(A_1\) are not reachable from \(\gamma ^{1}_{A_1}(R_i)\) in \(A_1\).
Proposition 12
Let \(\pi \) be a counterexample of A and \(\rho \) its annotation. Let R be the refinement constructed by our strategy after \(\rho \) is found to be spurious. Let \(\pi '\) be a counterexample of R that corresponds to \(\pi \), and let \(\rho '\) be its annotation. Then, \(\mathtt {por}_{C,R}(\rho ') < \mathtt {por}_{C,A}(\rho )\).
The above proposition implies that a counterexample \(\pi \) can appear only finitely many times in the CEGAR loop. This is because the point of refinement of any \(\pi '\) in R corresponding to \(\pi \) in A is strictly smaller.
Next, we claim that a partition satisfying the refinement strategy always exists. It relies on the following observation from [28] which states that the reach set of a linear dynamical system can be approximated to within any \(\epsilon \) by a rectangular hybridization over a bounded time interval.
Theorem 13
([28]). Let H be a linear hybrid automaton with a single location such that there is a bound T on the time for which the system can evolve in the location. Then, for any \(\epsilon > 0\), there exists an invariant partition P of H such that \(\mathtt {{dist_H}}(\mathsf {reach}(H), \mathsf {reach}(\alpha (H, P))) < \epsilon \).
Corollary 14
(Existence of Refinement). There always exists a partition \(P'\) that separates \(R_i\) and \(S'_i\).
4.6 Validation Approximation

\({\mathsf {c\mathsf {post}}^{\epsilon }_\mathsf {over}}(S)\) is an overapproximation of \(\mathsf {c\mathsf {post}}(S)\). Formally, if \({\mathsf {c\mathsf {post}}^{\epsilon }_\mathsf {over}}(S)\) returns \(S'\) then we know \(\mathsf {c\mathsf {post}}(S)\subseteq S'\) and \(\mathtt {{dist_H}}(S', \mathsf {c\mathsf {post}}(S))<\epsilon \).

\({\mathsf {c\mathsf {post}}^{\epsilon }_\mathsf {under}}(S)\) is an underapproximation of \(\mathsf {c\mathsf {post}}(S)\). Formally, if \({\mathsf {c\mathsf {post}}^{\epsilon }_\mathsf {under}}(S)\) returns \(S'\) then we know \(\mathsf {c\mathsf {post}}(S)\supseteq S'\) and \(\mathtt {{dist_H}}(S', \mathsf {c\mathsf {post}}(S))<\epsilon \).
During the validation procedure, instead of computing \(\rho '\) we compute \(\rho _o\) and \(\rho _u\). They are computed exactly as \(\rho '\), except that in \(\rho _o\) and \(\rho _u\), instead of \(\mathsf {c\mathsf {post}}\), we respectively use \({\mathsf {c\mathsf {post}}^{\epsilon }_\mathsf {over}}\) and \({\mathsf {c\mathsf {post}}^{\epsilon }_\mathsf {under}}\). Let us denote the last elements of \(\rho _o\) and \(\rho _u\) respectively by \(R'_n\) and \(U'_n\). If \(U'_n\) is nonempty, we know \(\rho \) represents at least one valid counterexample. Therefore, the algorithm outputs ‘unsafe’ and terminates. If \(U'_n\) is empty but \(R'_n\) is nonempty, it means \(\epsilon \) is too big. Therefore, the algorithm repeats itself using \(\frac{\epsilon }{2}\). If \(R'_n\) is empty, it means all counterexamples in \(\rho \) are spurious. Therefore, too much overapproximation is deployed in A and it needs to be refined as stated in Sect. 4.5.
Lemma 15
Given a counterexample \(\pi \) of A, if \(\gamma _A(\pi )\) is spurious, then there exists an \(\epsilon > 0\) for which \(R'_n\) is empty.
The above lemma states that if the abstract counterexample is spurious, then the same will be detected by our algorithm. This is a direct consequence of Lemma 11.
5 Experimental Results
Our tool (Hybrid Abstraction Refinement Engine or \(\mathtt {HARE}\), for short) is implemented in \(\mathtt {Scala}\). The CEGAR framework relies on a model checker that analyzes an abstract model and produce a counterexample if the abstract model violates the safety requirement. In our case this is a model checker for Rectangular Hybrid Automata that produces counterexamples. The only model checkers for Rectangular Automata that produce counterexample that we are aware of are \(\mathtt {HyTech}\) [20] and the old version of \(\mathtt {HARE}\) [27]^{1}. Unfortunately, because \(\mathtt {HyTech}\) is not being actively maintained, it does not have support for numbers of arbitrary size, and so in our experiments we frequently ran into overflow problems. Also, we decided not to use the old version of \(\mathtt {HARE}\) to model check Rectangular Automata for two reasons: 1. we wanted to only study the effects of the abstraction techniques introduced in this paper, and not have our results compromised by other simplification steps introduced in [27] like merging control locations and transitions, and ignoring variables. 2. The old version of \(\mathtt {HARE}\) internally calls \(\mathtt {HyTech}\), hence, the overflow error happens when the size of the automaton becomes large as a result of refinements. Therefore, we implemented a new model checker for Rectangular Hybrid Automata. Our implementation uses the Parma Polyhedral Library (\(\mathtt {PPL}\)) [4] to compute the discrete and continuous \(\mathsf {pre}\) in Rectangular Hybrid Automata^{2}, and \(\mathtt {Z3}\) [13] to check for fixpoints or intersection with initial states. Starting from the unsafe states, we iteratively compute \(\mathsf {pre}\) until either a fixed point is found or we reach an initial state. Both of these libraries can handle numbers of arbitrary size. Validation of counterexamples requires computing \(\mathsf {post}\)s in the concrete Affine Hybrid Automata. For discrete \(\mathsf {post}\) we use the \(\mathtt {PPL}\) library, and for the continuous \(\mathsf {post}\) we call \(\mathtt {SpaceEx}\) [19] with either \(\mathtt {Supp}\) or \(\mathtt {PHAVer}\) [18] scenario. Note that \(\mathtt {SpaceEx}\) only computes an overapproximation of the continuous \(\mathsf {post}\) and does not have support for computing underapproximations. Therefore, currently in our tool, we stop when an abstract counterexample is validated using the overapproximation implemented by \(\mathtt {SpaceEx}\). Finally, in the current implementation, in order to refine a location we simply halve its invariant along some variable at the point of refinement.
Experimental results. Columns Dim., Locs., and Trns. specify number of respectively variables (dimension), locations, and transitions in each benchmark. Five different Time columns specify amount of time each tool took to solve a problem. Times are all in seconds. ‘\(< 1\)’ means less than a second and ‘\({>}\,600\)’ means time out (more than 10 min). Also, ‘  ’ means one of the following: (1) it could not be run on \(\mathtt {HSolver}\) because of specific features the model has, (2) it could not be run on \(\mathtt {SpaceEx~AGAR}\) because we could not find any set of locations that can be merged without causing the tool to terminate unexpectedly, (3) we do not have the data because of \(\mathtt {SpaceEx~AGAR}\)’s time out. Four different Safe columns specify the output of each tool. Note that all tools perform some kind of overapproximation. Three FP. columns mean whether or not the corresponding tool reached a fixedpoint in its reachability computation. No* in the FP. column of \(\mathtt {SpaceEx}\) means that the tool reached a fixedpoint, but it also generates the following warning which invalidates the reliability of its “safe” answer: WARNING (incomplete output) Reached time horizon without exhausting all states, result is incomplete.
We ran different instances of the above examples on 4 different tools, in addition to \(\mathtt {HARE}\) — \(\mathtt {SpaceEx}\), \(\mathtt {PHAVer}\) (i.e. \(\mathtt {SpaceEx}\) using \(\mathtt {PHAVer}\) scenario), \(\mathtt {SpaceEx~AGAR}\) [7], and \(\mathtt {HSolver}\) [29]. We do not compare with the older version of \(\mathtt {HARE}\), since it implements a CEGAR algorithm for Rectangular Hybrid Automata and not for Affine Hybrid Automata.
Table 1 shows the results on some of the instances we ran the tools on. All examples were run on a laptop with Intel i5 2.50 GHz CPU, 6 GB of RAM, and Ubuntu 14.10. The salient observations, based on the experiments reported in Table 1, are summarized below.
 1.
The Satellite benchmark shows that \(\mathtt {HARE}\) scales up to automata with a large control structure.
 2.
\(\mathtt {HARE}\) often beats the \(\mathtt {SpaceEx}\) scenario in terms of proving safety or running time. For 4 problems, \(\mathtt {HARE}\) performed faster. For 3 problems both tools have the same time, but in one of them only \(\mathtt {HARE}\) proved safety. For 5 out of the remaining 7 problems in which \(\mathtt {SpaceEx}\) performed faster, only \(\mathtt {HARE}\) proved safety.
 3.
The \(\mathtt {PHAVer}\) scenario is often faster but there are cases where \(\mathtt {HARE}\) beats \(\mathtt {PHAVer}\). There are only 4 instances in which \(\mathtt {HARE}\) performed faster, but in 7 examples \(\mathtt {PHAVer}\) performed faster. Also there are 3 cases (including one in which \(\mathtt {PHAVer}\) performed faster) where only \(\mathtt {HARE}\) proved safety.
 4.
\(\mathtt {HARE}\) often beats \(\mathtt {SpaceEx~AGAR}\) in terms of proving safety or running time. In 2 problems, we could not find any two locations such that merging them does not cause \(\mathtt {SpaceEx~AGAR}\) to encounter internal error. In 7 problems, \(\mathtt {HARE}\) performed faster. In the remaining 5 problems \(\mathtt {SpaceEx~AGAR}\) performed faster, but there is one problem among them for which only \(\mathtt {HARE}\) proved safety.
 5.
In some instances, \(\mathtt {SpaceEx}\), \(\mathtt {PHAVer}\), and \(\mathtt {SpaceEx~AGAR}\) failed to prove safety while \(\mathtt {HARE}\) did not. There are two reasons for it. Sometimes those three tools fail to reach a fixpoint in the reachability computation. Examples of this are Tank 1617, Satellite 4,11,15, and Nav 8,9,13,20 for \(\mathtt {SpaceEx}\), and Tank 1617 for both \(\mathtt {PHAVer}\) and \(\mathtt {SpaceEx~AGAR}\). The other reason is that sometimes those three tools overapproximate too much. Examples of this is Nav 9 for \(\mathtt {PHAVer}\) and \(\mathtt {SpaceEx~AGAR}\). Furthermore, it seems merging locations is a very expensive task in \(\mathtt {SpaceEx~AGAR}\), which we believe is the main reason for the time outs of this tool.
 6.
On all our examples, \(\mathtt {HSolver}\) either timed out or the specific constraints in the model made them unamenable to analysis by \(\mathtt {HSolver}\). \(\mathtt {HSolver}\) is an abstraction based tool that abstracts hybrid automata into finite state, discrete transition systems. It can handle models with nonlinear dynamics, and so applies to automata more general than what \(\mathtt {HARE}\), \(\mathtt {SpaceEx}\), and \(\mathtt {PHAVer}\) analyze. This suggests that \(\mathtt {HSolver}\)’s algorithm makes certain decisions that are not effective for Affine Hybrid Automata.
6 Conclusion
We presented a new algorithm for model checking safety problems of Hybrid Automata with Affine Dynamics and Rectangular Constraints in a counterexample guided abstraction refinement framework. We show that our algorithm is sound and have implemented it in a tool named \(\mathtt {HARE}\). We also compared the performance of our tool with a few stateoftheart tools. Results show that performance of our tool is promising compared to the other tools (\(\mathtt {SpaceEx}\), \(\mathtt {PHAVer}\), and \(\mathtt {HSolver}\)).
In the future, we intend to incorporate certain improvements to our implementation. In particular, we would like to integrate an algorithm for computing an underapproximation of the continuous post. The will allow us to definitively validate abstract counterexamples. Theoretically, we would like to explore the completeness of our algorithm, in terms of finding a concrete counterexample when the concrete system is unsafe. This may require a novel notion of counterexample in the abstract system, which is shortest in terms of the number of edges in the concrete system which do not correspond to selfloops. Our broad future goal is to extend the hybrid abstraction refinement method for nonlinear hybrid systems.
Footnotes
 1.
Note that \(\mathtt {FLOW}{^{*}}\) produces counterexamples and can even handle nonlinear ODEs. But it does not support differential inclusions and therefore it is incapable of handling Rectangular Automata.
 2.
Technically, we first convert the problem of computing \(\mathsf {pre}\) to an equivalent problem of computing \(\mathsf {post}\), and then use \(\mathtt {PPL}\) to find the solution.
Notes
Acknowledgement
The authors would like to thank Sergiy Bogolomov for help with using the SpaceEx AGAR. We gratefully acknowledge the support of the following grants — Nima Roohi was partially supported by NSF CNS 1329991; Pavithra Prabhakar was partially supported by EU FP7 Marie Curie Career Integration Grant no. 631622 and NSF CAREER 1552668; and Mahesh Viswanathan was partially supported by NSF CCF 1422798 and AFOSR FA99501510059.
References
 1.Alur, R., Courcoubetis, C., Halbwachs, N., Henzinger, T.A., Ho, P.H., Nicollin, X., Olivero, A., Sifakis, J., Yovine, S.: The algorithmic analysis of hybrid systems. TCS 138(1), 3–34 (1995)MathSciNetCrossRefzbMATHGoogle Scholar
 2.Alur, R., Dang, T., Ivančić, F.: Predicate abstraction for reachability analysis of hybrid systems. ACM Trans. Embed. Comput. Syst. 5(1), 152–199 (2006)CrossRefzbMATHGoogle Scholar
 3.Asarin, E., Maler, O., Pnueli, A.: Reachability analysis of dynamical systems having piecewiseconstant derivatives. TCS 138(1), 35–65 (1995)MathSciNetCrossRefzbMATHGoogle Scholar
 4.Bagnara, R., Hill, P.M., Zaffanella, E.: The parma polyhedra library: toward a complete set of numerical abstractions for the analysis and verification of hardware and software systems. Sci. Comput. Program. 72(1–2), 3–21 (2008)MathSciNetCrossRefGoogle Scholar
 5.Ball, T., Rajamani, S.: Bebop: a symbolic model checker for boolean programs. In: Havelund, K., Penix, J., Visser, W. (eds.) SPIN 2000. LNCS, vol. 1885, pp. 113–130. Springer, Heidelberg (2000)CrossRefGoogle Scholar
 6.Bogomolov, S., Donze, A., Frehse, G., Grosu, R., Johnson, T.T., Ladan, H., Podelski, A., Wehrle, M.: Guided search for hybrid systems based on coarsegrained space abstractions. Int. J. Softw. Tools Technol. Transfer, October 2014Google Scholar
 7.Bogomolov, S., Frehse, G., Greitschus, M., Grosu, R., Pasareanu, C., Podelski, A., Strump, T.: Assumeguarantee abstraction refinement meets hybrid systems. In: Yahav, E. (ed.) HVC 2014. LNCS, vol. 8855, pp. 116–131. Springer, Heidelberg (2014)Google Scholar
 8.Chen, X., Ábrahám, E., Sankaranarayanan, S.: Flow*: an analyzer for nonlinear hybrid systems. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 258–263. Springer, Heidelberg (2013)CrossRefGoogle Scholar
 9.Clarke, E., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexampleguided abstraction refinement. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 154–169. Springer, Heidelberg (2000)CrossRefGoogle Scholar
 10.Clarke, E., Fehnker, A., Han, Z., Krogh, B., Ouaknine, J., Stursberg, O., Theobald, M.: Abstraction and counterexampleguided refinement in model checking of hybrid systems. JFCS 14(4), 583–604 (2003)MathSciNetzbMATHGoogle Scholar
 11.Clarke, E., Fehnker, A., Han, Z., Krogh, B.H., Stursberg, O., Theobald, M.: Verification of hybrid systems based on counterexampleguided abstraction refinement. In: Garavel, H., Hatcliff, J. (eds.) TACAS 2003. LNCS, vol. 2619, pp. 192–207. Springer, Heidelberg (2003)CrossRefGoogle Scholar
 12.Corbett, J., Dwyer, M., Hatcliff, J., Laubach, S., Pasareanu, C., Robby, Z.H.: Bandera: extracting finitestate models from java source code. In: ICSE, pp. 439–448 (2000)Google Scholar
 13.de Moura, L., Bjørner, N.S.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337–340. Springer, Heidelberg (2008)CrossRefGoogle Scholar
 14.Dierks, H., Kupferschmid, S., Larsen, K.G.: Automatic abstraction refinement for timed automata. In: Raskin, J.F., Thiagarajan, P.S. (eds.) FORMATS 2007. LNCS, vol. 4763, pp. 114–129. Springer, Heidelberg (2007)CrossRefGoogle Scholar
 15.Doyen, L., Henzinger, T.A., Raskin, J.F.: Automatic rectangular refinement of affine hybrid systems. In: Pettersson, P., Yi, W. (eds.) FORMATS 2005. LNCS, vol. 3829, pp. 144–161. Springer, Heidelberg (2005)CrossRefGoogle Scholar
 16.Fehnker, A., Clarke, E., Jha, S.K., Krogh, B.H.: Refining abstractions of hybrid systems using counterexample fragments. In: Morari, M., Thiele, L. (eds.) HSCC 2005. LNCS, vol. 3414, pp. 242–257. Springer, Heidelberg (2005)CrossRefGoogle Scholar
 17.Fehnker, A., Ivančić, F.: Benchmarks for hybrid systems verification. In: Alur, R., Pappas, G.J. (eds.) HSCC 2004. LNCS, vol. 2993, pp. 326–341. Springer, Heidelberg (2004)CrossRefGoogle Scholar
 18.Frehse, G.: PHAVer: algorithmic verification of hybrid systems past hytech. In: Morari, M., Thiele, L. (eds.) HSCC 2005. LNCS, vol. 3414, pp. 258–273. Springer, Heidelberg (2005)CrossRefGoogle Scholar
 19.Frehse, G., Le Guernic, C., Donzé, A., Cotton, S., Ray, R., Lebeltel, O., Ripado, R., Girard, A., Dang, T., Maler, O.: SpaceEx: scalable verification of hybrid systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 379–395. Springer, Heidelberg (2011)CrossRefGoogle Scholar
 20.Henzinger, T.A., Ho, P.H., WongToi, H.: Hytech: a model checker for hybrid systems. Int. J. Softw. Tools Technol. Transfer (STTT) 1, 110–122 (1997)CrossRefzbMATHGoogle Scholar
 21.Henzinger, T.A., Kopke, P.W., Puri, A., Varaiya, P.: What’s decidable about hybrid automata? J. Comput. Syst. Sci., 373–382 (1995)Google Scholar
 22.Henzinger, T., Jhala, R., Majumdar, R., Sutre, G.: Lazy abstraction. In: POPL 2002, pp. 58–70 (2002)Google Scholar
 23.Holzmann, G., Smith, M.: Automating software feature verification. Bell Labs Tech. J. 5(2), 72–87 (2000)CrossRefGoogle Scholar
 24.Jha, S.K., Krogh, B.H., Weimer, J.E., Clarke, E.M.: Reachability for linear hybrid automata using iterative relaxation abstraction. In: Bemporad, A., Bicchi, A., Buttazzo, G. (eds.) HSCC 2007. LNCS, vol. 4416, pp. 287–300. Springer, Heidelberg (2007)CrossRefGoogle Scholar
 25.Mysore, V., Pnueli, A.: Refining the undecidability frontier of hybrid automata. In: Sarukkai, S., Sen, S. (eds.) FSTTCS 2005. LNCS, vol. 3821, pp. 261–272. Springer, Heidelberg (2005)CrossRefGoogle Scholar
 26.Nellen, J., Ábrahám, E., Wolters, B.: A CEGAR tool for the reachability analysis of PLCControlled plants using hybrid automata. In: BouabanaTebibel, T., Rubin, S.H. (eds.) Formalisms for Reuse and Systems Integration. AISC, vol. 346, pp. 55–78. Springer, Heidelberg (2015)Google Scholar
 27.Prabhakar, P., Duggirala, P.S., Mitra, S., Viswanathan, M.: Hybrid automatabased CEGAR for rectangular hybrid systems. In: Giacobazzi, R., Berdine, J., Mastroeni, I. (eds.) VMCAI 2013. LNCS, vol. 7737, pp. 48–67. Springer, Heidelberg (2013)CrossRefGoogle Scholar
 28.Puri, A., Borkar, V.S., Varaiya, P.: \(\epsilon \)approximation of differential inclusions. In: Alur, R., Sontag, E.D., Henzinger, T.A. (eds.) HS 1995. LNCS, vol. 1066, pp. 362–376. Springer, Heidelberg (1996)CrossRefGoogle Scholar
 29.Ratschan, S., She, Z.: Safety verification of hybrid systems by constraint propagation based abstraction refinement. ACM Trans. Embed. Comput. Syst. 6(1), 573–589 (2007)CrossRefzbMATHGoogle Scholar
 30.Roohi, N., Prabhakar, P., Viswanathan, M.: Hybridization based CEGAR for hybrid automata with affine dynamics. Technical report, University of Illinois at UrbanaChampaign (2016). http://hdl.handle.net/2142/88823 Google Scholar
 31.Segelken, M.: Abstraction and counterexampleguided construction of \(\omega \)Automata for model checking of stepdiscrete linear hybrid models. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol. 4590, pp. 433–448. Springer, Heidelberg (2007)CrossRefGoogle Scholar
 32.Sorea, M.: Lazy approximation for dense realtime systems. In: Lakhnech, Y., Yovine, S. (eds.) FORMATS 2004 and FTRTFT 2004. LNCS, vol. 3253, pp. 363–378. Springer, Heidelberg (2004)CrossRefGoogle Scholar
 33.Vladimerou, V., Prabhakar, P., Viswanathan, M., Dullerud, G.E.: STORMED hybrid systems. In: Aceto, L., Damgård, I., Goldberg, L.A., Halldórsson, M.M., Ingólfsdóttir, A., Walukiewicz, I. (eds.) ICALP 2008, Part II. LNCS, vol. 5126, pp. 136–147. Springer, Heidelberg (2008)CrossRefGoogle Scholar
 34.Zutshi, A., Deshmukh, J.V., Sankaranarayanan, S., Kapinski, J.: Multiple shooting, CEGARbased falsification for hybrid systems. In: Proceedings of the 14th International Conference on Embedded Software (2014)Google Scholar