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

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 : jeudi 11 janvier 2018 - 06:23:13

Identifiants

  • HAL Id : hal-00760387, version 1

Collections

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〉

Partager

Métriques

Consultations de la notice

144