SapoDescriptionSapo is a C++ tool for the formal analysis of discretetime polynomial dynamical systems. The problems treated by Sapo are:
For reachability analysis Sapo produces a flowpipe that overapproximates 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. ModelsThe dynamical systems supported by Sapo are discretetime polynomial dynamical systems, i.e., dynamical systems whose evolutions can be described by difference equations of the form: where is a polynomial and is the set of the reals. Reachability computation can be carried out also on systems without parameters whose dynamics look like with polynomial. Set representationThe flowpipe representing the reachable set consists in a series of sets. The sets supported by Sapo are:
The parameter synthesis produces a refined set of parameters represented by:
