Exact and fully symbolic verification of linear hybrid automata with large discrete state spaces

Werner Damm 1 Henning Dierks 2 Stefan Disch 3 Willem Hagemann 4 Florian Pigorsch 3 Christoph Scholl 3 Uwe Waldmann 4, 5 Boris Wirtz 1
1 Department für Informatik [Oldenburg]
2 Hochschule für Angewandte Wissenschaften
3 Albert-Ludwigs-Universität Freiburg
4 MPII - Max-Planck-Institut für Informatik
5 VERIDIS - Modeling and Verification of Distributed Algorithms and Systems
Inria Nancy - Grand Est, LORIA - FM - Department of Formal Methods
Abstract : We propose an improved symbolic algorithm for the verification of linear hybrid automata with large discrete state spaces (where an explicit representation of discrete states is difficult). Here both the discrete part and the continuous part of the hybrid state space are represented by one symbolic representation called LinAIGs. LinAIGs represent (possibly non-convex) polyhedra extended by Boolean variables. Key components of our method for state space traversal are redundancy elimination and constraint minimization: redundancy elimination eliminates so-called redundant linear constraints from LinAIG representations by a suitable exploitation of the capabilities of SMT (Satisfiability Modulo Theories) solvers. Constraint minimization optimizes polyhedra by exploiting the fact that states already reached in previous steps can be interpreted as "don't cares" in the current step. Experimental results (including comparisons to the state-of-the-art model checkers PHAVer and RED) demonstrate the advantages of our approach.
Type de document :
Article dans une revue
Science of Computer Programming, Elsevier, 2012, 77 (10-11), pp.1122-1150
Liste complète des métadonnées
https://hal.inria.fr/hal-00760387
Contributeur : Stephan Merz <>
Soumis le : lundi 3 décembre 2012 - 18:45:51
Dernière modification le : vendredi 21 septembre 2018 - 19:18:01

Identifiants

  • HAL Id : hal-00760387, version 1

Collections

INRIA | UNIV-LORRAINE | LORIA-FM | LORIA

Citation

Werner Damm, Henning Dierks, Stefan Disch, Willem Hagemann, Florian Pigorsch, et al.. Exact and fully symbolic verification of linear hybrid automata with large discrete state spaces. Science of Computer Programming, Elsevier, 2012, 77 (10-11), pp.1122-1150. 〈hal-00760387〉

Exporter

BibTeX TEI DC DCterms EndNote

Partager

Métriques

Consultations de la notice

238

Contact


archive-ouverte@inria.fr