Real-Time Model Checking on Secondary Storage | SpringerLink
Skip to main content
Springer Nature Link
Log in

Real-Time Model Checking on Secondary Storage

  • Conference paper
Model Checking and Artificial Intelligence (MoChArt 2006)

Part of the book series: Lecture Notes in Computer Science ((LNAI,volume 4428))

Included in the following conference series:

Abstract

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.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

Similar content being viewed by others

References

  1. Aggarwal, A., Vitter, J.S.: The input/output complexity of sorting and related problems. Journal of the ACM 31(9), 1116–1127 (1988)

    Article  MathSciNet  Google Scholar 

  2. Alur, R., Dill, D.L.: A theory of timed automata. Theoretical Computer Science 126(2), 183–235 (1994)

    Article  MATH  MathSciNet  Google Scholar 

  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. 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. 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. 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)

    Chapter  Google Scholar 

  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. 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)

    Chapter  Google Scholar 

  9. Edelkamp, S., Jabbar, S., Schroedl, S.: External A*. In: German Conference on Artificial Intelligence (KI), pp. 226–240 (2004)

    Google Scholar 

  10. Ginsberg, M., Harvey, W.: Iterative broadening. Artificial Intelligence, pp. 367–383 (1992)

    Google Scholar 

  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. Hirschberg, D.S.: A linear space algorithm for computing common subsequences. Communications of the ACM 18(6), 341–343 (1975)

    Article  MATH  MathSciNet  Google Scholar 

  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. 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)

    Chapter  Google Scholar 

  15. Korf, R.E.: Divide-and-conquer bidirectional search: First results. In: IJCAI, pp. 1184–1191 (1999)

    Google Scholar 

  16. Korf, R.E., Schultze, P.: Large-scale parallel breadth-first search. In: AAAI, pp. 1380–1385 (2005)

    Google Scholar 

  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. 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. 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)

    Chapter  Google Scholar 

  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. 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. Munagala, K., Ranade, A.: I/O-complexity of graph algorithms. In: SODA, pp. 687–694 (1999)

    Google Scholar 

  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. Sanders, P., Meyer, U., Sibeyn, J.F.: Algorithms for Memory Hierarchies. Springer, Heidelberg (2002)

    Google Scholar 

  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)

    Chapter  Google Scholar 

  26. Zhou, R., Hansen, E.: Breadth-first heuristic search. In: ICAPS, pp. 92–100 (2004)

    Google Scholar 

  27. Zhou, R., Hansen, E.: External-memory pattern databases using structured duplicate detection. In: AAAI (2005)

    Google Scholar 

  28. Zhou, R., Hansen, E.A.: Beam-stack search: Integrating backtracking with beam search. In: ICAPS, pp. 90–98 (2005)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. University of Dortmund, Otto-Hahn Straße 14, Germany

    Stefan Edelkamp & Shahid Jabbar

Authors
  1. Stefan Edelkamp
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Shahid Jabbar
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Stefan Edelkamp Alessio Lomuscio

Rights and permissions

Reprints and permissions

Copyright information

© 2007 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Edelkamp, S., Jabbar, S. (2007). Real-Time Model Checking on Secondary Storage. In: Edelkamp, S., Lomuscio, A. (eds) Model Checking and Artificial Intelligence. MoChArt 2006. Lecture Notes in Computer Science(), vol 4428. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-74128-2_5

Download citation

  • DOI: https://doi.org/10.1007/978-3-540-74128-2_5

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-74127-5

  • Online ISBN: 978-3-540-74128-2

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation