Sapo: Reachability Computation and Parameter Synthesis of Polynomial Dynamical Systems
Systems and Control
2016-07-11 v1
Abstract
Sapo is a C++ tool for the formal analysis of polynomial dynamical systems. Its main features are: 1) Reachability computation, i.e., the calculation of the set of states reachable from a set of initial conditions, and 2) Parameter synthesis, i.e., the refinement of a set of parameters so that the system satisfies a given specification. Sapo can represent reachable sets as unions of boxes, parallelotopes, or parallelotope bundles (symbolic representation of polytopes). Sets of parameters are represented with polytopes while specifications are formalized as Signal Temporal Logic (STL) formulas.
Cite
@article{arxiv.1607.02200,
title = {Sapo: Reachability Computation and Parameter Synthesis of Polynomial Dynamical Systems},
author = {Tommaso Dreossi},
journal= {arXiv preprint arXiv:1607.02200},
year = {2016}
}