Exact and fully symbolic verification of linear hybrid automata with large discrete state spaces. 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.
Keywords for this software
References in zbMATH (referenced in 5 articles )
Showing results 1 to 5 of 5.
- Hagemann, Willem: Efficient geometric operations on convex polyhedra, with an application to reachability analysis of hybrid systems (2015)
- Damm, Werner; Peter, Hans-Jörg; Rakow, Jan; Westphal, Bernd: Can we build it: formal synthesis of control strategies for cooperative driver assistance systems (2013)
- Damm, Werner; Dierks, Henning; Disch, Stefan; Hagemann, Willem; Pigorsch, Florian; Scholl, Christoph; Waldmann, Uwe; Wirtz, Boris: Exact and fully symbolic verification of linear hybrid automata with large discrete state spaces (2012)
- Damm, Werner; Ihlemann, Carsten; Sofronie-Stokkermans, Viorica: PTIME parametric verification of safety properties for reasonable linear hybrid automata (2011)
- Quesel, Jan-David; Fränzle, Martin; Damm, Werner: Crossing the bridge between similar games (2011)