Skip to main content
SpringerLink
Log in

Improved Algorithm Complexities for Linear Temporal Logic Model Checking of Pushdown Systems

  • Conference paper
Verification, Model Checking, and Abstract Interpretation (VMCAI 2006)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 3855))

Abstract

This paper presents a novel implementation strategy for linear temporal logic (LTL) model checking of pushdown systems (PDS). The model checking problem is formulated intuitively in terms of evaluation of Datalog rules. We use a systematic and fully automated method to generate a specialized algorithm and data structures directly from the rules. The generated implementation employs an incremental approach that considers one fact at a time and uses a combination of linked and indexed data structures for facts. We provide precise time complexity for the model checking problem; it is computed automatically and directly from the rules. We obtain a more precise and simplified complexity analysis, as well as improved algorithm understanding.

This work was supported in part by NSF under grants CCR-0306399 and CCR-0311512 and ONR under grants N00014-04-1-0722 and N00014-02-1-0363.

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

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Abiteboul, S., Hull, R., Vianu, V.: Foundations of Databases. Addison-Wesley, Reading (1995)

    MATH  Google Scholar 

  2. Aho, A.V., Sethi, R., Ullman, J.D.: Compilers: Principles, Techniques and Tools. Addison-Wesley, Reading (1986)

    Google Scholar 

  3. Alur, R., Etessami, K., Yannakakis, M.: Analysis of recursive state machines. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol. 2102, pp. 207–220. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

  4. Ball, T., Rajamani, S.K.: Bebop: A symbolic model checker for boolean programs. In: Havelund, K., Penix, J., Visser, W. (eds.) SPIN 2000. LNCS, vol. 1885, pp. 113–130. Springer, Heidelberg (2000)

    Chapter  Google Scholar 

  5. Basu, S., Kumar, K.N., Pokorny, L.R., Ramakrishnan, C.R.: Resource-constrained model checking of recursive programs. In: Katoen, J.-P., Stevens, P. (eds.) TACAS 2002. LNCS, vol. 2280, pp. 236–250. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  6. Benedikt, M., Godefroid, P., Reps, T.W.: Model checking of unrestricted hierarchical state machines. In: Orejas, F., Spirakis, P.G., van Leeuwen, J. (eds.) ICALP 2001. LNCS, vol. 2076, pp. 652–666. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

  7. Bouajjani, A., Esparza, J., Maler, O.: Reachability analysis of pushdown automata: Application to model-checking. In: International Conference on Concurrency Theory, pp. 135–150 (1997)

    Google Scholar 

  8. Burkart, O., Caucal, D., Moller, F., Steffen, B.: Verification on infinite structures. North-Holland, Amsterdam (2000)

    Google Scholar 

  9. Burkart, O., Steffen, B.: Model checking the full modal mu-calculus for infinite sequential processes. In: Degano, P., Gorrieri, R., Marchetti-Spaccamela, A. (eds.) ICALP 1997. LNCS, vol. 1256, pp. 419–429. Springer, Heidelberg (1997)

    Google Scholar 

  10. Cai, J., Paige, R.: Program derivation by fixed point computation. Science of Computer Programming 11(3), 197–261 (1989)

    Article  MATH  MathSciNet  Google Scholar 

  11. Ceri, S., Gottlob, G., Tanca, L.: Logic programming and databases. Springer, New York (1990)

    Google Scholar 

  12. Clarke, E.M., Emerson, E.A.: Design and synthesis of synchronization skeletons using branching-time temporal logic. In: Logic of Programs, Workshop, London, UK, pp. 52–71. Springer, Heidelberg (1982)

    Chapter  Google Scholar 

  13. Clarke, E.M., Emerson, E.A., Sistla, A.P.: Automatic verification of finite state concurrent system using temporal logic specifications: a practical approach. In: POPL 1983: Proceedings of the 10th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, pp. 117–126. ACM Press, New York (1983)

    Chapter  Google Scholar 

  14. Edmund, J., Clark, M., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, Cambridge (1999)

    Google Scholar 

  15. Esparza, J., Hansel, D., Rossmanith, P., Schwoon, S.: Efficient algorithms for model checking pushdown systems. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 232–247. Springer, Heidelberg (2000)

    Chapter  Google Scholar 

  16. Esparza, J., Schwoon, S.: A bdd-based model checker for recursive programs. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol. 2102, pp. 324–336. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

  17. Finkel, A., Willems, B., Wolper, P.: A direct symbolic approach to model checking pushdown systems. In: Proc. 2nd Int. Workshop on Verification of Infinite State Systems (INFINITY 1997). Electronic Notes in Theoretic Comp. Sci, vol. 9. Elsevier, Amsterdam (1997)

    Google Scholar 

  18. Liu, Y.A., Stoller, S.D.: From datalog rules to efficient programs with time and space guarantees. In: Proceedings of the 5th ACM SIGPLAN international conference on Principles and practice of declaritive programming, pp. 172–183. ACM Press, New York (2003)

    Chapter  Google Scholar 

  19. Paige, R.: Real-time simulation of a set machine on a ram (1989)

    Google Scholar 

  20. Paige, R., Koenig, S.: Finite differencing of computable expressions. ACM Trans. Program. Lang. Syst. 4(3), 402–454 (1982)

    Article  MATH  Google Scholar 

  21. Queille, J.-P., Sifakis, J.: Specification and verification of concurrent systems in cesar. In: Proceedings of the 5th Colloquium on International Symposium on Programming, London, UK, pp. 337–351. Springer, London (1982)

    Google Scholar 

  22. Reps, T., Horwitz, S., Sagiv, M.: Precise interprocedural dataflow analysis via graph reachability. In: Conference Record of POPL 1995: 22nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, San Francisco, California, pp. 49–61 (1995)

    Google Scholar 

  23. Sagonas, K., Swift, T., Warren, D.S.: XSB as an efficient deductive database engine. In: Snodgrass, R.T., Winslett, M. (eds.) Proceedings of the 1994 ACM SIGMOD International Conference on Management of Data SIGMOD 1994, pp. 442–453 (1994)

    Google Scholar 

  24. Steffen, B.: Generating data flow analysis algorithms from modal specifications. In: Ito, T., Meyer, A.R. (eds.) TACS 1991. LNCS, vol. 526, pp. 115–139. Springer, Heidelberg (1991)

    Google Scholar 

  25. Steffen, B., Classen, A., Klein, M., Knoop, J., Margaria, T.: The fixpoint-analysis machine. In: Lee, I., Smolka, S.A. (eds.) CONCUR 1995. LNCS, vol. 962, pp. 72–87. Springer, Heidelberg (1995)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Computer Science Department, State University of New York, Stony Brook, NY, 11794, USA

    Katia Hristova & Yanhong A. Liu

Authors
  1. Katia Hristova
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Yanhong A. Liu
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Aiken Computation Laboratory, Harvard University,, 02138, Cambridge, Mass, USA

    E. Allen Emerson

  2. Bell Laboratories, Alcatel-Lucent,  

    Kedar S. Namjoshi

Rights and permissions

Reprints and permissions

Copyright information

© 2005 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Hristova, K., Liu, Y.A. (2005). Improved Algorithm Complexities for Linear Temporal Logic Model Checking of Pushdown Systems. In: Emerson, E.A., Namjoshi, K.S. (eds) Verification, Model Checking, and Abstract Interpretation. VMCAI 2006. Lecture Notes in Computer Science, vol 3855. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11609773_13

Download citation

  • DOI: https://doi.org/10.1007/11609773_13

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-31139-3

  • Online ISBN: 978-3-540-31622-0

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation