AVERIST Algorithmic Verifier of Stability

The AVERIST tool is an algorithmic approach for stability analysis of hybrid systems. It is designed as a framework for counterexample guided abstraction refinement (CEGAR).

Currently, the processes implemented are Abstraction and Model-checking.

A CEGAR loop consists of four phases: abstraction, model-checking, validation and refinement. An abstraction of the original (concrete) system is constructed and model-checked,which either results in a stability proof or an abstract counterexample indicating a potential reason for instability. In the latter case, the abstract counterexample is analysed to either infer a bug in the concrete system or construct a finer abstraction.

• Abstraction: It is a finite state system which simulates the concrete system and preserves stability. The procedure to construct it consists of a modified predicate abstraction which results in a finite weighted graph. The absence of certain kind of cycles implies stability.


• Model-checking: It is an approach which accepts a system model and a property to verify in the system. The system model corresponds to the weighted graph and the presence of cycles with weight greater than one is the property to analyze. In case of the existence of a cycle with weight greater than one, there exist a potential reason for instability. This particular cycle is a counterexample.


• Validation: It consists of checking if the counterexample corresponds to a violation of stability in the concrete system. This can be formulated as the satisfiability of a first order logic formula over reals, obtaining instability of the concrete system or that the counterexample of the abstract system was spurious.


• Refinement: It is a procedure in order to obtain a tighter abstraction based on the counterexample. The counterexample provides the data to create a refined abstraction where such counterexample will not appear.

• The main program is implemented in Python 2.7.3.


• For the abstraction construction, for checking the concrete counterexample existence in the validation process and for computing pre and post reach sets in both validation and refinement processes, Cython wrapper is used for supporting the Parma Polyhedra Library (PPL).


• The NetworkX Python package is used for graph construction and in analysing of such graphs for stability criteria.

1. An algorithmic approach to stability verification of polyhedral switched systems, Pavithra Prabhakar and Miriam García Soto. American Control Conference (ACC), 2014.


2. Abstraction based Model-Checking of Stability of Hybrid Systems, Pavithra Prabhakar and Miriam García Soto. Computer Aided Verification (CAV), 2013.