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.
In order to use Pegasus, one needs to have access to Mathematica and MATLAB, as well as a working installation of KeYmaera X.
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:
SystemOpen@FileNameJoin[{$UserBaseDirectory, "Applications"}]
and extract the contents of the downloaded MATLink into the folder opened by the above command (on Unix-like systems this folder is usually /home/.Mathematica/Applications, but the value of $UserBaseDirectory varies on different systems; see documentation).
Needs["MATLink`"]
OpenMATLAB[]
/usr0/home/username/.Mathematica/Applications/SeDuMi_1_3
/usr0/home/username/.Mathematica/Applications/SOSTOOLS.303
Make sure to save your changes in order to add these folders to the path permanently.
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.
In Mathematica, an input problem for Pegasus takes the form of a continuous Hoare triple:
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:
When drawn, the invariant looks as follows (shown in light blue):