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 systems
