Advertisement

Hybridization Based CEGAR for Hybrid Automata with Affine Dynamics

  • Nima RoohiEmail author
  • Pavithra Prabhakar
  • Mahesh Viswanathan
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 9636)

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 counter-example 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 model-checking the abstract system is more expensive. Our CEGAR algorithm has been implemented in a prototype tool called \(\mathtt {HARE}\) (Hybrid Abstraction-Refinement 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 state-of-the-art safety verification tools, \(\mathtt {SpaceEx}\), \(\mathtt {PHAVer}\), \(\mathtt {SpaceEx~AGAR}\), and \(\mathtt {HSolver}\).

1 Introduction

The safety verification of cyber-physical 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 cyber-physical 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 CEGAR-based 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 state-of-the-art symbolic state space explorer for Affine Hybrid Automata that over-approximates the reachable set, and may occasionally converge to a fixpoint in the process. \(\mathtt {SpaceEx~AGAR}\) is a CEGAR-based tool that merges different locations and over-approximates their dynamics. \(\mathtt {HSolver}\) is a another CEGAR-based tool that abstracts hybrid automata into finite-state, 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 over-approximates 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 counter-example 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 counter-example 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 counter-example. The methods does not ensure counter-example 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 CEGAR-based search in [34] to find violations of safety properties. Here they consider the problem of finding a concrete counter-example and use CEGAR to guide the search of the same. We instead use CEGAR to prove safety — the absence of such concrete counter-examples.

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 non-negative rational and real numbers. For any \(n\in \mathbb {N}\) we define \([n]=\lbrace 0, 1,\ldots , n-1\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)\).

Distance and Intervals. When A and B are non-empty subsets of a normed space with norm \({\llbracket .\rrbracket }\), we define their Hausdorff distance \(\mathtt {{dist_H}}(A,B)\) by
$$\begin{aligned} \max \{\sup \limits _{a\in A}\inf \limits _{b\in B}{\llbracket a-b\rrbracket },\sup \limits _{b\in B}\inf \limits _{a\in A}\llbracket {a-b}\rrbracket \} \end{aligned}$$
An interval is any subset of real numbers of the form [ab], (ab], [ab), or (ab). We denote the set of all Intervals by \(\mathcal {I}\) and the set of all Closed-Bounded Intervals by \(\mathcal {I}_\circ \).

3.1 Hybrid Automata

In this section, we present a hybrid automaton model for representing hybrid systems.

Definition 1

A Hybrid Automaton H is a tuple \((\mathtt {Q}, {\mathtt {X}}, \mathtt {I}, \mathtt {F}, \mathtt {E}, \mathtt {Q}^\mathsf {init},\mathtt {Q}^\mathtt {bad})\), where
  • \(\mathtt {Q}\) is a finite non-empty 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 (sdgjr) 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

A Transition System T is a tuple \((\mathtt {S},\mathtt {\Sigma },\rightarrow ,\mathtt {S}^\mathsf {init},\mathtt {S}^\mathsf {bad})\) in which
  1. 1.

    \(\mathtt {S}\) is a (possibly infinite) set of states,

     
  2. 2.

    \(\mathtt {\Sigma }\) is a (possibly infinite) set of labels,

     
  3. 3.

    \(\rightarrow \subseteq \mathtt {S}\times \mathtt {\Sigma }\times \mathtt {S}\) is a transition relation,

     
  4. 4.

    \(\mathtt {S}^\mathsf {init}\subseteq \mathtt {S}\) is the set of initial states, and

     
  5. 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.

The semantics of a Hybrid Automaton \(H = (\mathtt {Q}, {\mathtt {X}}, \mathtt {I}, \mathtt {F}, \mathtt {E}, \mathtt {Q}^\mathsf {init},\mathtt {Q}^\mathtt {bad})\) can be defined as a Transition System \({\llbracket H\rrbracket }=(\mathtt {S},\mathtt {\Sigma },\rightarrow ,\mathtt {S}^\mathsf {init},\mathtt {S}^\mathsf {bad})\) in which
In this paper, we deal with two subclasses of Hybrid Automata:
  1. 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. 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_{i-1}\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.

For any Hybrid Automaton H, set of states \(S\subseteq \mathtt {S}_{\llbracket H\rrbracket }\), and edge \(e\in \mathtt {E}_H\) we define the following functions:
  • 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

Every CEGAR-based algorithm has four main parts [9]: 1. abstracting the concrete system, 2. model checking the abstract system, 3. validating the abstract counterexample, and 4. refining the abstract system. We explain parts of our algorithm regarding each of these parts in this section. Before that, Algorithm 1 shows at a very high level what the steps of our algorithm are.

