A tool for generating inductive invariants for continuous systems

Pegasus is a tool for generating continuous invariants for systems described by polynomial ordinary differential equations. It is integrated with the KeYmaera X theorem prover for hybrid systems and implements a number of methods for invariant generation. Pegasus provides a framework for combining techniques for invariant generation into more powerful strategies. Its ultimate purpose is to improve the level of proof automation in KeYmaera X and other deductive verification frameworks for hybrid systems.

System requirements and installation guidelines

In order to use Pegasus, one needs to have access to Mathematica and MATLAB, as well as a working installation of KeYmaera X.

Installation instructions

Pegasus is implemented in Wolfram Language and runs inside Mathematica; it is (optionally) able to make use of MATLAB for additional computations. The simplest way to get started is:

To enable additional Pegasus functionality with MATLAB, additional packages are required.

Running with KeYmaera X

Pegasus ships with KeYmaera X and is used automatically in some parts of the proof automation. In order to discover the right proof and controllers you can also use Tools→Find ODE Invariant Candidates. Keep in mind that the version of Pegasus that ships with KeYmaera X gets better when installing the additional software such as MATLab etc.

Running Pegasus separately

Using Pegasus as a standalone tool can be achieved by navigating to keymaerax-core/src/main/resources/Pegasus inside the folder containing the KeYmaera X source directory. The file Pegasus.m serves as the main package from which invariant generation strategies may be called. Various examples of invariant generation using this file are contained in the Tests/ sub-folder. Keep in mind that by running Pegasus separately using Mathematica one only obtains invariant candidates, whereas KeYmaera X additionally formally proves the invariance property of these candidates.

In Mathematica, an input problem for Pegasus takes the form of a continuous Hoare triple:

{precondition, {vector_field, state_variables, evolution_constraint}, postcondition}

where precondition, postcondition and evolution_constraint are first-order formulas of real arithmetic, state_variables is a finite list of the system's state variables (e.g. {x,y,z}), and vector_field is a list of equal size containing polynomials in those variables (corresponding to the right-hand side of the system of ODEs). For instance, when calling from a notebook file in the Test/ sub-folder in the Pegasus main directory:

In[1] = SetDirectory[ParentDirectory[NotebookDirectory[]]]
In[2] = Needs["Pegasus`", FileNameJoin[{Directory[], "Pegasus.m"}]]
In[3] = InvGen[{(-2 + x)^2 + y^2 <= 1/5 || (2 + x)^2 + (-2 + y)^2 <= 1/3, {{-4 y, x}, {x, y}, True}, y <= 4 && y >= -4 && x^2 + y^2 > 1/3}]

In the illustration of this verification problem below, the unsafe sets are shown in light red and the initial states in light green:

The output is a nested list, whose first formal entry is the invariant candidate (other entries in the list serve to facilitate proof construction within KeYmaera X and may be ignored when using Pegasus separately).

Out[4] = {{106345581/44105831 < x^2+4 y^2 < 784012261/25449817,{{x^2+4 y^2 < 784012261/25449817,kyx`ProofHint==kyx`FirstIntegral},{x^2+4 y^2 > 106345581/44105831,kyx`ProofHint==kyx`FirstIntegral}}},True}

When drawn, the invariant looks as follows (shown in light blue):