Invariant generation methods

As of version 1.0 Pegasus implements a number of methods for generating inductive invariants for continuous systems.

Barrier certificates

The method of barrier certificates is a popular and promising technique for safety verification of continuous systems. It employs Lyapunov-like differential inequalities and typically requires a polynomial template which is then transformed into a constraint problem in the template coefficient variables. If the constraint is feasible, a real-valued polynomial B ( x ) can be synthesized from the feasible point, with the property that B ( x ) 0 defines a continuous invariant of the system which separates the initial states of the system from states that are deemed unsafe. There are many different flavors of barrier certificates in the verification literature. A systematic development of the barrier certificate method and its integration with a sound theorem proving system is one of the goals behind developing Pegasus. As part of this effort, a generalization called vector barrier certificates was developed at the Logical Systems Lab in collaboration with Inria, which is based on the theory of comparison systems and serves to organize existing notions of barrier certificates under a unified framework.

Darboux polynomials

Polynomials p satisfying the differential equation p ' = α p where α is also a polynomial are known as Darboux polynomials, named after Gaston Darboux who introduced them as a tool to study integrability.

First integrals

First integrals, also known as conserved quantities, or constants of motion, are functions of state whose value remains constant as the system evolves. In other words, a first integral is a function whose time derivative is zero. In general, first integrals can be very complicated functions and can be extremely difficult to find. However, searching for polynomial first integrals is straightforward and can be achieved using a polynomial template and a solver for systems of linear equations.

Qualitative abstraction

Qualitative abstraction of continuous systems is related to predicate abstraction. It produces a discrete abstraction by partitioning the state space of a continuous system using predicates that represent significant ``qualitative information'' about the system. If the set of predicates used for the abstraction is ``good'', many interesting properties about the behavior of the continuous system may be proved. The idea of qualitative abstraction originally emerged in the field of Artificial Intelligence in the 1980s and was used for qualitative simulation and qualitative reasoning about physical systems. Later work in this field in the 1990s considered verification of termporal properties of physical systems as an application of this technique. Within the verification community, qualitative abstraction was advanced in the work of A. Tiwari and was employed in tools such as HybridSAL from SRI International to enable model checking hybrid systems.

Strategies for invariant generation

Pegasus implements strategies that generate invariants by combining invariant generation methods in a differential saturation loop, refining the evolution constraint at each step.