4.1 Time-Bounded Transitions

A step of every CEGAR algorithm is to validate a counterexample of an abstract system returned by the model-checking 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 over-approximates 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

(Invariant Partitions). For any Hybrid Automaton C and function Open image in new window we say P partitions invariants of C iff the following conditions hold for any location \(q\in \mathtt {Q}\):

Definition 4

(Abstraction Using Invariant Partitioning). For any Affine Hybrid Automaton C and invariant partition Open image in new window , \(\alpha (C,P)\) returns Rectangular Automaton A which is defined below:
In addition, we define function \(\gamma _A\) to map 1. every state in \({\llbracket A\rrbracket }\) to a state in \({\llbracket C\rrbracket }\), and 2. every edge in \(\mathtt {E}_A\) to an edge in \(\mathtt {E}_C\). Formally, for any \(s=((q,p),\nu )\in \mathtt {S}_{\llbracket A\rrbracket }\) and \(e=((q_1,p_1),(q_2,p_2),g,j,r)\in \mathtt {E}_A\), we define \(\gamma _A(s)\) to be \((q,\nu )\) and \(\gamma _A(e)\) to be \((q_1,q_2, g,j,r)\).

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 fixed-point, we believe our tool is not considerably affected by this type of behavior.

Proposition 5

(Over-Approximation). For any Affine Hybrid Automaton C and invariant partition P, \(A = \alpha (C,P)\) is a Rectangular Automaton which over-approximates 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

