Synthesis of Switching Controllers for Linear Hybrid Systems

Minopoli, Stefano (2011) Synthesis of Switching Controllers for Linear Hybrid Systems. [Tesi di dottorato] (Inedito)

Full text disponibile come:

[img]PDF - Solo per gli Amministratori dell'archivio fino a 13 Febbraio 2013 - Richiede un editor Pdf del tipo GSview, Xpdf o Adobe Acrobat Reader
1518Kb

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.

Tipologia di documento:Tesi di dottorato
Parole chiave:Control Theory, Automata, Hybrid Automata, Hybrid Systems, Game Theory, Verification, Synthesis
Settori scientifico-disciplinari MIUR:Area 01 Scienze matematiche e informatiche > INF/01 INFORMATICA
Coordinatori della Scuola di dottorato:
Coordinatore del Corso di dottoratoe-mail (se nota)
Burattini, Ernestoeburatti@unina.it
Tutor della Scuola di dottorato:
Tutor del Corso di dottoratoe-mail (se nota)
Benerecetti, Massimobenerecetti@na.infn.it
Marco, Faellafaella@na.infn.it
Stato del full text:Inedito
Data:30 Novembre 2011
Numero di pagine:148
Istituzione:Università di Napoli Federico II
Dipartimento o Struttura:Matematica e applicazioni "R. Caccioppoli"
Stato dell'Eprint:Inedito
Scuola di dottorato:Scienze matematiche ed informatiche
Denominazione del dottorato:Scienze computazionali e informatiche
Ciclo di dottorato:24
Numero di sistema:8829
Depositato il:09 Dicembre 2011 17:46
Ultima modifica:24 Aprile 2012 09:41

Solo per gli Amministratori dell'archivio: edita il record