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. The ultimate purpose is to improve the level of proof automation in KeYmaera X and other deductive verification frameworks for hybrid systems.

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 Mathematica and 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 Pegasus separately 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):

Some of the invariant generation methods currently implemented in Pegasus include:

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


Non-linear benchmark problems: A set of non-linear continuous safety verification problems (in the KeYmaera X format) on which one can test Pegasus within KeYmaera X can be obtained from: https://raw.githubusercontent.com/LS-Lab/KeYmaeraX-projects/master/benchmarks/nonlinear.kyx.

Contributors: Andrew Sogokon, Stefan Mitsch, Yong Kiam Tan, Katherine Cordwell, André Platzer.