Skip to main content
SpringerLink
Log in
Book cover

International Symposium on Automated Technology for Verification and Analysis

ATVA 2015: Automated Technology for Verification and Analysis pp 361–377Cite as

On the Complexity of Model-Checking Branching and Alternating-Time Temporal Logics in One-Counter Systems

  • Conference paper
  • First Online:

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 9364))

Abstract

We study the complexity of the model-checking problem for the branching-time logic \(\text {CTL}^*\) and the alternating-time temporal logics \(\text {ATL}/\text {ATL}^*\) in one-counter processes and one-counter games respectively. The complexity is determined for all three logics when integer weights are input in unary (non-succinct) and binary (succinct) as well as when the input formula is fixed and is a parameter. Further, we show that deciding the winner in one-counter games with \(\text {LTL}\) objectives is \(\textsc {2ExpSpace}\)-complete for both succinct and non-succinct games. We show that all the problems considered stay in the same complexity classes when we add quantitative constraints that can compare the current value of the counter with a constant.

This is a preview of subscription content, 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 EPUB and 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

Learn about institutional subscriptions

References

  1. Alur, R., Henzinger, T.A., Kupferman, O.: Alternating-time temporal logic. J. ACM 49(5), 672–713 (2002)

    Article  MathSciNet  MATH  Google Scholar 

  2. Bouyer, P., Fahrenberg, U., Larsen, K.G., Markey, N., Srba, J.: Infinite runs in weighted timed automata with energy constraints. In: Cassez, F., Jard, C. (eds.) FORMATS 2008. LNCS, vol. 5215, pp. 33–47. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  3. Bouyer, P., Gardy, P., Markey, N.: Quantitative verification of weighted kripke structures. In: Cassez, F., Raskin, J.-F. (eds.) ATVA 2014. LNCS, vol. 8837, pp. 64–80. Springer, Heidelberg (2014)

    Google Scholar 

  4. Bozzelli, L.: Complexity results on branching-time pushdown model checking. Theoret. Comput. Sci. 379(1–2), 286–297 (2007)

    Article  MathSciNet  MATH  Google Scholar 

  5. Bozzelli, L., Murano, A., Peron, A.: Pushdown module checking. Form. Methods Syst. Des. 36(1), 65–95 (2010)

    Article  MATH  Google Scholar 

  6. Brázdil, T., Jančar, P., Kučera, A.: Reachability games on extended vector addition systems with states. In: Abramsky, S., Gavoille, C., Kirchner, C., Meyer auf der Heide, F., Spirakis, P.G. (eds.) ICALP 2010. LNCS, vol. 6199, pp. 478–489. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

  7. Bulling, N., Goranko, V.: How to be both rich and happy: combining quantitative and qualitative strategic reasoning about multi-player games (extended abstract). In: SR, pp. 33–41 (2013)

    Google Scholar 

  8. Clarke, E.M., Emerson, E.A.: Design and synthesis of synchronization skeletons using branching time temporal logic. In: Kozen, D. (ed.) Logic of Programs 1981. LNCS, vol. 131, pp. 52–71. Springer, Heidelberg (1982)

    Chapter  Google Scholar 

  9. Demri, S., Gascon, R.: The effects of bounding syntactic resources on presburger LTL. J. Log. Comput. 19(6), 1541–1575 (2009)

    Article  MathSciNet  MATH  Google Scholar 

  10. Emerson, E.A.: The beginning of model checking: a personal perspective. In: Grumberg, O., Veith, H. (eds.) 25 Years of Model Checking. LNCS, vol. 5000, pp. 27–45. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  11. Emerson, E.A., Halpern, J.Y.: "sometimes" and "not never" revisited: on branching versus linear time temporal logic. J. ACM 33(1), 151–178 (1986)

    Article  MathSciNet  MATH  Google Scholar 

  12. Göller, S., Haase, C., Ouaknine, J., Worrell, J.: Model checking succinct and parametric one-counter automata. In: Abramsky, S., Gavoille, C., Kirchner, C., Meyer auf der Heide, F., Spirakis, P.G. (eds.) ICALP 2010. LNCS, vol. 6199, pp. 575–586. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

  13. Göller, S., Lohrey, M.: Branching-time model checking of one-counter processes and timed automata. SIAM J. Comput. 42(3), 884–923 (2013)

    Article  MathSciNet  MATH  Google Scholar 

  14. Holzer, M.: On emptiness and counting for alternating finite automata. In: Developments in Language Theory, pp. 88–97 (1995)

    Google Scholar 

  15. Jancar, P., Sawa, Z.: A note on emptiness for alternating finite automata with a one-letter alphabet. Inf. Process. Lett. 104(5), 164–167 (2007)

    Article  MathSciNet  MATH  Google Scholar 

  16. Kupferman, O., Madhusudan, P., Thiagarajan, P.S., Vardi, M.Y.: Open systems in reactive environments: control and synthesis. In: Palamidessi, C. (ed.) CONCUR 2000. LNCS, vol. 1877, pp. 92–107. Springer, Heidelberg (2000)

    Chapter  Google Scholar 

  17. Löding, C., Madhusudan, P., Serre, O.: Visibly pushdown games. In: Lodaya, K., Mahajan, M. (eds.) FSTTCS 2004. LNCS, vol. 3328, pp. 408–420. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  18. Piterman, N.: From nondeterministic büchi and streett automata to deterministic parity automata. In: Logical Methods in Computer Science, 3(3) (2007)

    Google Scholar 

  19. Pnueli, A.: The temporal logic of programs. In: FOCS, pp. 46–57 (1977)

    Google Scholar 

  20. Pnueli, A., Rosner, R.: On the synthesis of a reactive module. In: POPL, pp. 179–190 (1989)

    Google Scholar 

  21. Pnueli, A., Rosner, R.: On the synthesis of an asynchronous reactive module. In: Ausiello, G., Dezani-Ciancaglini, M., Rocca, S.R.D. (eds.) ICALP 1989. LNCS, vol. 372, pp. 652–671. Springer, Heidelberg (1989)

    Chapter  Google Scholar 

  22. Serre, O.: Parity games played on transition graphs of one-counter processes. In: Aceto, L., Ingólfsdóttir, A. (eds.) FOSSACS 2006. LNCS, vol. 3921, pp. 337–351. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  23. Sistla, A.P., Clarke, E.M.: The complexity of propositional linear temporal logics. J. ACM 32(3), 733–749 (1985)

    Article  MathSciNet  MATH  Google Scholar 

  24. Vardi, M.Y.: Reasoning about the past with two-way automata. In: Larsen, K.G., Skyum, S., Winskel, G. (eds.) ICALP 1998. LNCS, vol. 1443, pp. 628–641. Springer, Heidelberg (1998)

    Chapter  Google Scholar 

  25. Wolper, P., Vardi, M.Y., Sistla, P.V.: Reasoning about infinite computation paths (extended abstract). In: FOCS, pp. 185–194 (1983)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Technical University of Denmark, Kongens Lyngby, Denmark

    Steen Vester

Authors
  1. Steen Vester
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Steen Vester .

Editor information

Editors and Affiliations

  1. Universität des Saarlandes, Saarbrücken, Germany

    Bernd Finkbeiner

  2. East China Normal University, Shanghai, China

    Geguang Pu

  3. Chinese Academy of Sciences, Beijing, China

    Lijun Zhang

Rights and permissions

Reprints and permissions

Copyright information

© 2015 Springer International Publishing Switzerland

About this paper

Cite this paper

Vester, S. (2015). On the Complexity of Model-Checking Branching and Alternating-Time Temporal Logics in One-Counter Systems. In: Finkbeiner, B., Pu, G., Zhang, L. (eds) Automated Technology for Verification and Analysis. ATVA 2015. Lecture Notes in Computer Science(), vol 9364. Springer, Cham. https://doi.org/10.1007/978-3-319-24953-7_27

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-24953-7_27

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-24952-0

  • Online ISBN: 978-3-319-24953-7

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation