Minopoli, Stefano (2011) Synthesis of Switching Controllers for Linear Hybrid Systems. [Tesi di dottorato] (Inedito)
Anteprima |
PDF
Minopoli_Thesis.pdf Download (1MB) | Anteprima |
| Tipologia del documento: | Tesi di dottorato |
|---|---|
| Lingua: | English |
| Titolo: | Synthesis of Switching Controllers for Linear Hybrid Systems |
| Autori: | Autore Email Minopoli, Stefano minopoli@na.infn.it |
| Data: | 30 Novembre 2011 |
| Numero di pagine: | 148 |
| Istituzione: | Università degli Studi di Napoli Federico II |
| Dipartimento: | Matematica e applicazioni "Renato Caccioppoli" |
| Scuola di dottorato: | Scienze matematiche e informatiche |
| Dottorato: | Scienze computazionali e informatiche |
| Ciclo di dottorato: | 24 |
| Coordinatore del Corso di dottorato: | nome email Burattini, Ernesto eburatti@unina.it |
| Tutor: | nome email Benerecetti, Massimo benerecetti@na.infn.it Marco, Faella faella@na.infn.it |
| Data: | 30 Novembre 2011 |
| Numero di pagine: | 148 |
| Parole chiave: | Control Theory, Automata, Hybrid Automata, Hybrid Systems, Game Theory, Verification, Synthesis |
| Settori scientifico-disciplinari del MIUR: | Area 01 - Scienze matematiche e informatiche > INF/01 - Informatica |
| Depositato il: | 09 Dic 2011 16:46 |
| Ultima modifica: | 17 Giu 2014 06:03 |
| URI: | http://www.fedoa.unina.it/id/eprint/8829 |
Abstract
This thesis is focused on the problem of automatically generating switching controllers for the class of Linear Hybrid Game, with respect to safety and reachability objectives. In order to solve the safety control problem, a sound and complete symbolic fix-point procedure on the so-called controllable predecessor operator for safety, called CPreS and based on polyhedral abstractions of the state space, are provided and the termination of each iteration is proved. Some inaccuracies contained in previous characterizations of the problem are identified and solved. In particular, this work shows that the algorithm provided by Wong-Toi [WT97] does not work in some case which are very likely to occur in practice. The error is identified in the heart of this algorithm (the operator flow avoid), and is here fixed by proposing a sound and complete procedure, based on a novel algorithm for computing, within a given location of the automaton, the may reach while avoiding operator RWAm, that is the set of states that may reach a given polyhedral region while avoiding another one. The reachability control problem for hybrid games was never considered in the literature, and the task is not trivially due the fact that, unlike classical results for discrete and real-timed case, the reachability control problem is not dual to the safety control problem. Hence, in order to solve this problem an entirely new study was necessary. This thesis proposed a sound and complete fix-point procedure based on a novel algorithm for computing, within a given location of the automaton, the set of must reach while avoiding operator RWAM, that is the set of states that must reach a given polyhedral region while avoiding another one. The theoretical results of this thesis are then effectively and efficiently implemented on the top of the open source tool PHAVer. The obtained tool, called PHAVer+, is used to present some promising experimental results at the end of this thesis.
Downloads
Downloads per month over past year
Actions (login required)
 |
Modifica documento |
