×

Exact and fully symbolic verification of linear hybrid automata with large discrete state spaces. (English) Zbl 1243.68212

Summary: 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.

MSC:

68Q60 Specification and verification (program logics, model checking, etc.)
68Q45 Formal languages and automata
68W30 Symbolic computation and algebraic computation
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Damm, W.; Disch, S.; Hungar, H.; Pang, J.; Pigorsch, F.; Scholl, C.; Waldmann, U.; Wirtz, B.: Automatic verification of hybrid systems with large discrete state space, Lncs 4218, 276-291 (2006) · Zbl 1161.68562 · doi:10.1007/11901914_22
[2] Damm, W.; Disch, S.; Hungar, H.; Jacobs, S.; Pang, J.; Pigorsch, F.; Scholl, C.; Waldmann, U.; Wirtz, B.: Exact state set representations in the verification of linear hybrid systems with large discrete state space, Lncs 4762, 425-440 (2007) · Zbl 1141.68461 · doi:10.1007/978-3-540-75596-8_30
[3] Scholl, C.; Disch, S.; Pigorsch, F.; Kupferschmid, S.: Computing optimized representations for non-convex polyhedra by detection and removal of redundant linear constraints, Lncs 5505, 383-397 (2009) · Zbl 1234.68266
[4] Segelken, M.: Abstraction and counterexample-guided construction of \({\omega}\)-automata for model checking of step-discrete linear hybrid models, Lncs 4590, 433-448 (2007) · Zbl 1135.68482 · doi:10.1007/978-3-540-73368-3_46
[5] B.I. Silva, K. Richeson, B.H. Krogh, A. Chutinan, Modeling and verification of hybrid dynamical system using CheckMate, in: 4th Conference on Automation of Mixed Processes, 2000.
[6] Henzinger, T. A.; Ho, P. -H.; Wong-Toi, H.: Hytech: a model checker for hybrid systems, Software tools for technology transfer 1, No. 1–2, 110-122 (1997) · Zbl 1060.68603 · doi:10.1007/s100090050008
[7] Frehse, G.: Phaver: algorithmic verification of hybrid systems past hytech, International journal on software tools for technology transfer (STTT) 10, No. 3, 263-279 (2008)
[8] Asarin, E.; Dang, T.; Maler, O.: The d/dt tool for verification of the hybrid systems, Lncs 2404, 365-370 (2002) · Zbl 1010.68796
[9] Mcmillan, K. L.: Symbolic model checking, (1993) · Zbl 0784.68004
[10] Group, The Vis: VIS: a system for verification and synthesis, Lncs 1102, 428-432 (1996)
[11] Dutertre, B.; De Moura, L.: A fast linear-arithmetic solver for \(DPLL(T)\), Lncs 4144, 81-94 (2006)
[12] Bruttomesso, R.; Cimatti, A.; Franzen, A.; Griggio, A.; Sebastiani, R.: The mathsat 4 SMT solver, Lncs, 299-303 (2008)
[13] Loos, R.; Weispfenning, V.: Applying linear quantifier elimination, The computer journal 36, No. 5, 450-462 (1993) · Zbl 0787.03021 · doi:10.1093/comjnl/36.5.450
[14] Craig, W.: Three uses of the Herbrand–gentzen theorem in relating model theory and proof theory, Journal on symbolic logic 22, No. 3, 269-285 (1957) · Zbl 0079.24502 · doi:10.2307/2963594
[15] Pudlák, P.: Lower bounds for resolution and cutting plane proofs and monotone computations, Journal on symbolic logic 62, No. 3, 981-998 (1997) · Zbl 0945.03086 · doi:10.2307/2275583
[16] Mcmillan, K. L.: Interpolation and SAT-based model checking, Lncs 2725, 1-13 (2003) · Zbl 1278.68184
[17] C.-C. Lee, J.-H.R. Jiang, C.-Y. Huang, A. Mishchenko, Scalable exploration of functional dependency by interpolation and incremental SAT solving, in: ICCAD, 2007, pp. 227–233.
[18] Coudert, O.; Berthet, C.; Madre, J. C.: Verification of synchronous sequential machines based on symbolic execution, Lncs 407, 365-373 (1989)
[19] O. Coudert, J.C. Madre, A unified framework for the formal verification of sequential circuits, in: Int’l Conf. on CAD, 1990, pp. 126–129.
[20] Burch, J. R.; Clarke, E. M.; Mcmillan, K. L.; Dill, D. L.; Hwang, J.: Symbolic model checking: 1020 states and beyond, , 428-439 (1990) · Zbl 0753.68066
[21] Beyer, D.; Noack, A.: Can decision diagrams overcome state space explosion in real-time verification?, Lecture notes in computer science 2767, 193-208 (2003) · Zbl 1279.68196
[22] Wang, F.: Symbolic parametric safety analysis of linear hybrid systems with BDD-like data-structures, IEEE transactions on software engineering 31, No. 1, 38-52 (2005)
[23] Frehse, G.: Phaver: algorithmic verification of hybrid systems past hytech, Lncs 3414, 258-273 (2005) · Zbl 1078.93533 · doi:10.1007/b106766
[24] G. Frehse, Compositional verification of hybrid systems using simulation relations, Ph.D. Thesis, Radboud Universiteit Nijmegen, 2005. · Zbl 1078.93533
[25] Girard, A.; Pappas, G. J.: Approximation metrics for discrete and continuous systems, IEEE transactions on automatic control 52, No. 5, 782-798 (2007) · Zbl 1366.93032
[26] Damm, W.; Pinto, G.; Ratschan, S.: Guaranteed termination in the verification of LTL properties of non-linear robust discrete time hybrid systems, Lncs 3707, 99-113 (2005) · Zbl 1170.68511 · doi:10.1007/11562948
[27] Agrawal, M.; Thiagarajan, P. S.: Lazy rectangular hybrid automata, Lncs 2993, 1-15 (2004) · Zbl 1133.68359 · doi:10.1007/b96398
[28] Agrawal, M.; Thiagarajan, P. S.: The discrete time behavior of lazy linear hybrid automata, Lncs 3414, 55-69 (2005) · Zbl 1078.68069 · doi:10.1007/b106766
[29] Platzer, A.; Clarke, E.: The image computation problem in hybrid systems model checking, Lncs 4416, 473-486 (2007) · Zbl 1221.93118 · doi:10.1007/978-3-540-71493-4_37
[30] S. Jha, B. Brady, S. Seshia, Symbolic reachability analysis of lazy linear hybrid automata, Tech. Rep., EECS Dept., UC Berkeley, 2007. · Zbl 1141.93352
[31] Asarin, E.; Dang, T.; Girard, A.: Hybridization methods for the analysis of non-linear systems, Acta informatica 43, No. 7, 451-476 (2007) · Zbl 1134.93026 · doi:10.1007/s00236-006-0035-7
[32] Henzinger, T. A.: The theory of hybrid automata, , 278-292 (1996) · Zbl 0959.68073
[33] Benveniste, A.; Berry, G.: The synchronous approach to reactive and real-time systems, Proceedings of the IEEE 79, No. 9, 1270-1282 (1991)
[34] A. Mishchenko, S. Chatterjee, R. Jiang, R.K. Brayton, FRAIGs: a unifying representation for logic synthesis and verification, Tech. Rep., EECS Dept., UC Berkeley, 2005.
[35] Pigorsch, F.; Scholl, C.; Disch, S.: Advanced unbounded model checking by using aigs, BDD sweeping and quantifier scheduling, , 89-96 (2006)
[36] F. Pigorsch, C. Scholl, Exploiting structure in an AIG based QBF solver, in: Conf. on Design, Automation and Test in Europe, 2009, pp. 1596–1601.
[37] F. Pigorsch, C. Scholl, An AIG-based QBF-solver using SAT for preprocessing, in: Design Automation Conference, 2009.
[38] A. Dolzmann, Algorithmic strategies for applicable real quantifier elimination, Ph.D. Thesis, Universität Passau, 2000.
[39] Hoare, C. A. R.: An axiomatic basis for computer programming, Communication of the ACM 12, 576-583 (1969) · Zbl 0179.23105 · doi:10.1145/363235.363259
[40] Alur, R.; Henzinger, T. A.; Ho, P. -H.: Automatic symbolic verification of embedded systems, IEEE transactions on software engineering 22, No. 3, 181-201 (1996)
[41] F. Pigorsch, C. Scholl, Using implications for optimizing state set representations of linear hybrid systems, in: GI/ITG/GMM Workshop Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen, 2009, pp. 77–86.
[42] Aho, A. V.; Garey, M. R.; Ullman, J. D.: The transitive reduction of a directed graph, SIAM journal on computing 1, No. 2, 131-137 (1972) · Zbl 0247.05128 · doi:10.1137/0201008
[43] Sebastiani, R.: Lazy satisability modulo theories, Jsat 3, 141-224 (2007) · Zbl 1145.68501
[44] Tseitin, G.: On the complexity of derivations in propositional calculus, (1968)
[45] M. Lewis, T. Schubert, B. Becker, Multithreaded SAT solving, in: 12th Asia and South Pacific Design Automation Conference, 2007, pp. 926–931.
[46] B. Haible, R.B. Kreckel, CLN – class library for numbers, http://www.ginac.de/CLN/.
[47] Eén, N.; Sörensson, N.: An extensible SAT-solver, Lncs 2919, 541-638 (2003)
[48] F. Somenzi, CUDD: CU decision diagram package, http://vlsi.colorado.edu/ fabio/CUDD/.
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.