Minopoli, Stefano
(2011)
Synthesis of Switching Controllers for Linear Hybrid Systems.
[Tesi di dottorato]
(Inedito)
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 scientificodisciplinari 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 fixpoint procedure on the socalled 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 WongToi [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 realtimed 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 fixpoint 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.
Actions (login required)

Modifica documento 