An annotation for a counterexample \(\pi = e_1,\ldots ,e_n\) of Hybrid Automaton H is a sequence \(\rho = S_0\xrightarrow {}S'_0\xrightarrow {e_1}S_1\xrightarrow {}S'_1\xrightarrow {e_2}\cdots \xrightarrow {e_n}S_n\xrightarrow {}S'_n\) such that the following conditions hold:

Condition 1 means that each \(S_i\) and \(S'_i\) in \(\rho \) are a non-empty 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 over-approximation 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.

To validate \(\rho \), an annotated counterexample of \(A=\alpha (C,P)\), we run \(\rho \) on C. More precisely, we create a sequence \(\rho ' = R_0\xrightarrow {}R'_0\xrightarrow {e'_1}R_1\xrightarrow {}\cdots \xrightarrow {e'_n}R_n\xrightarrow {}R'_n\) where
Condition 1 states that edges in \(\rho '\) correspond to the edges in \(\rho \) as defined by the function \(\gamma _A\) in Definition 4. Condition 2 states that \(R_0\) is just concrete states corresponding to \(S_0\). Note that \(R_0\) is never empty. Condition 3 states that each \(R'_i\) is the intersection of two sets: 1. concrete states corresponding to abstract states in \(S'_i\), and 2. continuous post of \(R_i\). Condition 4 states that each \(R_i\) is the intersection of two sets: 1. concrete states corresponding to abstract states in \(S_i\), and 2. discrete post of \(R'_{i-1}\) using \(e'_i\). It is easy to see that for any i if \(R_i\) or \(R'_i\) becomes empty then for all \(j>i\) both \(R_j\) and \(R'_j\) will be empty. Also, if \(R_i\) is empty then \(R'_i\) is empty too. Figure 1 depicts the situation when the counterexample is spurious and \(R'_i\) is the first empty set we reach during our validation. Proposition 9 proves that the first empty set (if any) is always \(R'_i\) for some i and not \(R_i\).

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 \).

Fig. 1.

Validation and refinement. There are three locations: \(i-1\), i, and \(i+1\). \(S_{i+1}\) and \(S'_i\) are elements of annotated counterexample \(\rho \). \(R'_{i-1}\), \(R_i\), and \(\mathsf {c\mathsf {post}}_C(R_i)\) are computed when \(\rho \) is validated. i is the smallest index for which \(\mathsf {c\mathsf {post}}_C(R_i)\) and \(\gamma _A(S'_i)\) are separated. Hence we need to refine A in location i. Refinement should be done in such a way that for the result of refinement \(A'\) we have \(\mathsf {c\mathsf {post}}_{A'}(\gamma ^{-1}_{A'}(R_i))\cap \gamma _{A'}(S'_i)=\emptyset \).

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 (qp) 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 (qp) 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 (qp) 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\).

Refinement Strategy. Let \(P_r\) be an invariant partition of \(C_{q, p}\) that separates \(R_i\) from \(S'_i\). Define the invariant partition \(P'\) of C as follows: \(P'(q') = P(q')\) if \(q' \ne q\), and \(P'(q) = (P(q) \setminus \{p\}) \cup P_r(q)\). The new abstract automaton will be \(R = \alpha (C,P')\). Observe that R is a refinement of A (since the invariant partition is refined), and the relationship between the locations and edges of the two automata is characterized by a function \(\alpha _{R,A}(\cdot )\) defined as follows. For a location \((q',p')\), \(\alpha _{R,A}(q',p') = (q',p')\) if either \(q' \ne q\), or \(p' \not \subseteq p\), and \(\alpha _{R,A}(q',p') = (q,p)\) otherwise. Having defined the mapping between locations, the mapping between edges is its natural extension:
$$\begin{array}{c} \alpha _{R,A}((q_1,p_1),(q_2,p_2),g,j,r) =\\ (\alpha _{R,A}(q_1,p_1),\alpha _{R,A}(q_2,p_2),g,j,r). \end{array}$$
The goal of the refinement strategy outlined above is to ensure that a given counterexample \(\pi \) is eventually eliminated, if the abstract model checker generates it sufficiently many times. To make this statement precise and to articulate the nature of progress we need to first identify when a counterexample of R corresponds to a counterexample of A. Observe that a path \(\pi \) of A can “correspond” to a longer path \(\pi '\) in R, where previous sojourn in location (qp) in \(\pi \), now corresponds to a path in \(\pi '\) that traverses the newly created locations by partitioning p. Recall that we are assuming that \(\mathtt {por}_{C,A}(\rho ) = i\), where \(\rho \) is the annotation corresponding to \(\pi \). We will say that a counterexample \(\pi ' = e'_1,e'_2,\ldots e'_m\) corresponds to counterexample \(\pi = e_1,e_2,\ldots e_n\), if there exists k, \(0 \le k \le m-i\), such that 1. for all \(j \le i\), \(\alpha _{R,A}(e'_j) = e_j\), 2. for all \(j > i+k\), \(\alpha _{R,A}(e'_j) = e_{j-k}\), and 3. for all \(i < j \le i+k\), source and destination of \(\alpha _{R,A}(e'_j)\) is (qp). If \(\pi '\) corresponds to \(\pi \), we will call k its witness. Using this notion of correspondence, we are ready to state what our refinement achieves.

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

In order to validate a counterexample, we assumed to be able to exactly compute continuous post of a set of states in the Affine Hybrid Automaton for a finite amount of time. But the best one can actually hope for is computing over and under approximation of this set. In this section we show that being able to approximate the continuous post is enough for our algorithm. For any Hybrid Automaton H, set of states \(S\subseteq \mathtt {S}_{\llbracket H\rrbracket }\), edge \(e\in \mathtt {E}_H\), and parameter \(\epsilon \in \mathbb {R}_+\) we define the following functions:
  • \({\mathsf {c\mathsf {post}}^{\epsilon }_\mathsf {over}}(S)\) is an over-approximation 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 under-approximation 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 non-empty, 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 non-empty, 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 over-approximation 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 Automata2, 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 over-approximation of the continuous \(\mathsf {post}\) and does not have support for computing under-approximations. Therefore, currently in our tool, we stop when an abstract counterexample is validated using the over-approximation 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.

We evaluate our tool against four suites of examples that have been proposed by the community [2, 6, 17] as benchmarks for model checkers of hybrid systems. Each of these suites is qualitatively different and tests different aspects of the performance of a model checker. They are Tank, Satellite, Heater, and Navigation benchmarks.
Table 1.

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 over-approximation. Three FP. columns mean whether or not the corresponding tool reached a fixed-point in its reachability computation. No* in the FP. column of \(\mathtt {SpaceEx}\) means that the tool reached a fixed-point, 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. 1.

    The Satellite benchmark shows that \(\mathtt {HARE}\) scales up to automata with a large control structure.

     
  2. 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. 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. 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. 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 16-17, Satellite 4,11,15, and Nav 8,9,13,20 for \(\mathtt {SpaceEx}\), and Tank 16-17 for both \(\mathtt {PHAVer}\) and \(\mathtt {SpaceEx~AGAR}\). The other reason is that sometimes those three tools over-approximate 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. 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 non-linear 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 state-of-the-art 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 under-approximation 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 self-loops. Our broad future goal is to extend the hybrid abstraction refinement method for non-linear hybrid systems.

Footnotes

  1. 1.

    Note that \(\mathtt {FLOW}{^{*}}\) produces counterexamples and can even handle non-linear ODEs. But it does not support differential inclusions and therefore it is incapable of handling Rectangular Automata.

  2. 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 FA9950-15-1-0059.

References

  1. 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. 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. 3.
    Asarin, E., Maler, O., Pnueli, A.: Reachability analysis of dynamical systems having piecewise-constant derivatives. TCS 138(1), 35–65 (1995)MathSciNetCrossRefzbMATHGoogle Scholar
  4. 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. 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. 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 coarse-grained space abstractions. Int. J. Softw. Tools Technol. Transfer, October 2014Google Scholar
  7. 7.
    Bogomolov, S., Frehse, G., Greitschus, M., Grosu, R., Pasareanu, C., Podelski, A., Strump, T.: Assume-guarantee abstraction refinement meets hybrid systems. In: Yahav, E. (ed.) HVC 2014. LNCS, vol. 8855, pp. 116–131. Springer, Heidelberg (2014)Google Scholar
  8. 8.
    Chen, X., Ábrahám, E., Sankaranarayanan, S.: Flow*: an analyzer for non-linear hybrid systems. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 258–263. Springer, Heidelberg (2013)CrossRefGoogle Scholar
  9. 9.
    Clarke, E., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 154–169. Springer, Heidelberg (2000)CrossRefGoogle Scholar
  10. 10.
    Clarke, E., Fehnker, A., Han, Z., Krogh, B., Ouaknine, J., Stursberg, O., Theobald, M.: Abstraction and counterexample-guided refinement in model checking of hybrid systems. JFCS 14(4), 583–604 (2003)MathSciNetzbMATHGoogle Scholar
  11. 11.
    Clarke, E., Fehnker, A., Han, Z., Krogh, B.H., Stursberg, O., Theobald, M.: Verification of hybrid systems based on counterexample-guided abstraction refinement. In: Garavel, H., Hatcliff, J. (eds.) TACAS 2003. LNCS, vol. 2619, pp. 192–207. Springer, Heidelberg (2003)CrossRefGoogle Scholar
  12. 12.
    Corbett, J., Dwyer, M., Hatcliff, J., Laubach, S., Pasareanu, C., Robby, Z.H.: Bandera: extracting finite-state models from java source code. In: ICSE, pp. 439–448 (2000)Google Scholar
  13. 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. 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. 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. 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. 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. 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. 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. 20.
    Henzinger, T.A., Ho, P.H., Wong-Toi, H.: Hytech: a model checker for hybrid systems. Int. J. Softw. Tools Technol. Transfer (STTT) 1, 110–122 (1997)CrossRefzbMATHGoogle Scholar
  21. 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. 22.
    Henzinger, T., Jhala, R., Majumdar, R., Sutre, G.: Lazy abstraction. In: POPL 2002, pp. 58–70 (2002)Google Scholar
  23. 23.
    Holzmann, G., Smith, M.: Automating software feature verification. Bell Labs Tech. J. 5(2), 72–87 (2000)CrossRefGoogle Scholar
  24. 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. 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. 26.
    Nellen, J., Ábrahám, E., Wolters, B.: A CEGAR tool for the reachability analysis of PLC-Controlled plants using hybrid automata. In: Bouabana-Tebibel, T., Rubin, S.H. (eds.) Formalisms for Reuse and Systems Integration. AISC, vol. 346, pp. 55–78. Springer, Heidelberg (2015)Google Scholar
  27. 27.
    Prabhakar, P., Duggirala, P.S., Mitra, S., Viswanathan, M.: Hybrid automata-based 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. 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. 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. 30.
    Roohi, N., Prabhakar, P., Viswanathan, M.: Hybridization based CEGAR for hybrid automata with affine dynamics. Technical report, University of Illinois at Urbana-Champaign (2016). http://hdl.handle.net/2142/88823 Google Scholar
  31. 31.
    Segelken, M.: Abstraction and counterexample-guided construction of \(\omega \)-Automata for model checking of step-discrete linear hybrid models. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol. 4590, pp. 433–448. Springer, Heidelberg (2007)CrossRefGoogle Scholar
  32. 32.
    Sorea, M.: Lazy approximation for dense real-time systems. In: Lakhnech, Y., Yovine, S. (eds.) FORMATS 2004 and FTRTFT 2004. LNCS, vol. 3253, pp. 363–378. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  33. 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. 34.
    Zutshi, A., Deshmukh, J.V., Sankaranarayanan, S., Kapinski, J.: Multiple shooting, CEGAR-based falsification for hybrid systems. In: Proceedings of the 14th International Conference on Embedded Software (2014)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2016

Authors and Affiliations

  • Nima Roohi
    • 1
    Email author
  • Pavithra Prabhakar
    • 2
  • Mahesh Viswanathan
    • 1
  1. 1.Department of Computer ScienceUniversity of Illinois at Urbana-ChampaignIllinoisUSA
  2. 2.Department of Computing and Information SciencesKansas State UniversityManhattanUSA

Personalised recommendations