Towards Efficient Exact Synthesis for Linear Hybrid Systems

Massimo Benerecetti
(Università di Napoli "Federico II", Italy)
Marco Faella
(Università di Napoli "Federico II", Italy)
Stefano Minopoli
(Università di Napoli "Federico II", Italy)

We study the problem of automatically computing the controllable region of a Linear Hybrid Automaton, with respect to a safety objective. We describe the techniques that are needed to effectively and efficiently implement a recently-proposed solution procedure, based on polyhedral abstractions of the state space. Supporting experimental results are presented, based on an implementation of the proposed techniques on top of the tool PHAVer.

In Giovanna D'Agostino and Salvatore La Torre: Proceedings Second International Symposium on Games, Automata, Logics and Formal Verification (GandALF 2011), Minori, Italy, 15-17th June 2011, Electronic Proceedings in Theoretical Computer Science 54, pp. 263–277.
Published: 4th June 2011.

ArXived at: http://dx.doi.org/10.4204/EPTCS.54.19 bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org