Exact and fully symbolic verification of linear hybrid automata with large discrete state spaces - Archive ouverte HAL Access content directly
Journal Articles Science of Computer Programming Year : 2012

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

(1) , (2) , (3) , (4) , (3) , (3) , (4, 5) , (1)
1
2
3
4
5

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.
Not file

Dates and versions

hal-00760387 , version 1 (03-12-2012)

Identifiers

  • HAL Id : hal-00760387 , version 1

Cite

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, 2012, 77 (10-11), pp.1122-1150. ⟨hal-00760387⟩
361 View
0 Download

Share

Gmail Facebook Twitter LinkedIn More