Abstract
This article surveys and gives historical accounts to the algorithmic essentials of directed model checking, a promising bug-hunting technique to mitigate the state explosion problem. In the enumeration process, successor selection is prioritized. We discuss existing guidance and methods to automatically generate them by exploiting system abstractions. We extend the algorithms to feature partial-order reduction and show how liveness problems can be adapted by lifting the search space. For deterministic, finite domains we instantiate the algorithms to directed symbolic, external and distributed search. For real-time domains we discuss the adaption of the algorithms to timed automata and for probabilistic domains we show the application to counterexample generation. Last but not least, we explain how directed model checking helps to accelerate finding solutions to scheduling problems.
Access provided by Autonomous University of Puebla. Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Abdeddaïm, Y., Asarin, E., Maler, O.: Scheduling With Timed Automata. Theoretical Computer Science 354(2), 272–300 (2006)
Ajwani, D., Malinger, I., Meyer, U., Toledo, S.: Characterizing the performance of flash memory storage devices and its impact on algorithm design. In: McGeoch, C.C. (ed.) WEA 2008. LNCS, vol. 5038, pp. 208–219. Springer, Heidelberg (2008)
Aljazzar, H., Hermanns, H., Leue, S.: Counterexamples for timed probabilistic reachability. In: Pettersson, P., Yi, W. (eds.) FORMATS 2005. LNCS, vol. 3829, pp. 177–195. Springer, Heidelberg (2005)
Aljazzar, H., Leue, S.: Extended directed search for probabilistic timed reachability. In: Asarin, E., Bouyer, P. (eds.) FORMATS 2006. LNCS, vol. 4202, pp. 33–51. Springer, Heidelberg (2006)
Aljazzar, H., Leue, S.: Counterexamples for model checking of markov decision processes. Technical Report soft-08-01, Chair for Software Engineering, University of Konstanz, Gemany (December 2007) (submitted for publication)
Aljazzar, H., Leue, S.: Debugging of dependability models using interactive visualization of counterexamples. In: QEST 2008. IEEE Computer Society Press, Los Alamitos (2008)
Alur, R., Brayton, R., Henzinger, T., Qadeer, S., Rajamani, S.: Partial-order reduction in symbolic state-space exploration. Formal Methods in System Design 18, 97–116 (2001)
Alur, R., Dill, D.L.: A theory of timed automata. Theoretical Computer Science 126(2), 183–235 (1994)
Aziz, A., Sanwal, K., Singhal, V., Brayton, R.: Model-checking continuous-time Markov chains. ACM Trans. Comput. Logic 1(1), 162–170 (2000)
Baier, C., Haverkort, B., Hermanns, H., Katoen, J.-P.: Model-checking algorithms for continuous-time Markov chains. IEEE Trans. Software Eng. 29(7) (2003)
Barnat, J., Brim, L., Edelkamp, S., Šimeček, P., Sulewski, D.: Can flash memory help in model checking? In: FMICS, pp. 159–174 (2008)
Barnat, J., Brim, L., Šimeček, P., Weber, M.: Revisiting resistance speeds up I/O-efficient LTL model checking. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 48–62. Springer, Heidelberg (2008)
Behrmann, G., Fehnker, A., Hune, T., Larsen, K.G., Pettersson, P., Romijn, J.M.T.: Efficient guiding towards cost-optimality in UPPAAL. In: Margaria, T., Yi, W. (eds.) TACAS 2001. LNCS, vol. 2031, p. 174. Springer, Heidelberg (2001)
Behrmann, G., Larsen, K., Rasmussen, J.: Optimal scheduling using priced timed automata. SIGMETRICS Performance Evaluation Review 32(4), 34–40 (2005)
Bellman, R.: On a routing problem. Quaterly of Applied Mathematics 16(1), 87–90 (1958)
Bengtsson, J.E., Yi, W.: Timed Automata: Semantics, Algorithms and Tools. In: Desel, J., Reisig, W., Rozenberg, G. (eds.) Lectures on Concurrency and Petri Nets. LNCS, vol. 3098, pp. 87–124. Springer, Heidelberg (2004)
Biere, A.: μcke — efficient μ-calculus model checking. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol. 1254. Springer, Heidelberg (1997)
Biere, A., Artho, C., Schuppan, V.: Liveness checking as safety checking. In: FMICS (2002)
Bisiani, R.: Beam search. In: Shapiro [99], pp. 1467–1568
Bloem, R., Ravi, K., Somenzi, F.: Efficient decision procedures for model checking of linear time logic properties. In: Halbwachs, N., Peled, D.A. (eds.) CAV 1999. LNCS, vol. 1633, pp. 222–235. Springer, Heidelberg (1999)
Bloem, R., Ravi, K., Somenzi, F.: Symbolic guided search for CTL model checking. In: DAC, pp. 29–34 (2000)
Bouajjani, A., Habermehl, P., Vojnar, T.: Abstract regular model checking. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol. 3114, pp. 372–386. Springer, Heidelberg (2004)
Bošnački, D., Leue, S., Lluch-Lafuente, A.: Partial-order reduction for general state exploring algorithms. In: SPIN (2006)
Bozga, M., Kerbaa, A., Maler, O.: Scheduling Acyclic Branching Programs on Parallel Machines. In: RTSS, pp. 208–215. IEEE Computer Society Press, Los Alamitos (2004)
Brinksma, E., Mader, A.: Verification and Optimization of a PLC Control Schedule. In: Havelund, K., Penix, J., Visser, W. (eds.) SPIN 2000. LNCS, vol. 1885. Springer, Heidelberg (2000)
Clarke, E., Grumberg, O., Long, D.: Model checking and abstraction. ACM Trans. Program. Lang. Syst. 16(5), 1512–1542 (1994)
Clarke, E., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge (2000)
Courcoubetis, C., Vardi, M., Wolper, P., Yannakakis, M.: Memory efficient algorithms for the verification of temporal properties. Formal Methods in System Design 1, 275–288 (1992)
Cousot, P., Cousot, R.: Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: POPL (1977)
Dechter, R., Pearl, J.: The optimality of A* revisited. In: AAAI (1983)
Della Croce, F., T’kindt, V.: A recovering beam search algorithm for the one-machine dynamic total completion time scheduling problem. J. of the Operational Research Society 53, 1275–1280 (2002)
Dial, R.: Shortest-path forest with topological ordering. Communications of the ACM 12(11), 632–633 (1969)
Dierks, H.: Time, abstraction and heuristics – automatic verification and planning of timed systems using abstraction and heuristics. Habilitation thesis (July 2005)
Dijkstra, E.: A note on two problems in connection with graphs. Numerische Mathematik 1, 269–271 (1959)
Dillenburg, J., Nelson, P.: Perimeter search. Artificial Intelligence 65(1), 165–178 (1994)
Edelkamp, S.: Symbolic pattern databases in heuristic search planning. In: AIPS (2002)
Edelkamp, S., Jabbar, S.: Large-scale directed model checking LTL. In: Valmari, A. (ed.) SPIN 2006. LNCS, vol. 3925, pp. 1–18. Springer, Heidelberg (2006)
Edelkamp, S., Jabbar, S., Lluch-Lafuente, A.: Cost-algebraic heuristic search. In: AAAI (2005)
Edelkamp, S., Leue, S., Lluch-Lafuente, A.: Directed explicit-state model checking in the validation of communication protocols. STTT 5, 247–267 (2004)
Edelkamp, S., Leue, S., Lluch-Lafuente, A.: Partial order reduction and trail improvement in directed model checking. STTT 6, 277–301 (2004)
Edelkamp, S., Lluch-Lafuente, A.: Abstraction in directed model checking. In: ICAPS-Workshop on Connecting Planning Theory with Practice (2004)
Edelkamp, S., Sanders, P., Šimeček, P.: Semi-external LTL model checking. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol. 5123, pp. 530–542. Springer, Heidelberg (2008)
Edelkamp, S., Sulewski, D.: Flash-efficient LTL model checking with minimal counterexamples. In: SEFM (2008)
Edelkamp, S., Sulewski, D.: Model checking via delayed duplicate detection on the GPU. Technical Report 821, Dortmund University of Technology (2008)
Emerson, A.: Temporal and modal logic. In: van Leeuwen, J. (ed.) Handbook of Theoretical Computer Science, Volume B: Formal Models and Sematics, pp. 995–1072. Elsevier and MIT Press (1990)
Emerson, E., Lei, C.: Efficient model checking in fragments of the propositional mu-calculus (extended abstract). In: LICS, pp. 267–278 (1986)
Evangelista, S.: Dynamic delayed duplicate detection for external memory model checking. In: Havelund, K., Majumdar, R., Palsberg, J. (eds.) SPIN 2008. LNCS, vol. 5156, pp. 77–94. Springer, Heidelberg (2008)
Fehnker, A.: Scheduling a Steel Plant with Timed Automata. In: Proc. RTCSA 1999, IEEE Computer Society Press, Los Alamitos (1999)
Felner, A.: Improving Search Techniques and using them in Different Environments. PhD thesis, Bar-Ilan University (2001)
Fraer, R., Kamhi, G., Ziv, B., Vardi, M., Fix, L.: Prioritized traversal: Efficient reachability analysis for verification and falsification. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855. Springer, Heidelberg (2000)
Ginsberg, M., Harvey, W.: Iterative broadening. Artificial Intelligence 55, 367–383 (1992)
Godefroid, P. (ed.): Partial-Order Methods for the Verification of Concurrent Systems. LNCS, vol. 1032. Springer, Heidelberg (1996)
Grumberg, O., Veith, H. (eds.): 25 Years of Model Checking. LNCS, vol. 5000. Springer, Heidelberg (2008)
Hajek, J.: Self-synchronization and blocking in data transfer protocols. Technical Report THE-RC29286 (1977)
Hajek, J.: Automatically verified data transfer protocols. In: Proceedings 4th International Computer Communications Conference (1978)
Hajek, J. (2002), http://www.humintel.com/hajek/
Han, T., Katoen, J.-P.: Counterexamples in probabilistic model checking. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol. 4424, pp. 72–86. Springer, Heidelberg (2007)
Han, T., Katoen, J.-P.: Providing evidence of likely being on time: Counterexample generation for CTMC model checking. In: Namjoshi, K.S., Yoneda, T., Higashino, T., Okamura, Y. (eds.) ATVA 2007. LNCS, vol. 4762, pp. 331–346. Springer, Heidelberg (2007)
Hansen, E., Zhou, R., Feng, Z.: Symbolic heuristic search using decision diagrams. In: Koenig, S., Holte, R.C. (eds.) SARA 2002. LNCS, vol. 2371, p. 83. Springer, Heidelberg (2002)
Hansson, H., Jonsson, B.: A logic for reasoning about time and reliability. Formal Asp. Comput. 6(5), 512–535 (1994)
Helmert, M., Geffner, H.: Unifying the causal graph and additive heuristic. In: ICAPS, pp. 140–147 (2008)
Helmert, M., Haslum, P., Hoffmann, J.: Flexible abstraction heuristics in optimal sequential planning. In: ICAPS, pp. 176–183 (2007)
Holzmann, G.: The Spin Model Checker: Primer and Reference Manual. Addison-Wesley, Reading (2004)
Holzmann, G., Bosnacki, D.: The design of a multicore extension of the SPIN model checker. IEEE Trans. Software Eng. 33(10), 659–674 (2007)
Holzmann, G., Peled, D., Yannakakis, M.: On nested depth first search. In: SPIN (1996)
Jensen, R., Bryant, R., Veloso, M.: SetA*: An efficient BDD-based heuristic search algorithm. In: AAAI (2002)
Korf, R.: Depth-first iterative-deepening: An optimal admissible tree search. Artificial Intelligence 27(1), 97–109 (1985)
Korf, R., Zhang, W., Thayer, I., Hohwald, H.: Frontier search. Journal of the ACM 52(5), 715–748 (2005)
Kumar, V.: Branch-and-bound search. In: Shapiro [99], pp. 1468–1472
Kupferman, O., Sheinvald-Faragy, S.: Finding shortest witnesses to the nonemptiness of automata on infinite words. In: Baier, C., Hermanns, H. (eds.) CONCUR 2006. LNCS, vol. 4137, pp. 492–508. Springer, Heidelberg (2006)
Kupferschmid, S., Dräger, K., Hoffmann, J., Finkbeiner, B., Dierks, H., Podelski, A., Behrmann, G.: uppaal/DMC – abstraction-based heuristics for directed model checking. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol. 4424, pp. 679–682. Springer, Heidelberg (2007)
Kupferschmid, S., Hoffmann, J., Dierks, H., Behrmann, G.: Adapting an AI planning heuristic for directed model checking. In: Valmari, A. (ed.) SPIN 2006. LNCS, vol. 3925, pp. 35–52. Springer, Heidelberg (2006)
Kupferschmid, S., Wehrle, M., Nebel, B., Podelski, A.: Faster than uppaal? In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol. 5123, pp. 552–555. Springer, Heidelberg (2008)
Kurshan, R.: Computer-Aided Verification of Coordinating Processes: The Automata-Theoretic Approach. Princeton University Press, Princeton (1994)
Lamborn, P., Hansen, E.A.: Layered duplicate detection in external-memory model checking. In: Havelund, K., Majumdar, R., Palsberg, J. (eds.) SPIN 2008. LNCS, vol. 5156, pp. 160–175. Springer, Heidelberg (2008)
Lluch-Lafuente, A.: Directed Search for the Verification of Communication Protocols. PhD thesis, Albert-Ludwigs-Universität Freiburg im Breisgau (2003)
Lowerre, B.T.: The HARPY speech recognition system. PhD thesis, CMU (1976)
McMillan, K.L.: Interpolation and SAT-based model checking. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 1–13. Springer, Heidelberg (2003)
Pearl, J.: Heuristics. Addison-Wesley, Reading (1985)
Peled, D.: Combining partial order reductions with on-the-fly model-checking. Formal Methods in System Design 8, 39–64 (1996)
Qian, K.: Formal Symbolic Verification Using Heuristic Search and Abstraction Techniques. PhD thesis, University of New South Wales (2006)
Qian, K., Nymeyer, A.: Heuristic search algorithms based on symbolic data structures. In: ACAI (2003)
Qian, K., Nymeyer, A.: Guided invariant model checking based on abstraction and symbolic pattern databases. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol. 2988, pp. 497–511. Springer, Heidelberg (2004)
Rasmussen, J.I., Larsen, K.G., Subramani, K.: Resource-optimal scheduling using priced timed automata. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol. 2988, pp. 220–235. Springer, Heidelberg (2004)
Ravi, K., Somenzi, F.: High-density reachability analysis. In: ICCAD (1995)
Ravi, K., Somenzi, F.: Efficient fixpoint computation for invariant checking. In: ICCD (1999)
Ravi, K., Somenzi, F.: Hints to accelerate symbolic traversal. In: Pierre, L., Kropf, T. (eds.) CHARME 1999. LNCS, vol. 1703, pp. 250–266. Springer, Heidelberg (1999)
Reffel, F., Edelkamp, S.: Error detection with directed symbolic model checking. In: Wing, J.M., Woodcock, J.C.P., Davies, J. (eds.) FM 1999. LNCS, vol. 1708, p. 195. Springer, Heidelberg (1999)
Rubin, S.: The ARGOS Image Understanding System. PhD thesis, CMU (1978)
Rungta, N., Mercer, E.G.: Generating counter-examples through randomized guided search. In: Bošnački, D., Edelkamp, S. (eds.) SPIN 2007. LNCS, vol. 4595, pp. 39–57. Springer, Heidelberg (2007)
Russell, S.: Efficient memory-bounded search methods. In: European Conference on Artificial Intelligence (ECAI). Wiley, Chichester (1992)
Ruys, T.C.: Optimal scheduling using branch and bound with SPIN 4.0. In: Ball, T., Rajamani, S.K. (eds.) SPIN 2003. LNCS, vol. 2648, pp. 1–17. Springer, Heidelberg (2003)
Sabuncuoglu, I., Bayiz, M.: Job shop scheduling with beam search. European Journal of Operational Research 118, 390–412 (1999)
Sanders, P., Meyer, U., Sibeyn, J.F.: Algorithms for Memory Hierarchies. Springer, Heidelberg (2002)
Schuppan, V.: Liveness Checking as Safety Checking to Find Shortest Counterexamples to Linear Time Properties. PhD thesis, ETH Zürich (2006)
Schuppan, V., Biere, A.: Efficient reduction of finite state model checking to reachability analysis. STTT 5(2-3), 185–204 (2004)
Schuppan, V., Biere, A.: Liveness checking as safety checking for infinite state spaces. In: INFINITY (2005)
Schuppan, V., Biere, A.: Shortest counterexamples for symbolic model checking of LTL with past. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol. 3440, pp. 493–509. Springer, Heidelberg (2005)
Shapiro, S. (ed.): Encyclopedia of Artificial Intelligence. Wiley Interscience, Hoboken (1992)
Si Ow, P., Smith, S.F.: Viewing scheduling as an opportunistic problem-solving process. Annals of Operations Research 12(1-4), 85–108 (1988)
Sobrinho, J.L.: Algebra and algorithms for QoS path computation and hop-by-hop routing in the internet. IEEE/ACM Transactions on Networking 10, 541–550 (2002)
Stewart, W.: Introduction to the Numerical Solution of Markov Chains. Princeton University Press, New Jersey (1994)
Torabi Dashti, M., Wijs, A.J.: Pruning State Spaces with Extended Beam Search. In: Namjoshi, K.S., Yoneda, T., Higashino, T., Okamura, Y. (eds.) ATVA 2007. LNCS, vol. 4762, pp. 543–552. Springer, Heidelberg (2007)
Valmari, A.: Eliminating redundant interleavings during concurrent program verification. In: Odijk, E., Rem, M., Syre, J.-C. (eds.) PARLE 1989. LNCS, vol. 366, pp. 89–103. Springer, Heidelberg (1989)
Valtorta, M.: A result on the computational complexity of heuristic estimates for the A* algorithm. Information Sciences 34, 48–59 (1984)
Vardi, M., Wolper, P.: An automata-theoretic approach to automatic program verification. In: LICS (1986)
Wah, B., Shang, Y.: Study of IDA*-style searches. Artificial Intelligence 3(4), 493–523 (1995)
Wang, C., Bloem, R., Hachtel, G., Ravi, K., Somenzi, F.: Compositional SCC analysis for language emptiness. Formal Methods in System Design 28(1), 5–36 (2006)
Wehrle, M., Kupferschmidt, S., Podelski, A.: Useful actions are useful. In: ICAPS, pp. 388–395 (2008)
Wijs, A.J.: What to Do Next: Analysing and Optimising System Behaviour in Time. PhD thesis, Vrije Universiteit Amsterdam (2007)
Wijs, A.J., Lisser, B.: Distributed Extended Beam Search for Quantitative Model Checking. In: Edelkamp, S., Lomuscio, A. (eds.) MoChArt IV. LNCS (LNAI), vol. 4428, pp. 165–182. Springer, Heidelberg (2007)
Wijs, A.J., van de Pol, J.C., Bortnik, E.: Solving Scheduling Problems by Untimed Model Checking. In: STTT (to appear, 2008)
Yang, C., Dill, D.: Validation with guided search of the state space. In: DAC (1998)
Zhou, R., Hansen, E.: Breadth-first heuristic search. In: ICAPS (2004)
Zhou, R., Hansen, E.: Beam-stack search: Integrating backtracking with beam search. In: ICAPS (2005)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2009 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Edelkamp, S., Schuppan, V., Bošnački, D., Wijs, A., Fehnker, A., Aljazzar, H. (2009). Survey on Directed Model Checking. In: Peled, D.A., Wooldridge, M.J. (eds) Model Checking and Artificial Intelligence. MoChArt 2008. Lecture Notes in Computer Science(), vol 5348. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-00431-5_5
Download citation
DOI: https://doi.org/10.1007/978-3-642-00431-5_5
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-00430-8
Online ISBN: 978-3-642-00431-5
eBook Packages: Computer ScienceComputer Science (R0)