Assume-Guarantee Abstraction Refinement in SpaceEx
Large systems consisting of multiple components pose a special challenge for verification algorithms. Compositional verification techniques in the assume-guarantee style have been successfully applied to transition systems to efficiently reduce the search space by leveraging the compositional nature of the systems under consideration. We adapt these techniques to the domain of hybrid systems with affine dynamics. To build assumptions we introduce an appropriate abstraction based on location merging. We integrate the assume-guarantee style analysis with automatic abstraction refinement. We have implemented our approach in the symbolic hybrid model checker SpaceEx. The evaluation shows its practical potential. To the best of our knowledge, this is the first work combining assume-guarantee reasoning with automatic abstraction-refinement in the context of hybrid automata.
Assume-guarantee reasoning is a well-known methodology for the verification of large systems. The idea behind is to decompose the verification of a system into the verification of its components, which are smaller and therefore easier to verify. The most challenging part of applying assume-guarantee reasoning is coming up with appropriate assumptions to use in the application of abstraction-refinement techniques for automating the generation of assumptions for the verification of transition systems.
In this paper, we focus on the automated generation of assumptions in the context of hybrid systems. We use abstraction-refinement techniques to iteratively build the assumptions needed to perform assume-guarantee reasoning. Let us consider a system consisting of two components (plant) and (controller). We check whether the composed system satisfies a given property . In scope of our compositional reasoning framework, we first abstract the controller by its over-approximation . If the property is not violated in the composition of and , then we can immediately conclude that also the original system is safe. Otherwise, we obtain a counterexample leading to an abstract error state. Our algorithm proceeds with the analysis of the found counterexample. If it is spurious, the abstraction is refined to eliminate it. If the counterexample is genuine, then the parallel composition violates .
We present a framework which can efficiently handle the class of affine hybrid systems. Due to the mixed discrete-continuous nature of hybrid systems, we need to pay special attention on the abstraction of continuous dynamics. We illustrate the idea of our compositional analysis on a toy example. Fig. 1 shows a simple hybrid automaton consisting of the plant and controller .
Fig. 1: A motivating example - unmerged.
We observe that the derivative of variable in plant depends on the value of governed by the controller . Furthermore, we see that the controller operates in iterations of length 10. The possible controller options are grouped in a stratum. While analyzing this system, a hybrid model checker will consider all the three options on every controller iteration which results in branches for iterations. By noting that for some properties only the minimal and maximal values of are of relevance, we come up with an abstracted version of the automaton in Fig. 2.
Fig. 2: A motivating example - merged.
We replace the three alternative options by only one coarser option. To ensure that the resulting automaton is indeed an over-approximation of the original system, we use as an invariant of the merged location , i.e., we replace the exact values of with its bounds. This abstraction will be especially useful to prove, e.g., that within the first 1000 seconds of controller operation the state will still not be reached. In the abstraction we will reduce an exponential number of branchings to a linear one. Note that this kind of location-merging abstractions is especially useful for the class of stratified controllers, i.e. consisting of multiple layers. The reason is that the controller structure can be exploited to efficiently generate an initial abstraction by merging locations belonging to the same strata. Intuitively, this step allows us to adjust the precision level at which the system parameters are taken into account. If the resulting abstraction is too coarse, then the finer grained abstraction is generated in the refinement step.
The lesson we learn from this example is that merging of locations is a promising approach to generate abstractions in scope of the assume-guarantee reasoning paradigm. To ensure the conservativeness of the resulting abstraction, we compute the invariants as a convex hull of the original locations. Note that the computation of minimal and maximal values of shown above represents a simple case of a general convex hull computation. Given the continuous, affine dynamics of the form , the merged locations are computed by first eliminating the (unprimed) state variables and consequently computing the convex hull of the resulting polytopes over the derivatives. Our implementation in SpaceEx shows the practical potential.
Click here to download the archive which has the following contents:
- 64-bit binaries of SpaceEx supporting AGAR with the necessary libraries
- Models of plants and controllers
- Scripts to run each sample
- Sergiy Bogomolov, Goran Frehse, Marius Greitschus, Radu Grosu, Corina Pasareanu, Andreas Podelski, and Thomas Strump. "Assume-Guarantee Abstraction Refinement Meets Hybrid Systems", HVC2014 [ springer | dblp | pdf ].