# Sapo: Reachability Computation and Parameter Synthesis of Polynomial Dynamical Systems

arXiv: https://arxiv.org/abs/1607.02200 · HTML: https://mlsanity.com/paper/1607.02200/

## Key facts

- Cited by 3 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 8 Jul 2016.

## Built on by (most cited first, 3 of 3)

- [Neural Abstractions](https://mlsanity.com/paper/2301.11683/) (2023)
- [Attainment Regions in Feature-Parameter Space for High-Level Debugging in Autonomous Robots](https://mlsanity.com/paper/2108.03150/) (2021)
- [Learning-enabled Parameter Synthesis for Nonlinear Systems from Signal Temporal Logic](https://mlsanity.com/paper/2607.08899/) (2026)

## Abstract (arXiv)

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.