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
LORIA - FM - Department of Formal Methods , Inria Nancy - Grand Est, MPII - Max-Planck-Institut für Informatik
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.
Document type :
Journal articles
Complete list of metadatas
https://hal.inria.fr/hal-00760387
Contributor : Stephan Merz <>
Submitted on : Monday, December 3, 2012 - 6:45:51 PM
Last modification on : Tuesday, February 19, 2019 - 3:40:03 PM

Identifiers

  • HAL Id : hal-00760387, version 1

Collections

CNRS | 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⟩

Export

BibTeX TEI DC DCterms EndNote

Share

Metrics

Record views

495

 

 

Contact

archive-ouverte@inria.fr