Home

Sapo is a tool for the formal analysis of discrete-time polynomial dynamical systems.

The problems treated by Sapo are:

• Reachability computation, i.e., the calculation of the set of states reachable by the system from a set of initial conditions
• Parameter synthesis, i.e., the refinement of a set of parameters so that the system satisfies a given specification. For reachability analysis Sapo produces a flowpipe that over-approximates the set of states reachable by the system from a set of initial conditions.

For parameter synthesis Sapo computes a refinement of the given set of parameters such that the system satisfies a given specification. The specification is formalized as a Signal Temporal Logic (STL) formula.

In both cases, the analysis can be done on bounded time.

Sapo consists in a C++ library, named libSapo, and an optional command line application, named sapo, that is meant to ease Sapo usability.

A web user interface for Sapo is available here.

Models

The dynamical systems supported by Sapo are discrete-time polynomial dynamical systems, i.e., dynamical systems whose evolutions can be described by difference equations of the form .

Reachability computation can be carried out also on systems without parameters whose dynamics look like with polynomial.

Set representation

The flowpipe representing the reachable set consists in a series of sets. The sets supported by Sapo are:

• Boxes (or hyperrectangles), i.e., n-dimensional rectangles
• Parallelotopes, i.e., n-dimensional parallelograms
• Parallelotopes bundles, i.e., finite sets of parallelotopes whose intersections generate polytopes

The parameter synthesis produces a refined set of parameters represented by:

• Polytopes, i.e., n-dimensional polygon