Real-Time Model Checking on Secondary Storage

  • Stefan Edelkamp
  • Shahid Jabbar
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 4428)


In this paper, we consider disk based exploration in priced timed automata for resource-optimal scheduling. State spaces for large problems can easily go beyond the main memory capacity. We propose the use of hard disk to store the generated state space induced by priced timed automata. We contribute three algorithms: External Breadth First Search for reachability analysis in ordinary timed automata, External Breadth First Branch-and-Bound for cost-optimal reachability analysis in priced timed automata, and Iterative Broadening External Breadth First Branch-and-Bound for a partial exploration in priced timed automata. The third algorithm achieves its completeness by trying to find an upper bound on the optimal solution in an incomplete search tree. Iteratively, the upper bound is made tighter and the coverage of the search space is widened. We present correctness and completeness proofs for the suggested algorithms along with experimental results on different instances of aircraft landing scheduling to validate the practicality of our approach.


Model Check Hybrid Automaton Reachability Analysis Reachability Problem Time Automaton 
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.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Aggarwal, A., Vitter, J.S.: The input/output complexity of sorting and related problems. Journal of the ACM 31(9), 1116–1127 (1988)CrossRefMathSciNetGoogle Scholar
  2. 2.
    Alur, R., Dill, D.L.: A theory of timed automata. Theoretical Computer Science 126(2), 183–235 (1994)zbMATHCrossRefMathSciNetGoogle Scholar
  3. 3.
    Arge, L., Knudsen, M., Larsen, K.: Sorting multisets and vectors in-place. In: Dehne, F., Sack, J.-R., Santoro, N. (eds.) WADS 1993. LNCS, vol. 709, pp. 83–94. Springer, Heidelberg (1993)Google Scholar
  4. 4.
    Behrman, G., Fehnker, A., Vaandrager, F.: Distributed timed model checking - how the search order matters. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, Springer, Heidelberg (2000)Google Scholar
  5. 5.
    Behrmann, G., Larsen, K.G., Rasmussen, J.I.: Optimal scheduling using priced timed automata. In: ICAPS Workshop on Verification and Validation of Model-Based Planning and Scheduling Systems (2005)Google Scholar
  6. 6.
    Cassez, F., David, A., Fleury, E., Larsen, K.G., Lime, D.: Efficient on-the-fly algorithms for the analysis of timed games. In: Abadi, M., de Alfaro, L. (eds.) CONCUR 2005. LNCS, vol. 3653, Springer, Heidelberg (2005)CrossRefGoogle Scholar
  7. 7.
    Dierks, H.: Finding optimal plans for domains with restricted continuous effects with cora. In: ICAPS Workshop on Verification and Validation of Model-Based Planning and Scheduling Systems (2005)Google Scholar
  8. 8.
    Edelkamp, S., Jabbar, S.: Large-scale directed model checking LTL. In: Valmari, A. (ed.) Model Checking Software. LNCS, vol. 3925, pp. 1–18. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  9. 9.
    Edelkamp, S., Jabbar, S., Schroedl, S.: External A*. In: German Conference on Artificial Intelligence (KI), pp. 226–240 (2004)Google Scholar
  10. 10.
    Ginsberg, M., Harvey, W.: Iterative broadening. Artificial Intelligence, pp. 367–383 (1992)Google Scholar
  11. 11.
    Henzinger, T.A., Kopke, P.W., Puri, A., Varaiya, P.: What’s decidable about hybrid automata? In: ACM STOC, pp. 373–381 (1995)Google Scholar
  12. 12.
    Hirschberg, D.S.: A linear space algorithm for computing common subsequences. Communications of the ACM 18(6), 341–343 (1975)zbMATHCrossRefMathSciNetGoogle Scholar
  13. 13.
    Jabbar, S., Edelkamp, S.: I/O efficient directed model checking. In: Cousot, R. (ed.) VMCAI 2005. LNCS, vol. 3385, pp. 313–329. Springer, Heidelberg (2005)Google Scholar
  14. 14.
    Jabbar, S., Edelkamp, S.: Parallel external directed model checking with linear I/O. In: Emerson, E.A., Namjoshi, K.S. (eds.) VMCAI 2006. LNCS, vol. 3855, pp. 237–251. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  15. 15.
    Korf, R.E.: Divide-and-conquer bidirectional search: First results. In: IJCAI, pp. 1184–1191 (1999)Google Scholar
  16. 16.
    Korf, R.E., Schultze, P.: Large-scale parallel breadth-first search. In: AAAI, pp. 1380–1385 (2005)Google Scholar
  17. 17.
    Korf, R.E., Zhang, W.: Divide-and-conquer frontier search applied to optimal sequence allignment. In: AAAI, pp. 910–916 (2000)Google Scholar
  18. 18.
    Kristensen, L., Mailund, T.: Path finding with the sweep-line method using external storage. In: Dong, J.S., Woodcock, J. (eds.) ICFEM 2003. LNCS, vol. 2885, pp. 319–337. Springer, Heidelberg (2003)Google Scholar
  19. 19.
    Kupferschmid, S., Hoffmann, J., Dierks, H., Behrmann, G.: Adapting an AI planning heuristic for directed model checking. In: Valmari, A. (ed.) Model Checking Software. LNCS, vol. 3925, pp. 35–52. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  20. 20.
    Larsen, K.G., Behrmann, G., Brinksma, E., Fehnker, A., Hune, T.S., Petterson, P., Romijn, J.: As cheap as possible: Efficient cost-optimal reachability for priced timed automata. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol. 2102, pp. 493–505. Springer, Heidelberg (2001)Google Scholar
  21. 21.
    Larsen, K.G., Larsson, F., Petterson, P., Yi, W.: Efficient verification of real-time systems: Compact data structures and state-space reduction. In: IEEE Real Time Systems Symposium, pp. 14–24 (1997)Google Scholar
  22. 22.
    Munagala, K., Ranade, A.: I/O-complexity of graph algorithms. In: SODA, pp. 687–694 (1999)Google Scholar
  23. 23.
    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)Google Scholar
  24. 24.
    Sanders, P., Meyer, U., Sibeyn, J.F.: Algorithms for Memory Hierarchies. Springer, Heidelberg (2002)Google Scholar
  25. 25.
    Stern, U., Dill, D.: Using magnetic disk instead of main memory in the murphi verifier. In: Vardi, M.Y. (ed.) CAV 1998. LNCS, vol. 1427, pp. 172–183. Springer, Heidelberg (1998)CrossRefGoogle Scholar
  26. 26.
    Zhou, R., Hansen, E.: Breadth-first heuristic search. In: ICAPS, pp. 92–100 (2004)Google Scholar
  27. 27.
    Zhou, R., Hansen, E.: External-memory pattern databases using structured duplicate detection. In: AAAI (2005)Google Scholar
  28. 28.
    Zhou, R., Hansen, E.A.: Beam-stack search: Integrating backtracking with beam search. In: ICAPS, pp. 90–98 (2005)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2007

Authors and Affiliations

  • Stefan Edelkamp
    • 1
  • Shahid Jabbar
    • 1
  1. 1.University of Dortmund, Otto-Hahn Straße 14Germany

Personalised recommendations