Reachability Computation and Parameter Synthesis for Polynomial Dynamical Systems

Dynamical systems are important mathematical models used to describe the temporal evolution of systems. Often dynamical systems are equipped with parameters that allow the models to better capture the characteristics of the abstracted phenomena. An important question around dynamical systems is to formally determine whether a model (biased by its parameters) behaves well. In this thesis we deal with two main questions concerning discrete-time polynomial dynamical systems: 1) the reachability computation problem, i.e, given a set of initial conditions and a set of parameters, compute the set of states reachable by the system in a bounded time horizon; 2) the parameter synthesis problem, i.e., given a set of initial conditions, a set of parameters, and a specification, find the largest set of parameters such that all the behaviors of the system staring from the set of initial conditions satisfy the specification. The reachability computation problem for nonlinear dynamical systems is well known for being nontrivial. Difficulties arise in handling and representing sets generated by nonlinear transformations. In this thesis we adopt a common technique that consists in over-approximating the complex reachable sets with sets that are easy to manipulate. The challenge is to determine accurate over-approximations. We propose methods to finely over-approximate the images of sets using boxes, parallelotopes, and a new data structure called parallelotope bundles (that are collections of parallelotopes whose intersections symbolically represent polytopes). These approximation techniques are the basic steps of our reachability algorithm. The synthesis of parameters aims at determining the values of the parameters such that the system behaves as expected. This feature can be used, for instance, to tune a model so that it imitates the modeled phenomenon with a sufficient level of precision. The contributions of this thesis concerning the parameter synthesis problem are twofold. Firstly, we define a new semantics for the Signal Temporal Logic (STL) that allows one to formalize a specification and reason on sets of parameters and flows of behaviors. Secondly, we define an algorithm to compute the synthesis semantics of a formula against a discrete-time dynamical system. The result of the algorithm constitutes a conservative solution of the parameter synthesis problem. The developed methods for both reachability computation and parameter synthesis exploit and improve Bernstein coefficients computation. The techniques defined in this thesis have been implemented in a tool called Sapo. The effectiveness of our methods is validated by the application of our tool to several polynomial dynamical system