Università degli Studi di Udine OpenUniud - Archivio istituzionale delle tesi di dottorato

OpenUniud - Archivio istituzionale delle tesi di dottorato >
Udine Thesis Repository >
01 - Tesi di dottorato >

Utilizza questo identificativo per citare o creare un link a questo documento: http://hdl.handle.net/10990/681

Autori: Dreossi, Tommaso
Supervisore afferente all'Università: PIAZZA, CARLA
Supervisore non afferente all'Università: DANG, THAO
Titolo: Reachability Computation and Parameter Synthesis for Polynomial Dynamical Systems
Abstract (in inglese): 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
Parole chiave: Reachability; Parameter synthesis; Dynamical systems; Polynomials; Bernstein coefficients
MIUR : Settore INF/01 - Informatica
Lingua: eng
Data: 4-apr-2016
Corso di dottorato: Dottorato di ricerca in Informatica
Ciclo di dottorato: 28
Università di conseguimento titolo: Università degli Studi di Udine
Luogo di discussione: Udine
Ateneo di co-tutela: Université Joseph Fourier - Grenoble I
Citazione: Dreossi, T. Reachability Computation and Parameter Synthesis for Polynomial Dynamical Systems. (Doctoral Thesis, Università degli Studi di Udine, 2016).
In01 - Tesi di dottorato

Full text:

File Descrizione DimensioniFormatoConsultabilità
thesis.pdfTesi dottorato1,65 MBAdobe PDFVisualizza/apri

Tutti i documenti archiviati in DSPACE sono protetti da copyright. Tutti i diritti riservati.

Segnala questo record su




Stumble it!



  ICT Support, development & maintenance are provided by CINECA. Powered on DSpace SoftwareFeedback CINECA