Skip to main content
SpringerLink
Log in

On the Complexity of Resource-Bounded Logics

  • Conference paper
  • First Online:
Reachability Problems (RP 2016)

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

Included in the following conference series:

Abstract

We revisit decidability results for resource-bounded logics and use decision problems for vector addition systems with states (VASS) to characterise the complexity of (decidable) model-checking problems. We show that the model-checking problem for the logic RB\(\pm \)ATL is 2exptime-complete by using recent results on alternating VASS. In addition, we establish that the model-checking problem for RBTL is decidable and has the same complexity as for RBTL\(^*\) (the extension of RBTL with arbitrary path formulae), namely expspace-complete, proving a new decidability result as a by-product of the approach. Finally, we establish that the model-checking problem for RB\(\pm \)ATL\(^*\) is decidable by a reduction to parity games, and show how to synthesise values for resource parameters.

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

Institutional subscriptions

References

  1. Abdulla, P.A., Mayr, R., Sangnier, A., Sproston, J.: Solving parity games on integer vectors. In: D’Argenio, P.R., Melgratti, H. (eds.) CONCUR 2013 – Concurrency Theory. LNCS, vol. 8052, pp. 106–120. Springer, Heidelberg (2013)

    Chapter  Google Scholar 

  2. Alechina, N., Bulling, N., Logan, B., Nguyen, H.: On the boundary of (un)decidability: decidable model-checking for a fragment of resource agent logic. In: IJCAI 2015, pp. 1494–1501. AAAI Press (2015)

    Google Scholar 

  3. Alechina, N., Logan, B., Nguyen, H., Raimondi, F.: Decidable model-checking for a resource logic with production of resources. In: ECAI 2014, pp. 9–14 (2014)

    Google Scholar 

  4. Alechina, N., Logan, B., Nguyen, H., Raimondi, F.: Technical report: model-checking for resource-bounded ATL with production and consumption of resources. CoRR abs/1504.06766 (2015)

    Google Scholar 

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

    Article  MathSciNet  MATH  Google Scholar 

  6. Bérard, B., Haddad, S., Sassolas, M., Sznajder, N.: Concurrent games on VASS with inhibition. In: Koutny, M., Ulidowski, I. (eds.) CONCUR 2012. LNCS, vol. 7454, pp. 39–52. Springer, Heidelberg (2012)

    Chapter  Google Scholar 

  7. Blockelet, M., Schmitz, S.: Model checking coverability graphs of vector addition systems. In: Murlak, F., Sankowski, P. (eds.) MFCS 2011. LNCS, vol. 6907, pp. 108–119. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

  8. Blondin, M., Finkel, A., Göller, S., Haase, C., McKenzie, P.: Reachability in two-dimensional vector addition systems with states is PSPACE-complete. In: LICS 2015, pp. 32–43. ACM Press (2015)

    Google Scholar 

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

  10. Bulling, N., Farwer, B.: Expressing properties of resource-bounded systems: the logics \({\sf RTL}^\text{* }\) and \({\sf RTL}\). In: Dix, J., Fisher, M., Novák, P. (eds.) CLIMA X. LNCS, vol. 6214, pp. 22–45. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

  11. Bulling, N., Farwer, B.: On the (un-)decidability of model-checking resource-bounded agents. In: ECAI 2010, pp. 567–572 (2010)

    Google Scholar 

  12. Bulling, N., Nguyen, H.: Model checking resource bounded systems with shared resources via alternating Büchi pushdown systems. In: Chen, O., Torroni, P., Villata, S., Hsu, J., Omicini, A. (eds.) PRIMA 2015. LNCS, vol. 9387, pp. 640–649. Springer, Heidelberg (2015)

    Chapter  Google Scholar 

  13. Courtois, J.-B., Schmitz, S.: Alternating vector addition systems with states. In: Csuhaj-Varjú, E., Dietzfelbinger, M., Ésik, Z. (eds.) MFCS 2014, Part I. LNCS, vol. 8634, pp. 220–231. Springer, Heidelberg (2014)

    Google Scholar 

  14. Demri, S.: On selective unboundedness of VASS. JCSS 79(5), 689–713 (2013)

    MathSciNet  MATH  Google Scholar 

  15. Demri, S., Jurdziński, M., Lachish, O., Lazić, R.: The covering and boundedness problems for branching vector addition systems. JCSS 79(1), 23–38 (2013)

    MathSciNet  MATH  Google Scholar 

  16. Emerson, A.: Temporal and modal logic. In: Handbook of Theoretical Computer Science, pp. 996–1072. Elsevier (1990)

    Google Scholar 

  17. Esparza, J.: On the decidability of model checking for several \(\mu \)-calculi and Petri nets. In: Tison, J. (ed.) ICALP 1994. LNCS, vol. 787, pp. 115–129. Springer, Heidelberg (1994)

    Google Scholar 

  18. Esparza, J.: Decidability and complexity of Petri net problems - an introduction. In: Reisig, W., Rozenberg, G. (eds.) Advances in Petri Nets 1998. LNCS, vol. 1491, pp. 374–428. Springer, Heidelberg (1998)

    Google Scholar 

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

  20. Haase, C.: On the complexity of model checking counter automata. Ph.D. thesis, University of Oxford (2012)

    Google Scholar 

  21. Habermehl, P.: On the complexity of the linear-time mu-calculus for Petri nets. In: Azéma, P., Balbo, G. (eds.) Application and Theory of Petri Nets 1997. LNCS, vol. 1248, pp. 102–116. Springer, Heidelberg (1997)

    Chapter  Google Scholar 

  22. Howell, R., Rosier, L.: Problems concerning fairness and temporal logic for conflict-free Petri nets. TCS 64, 305–329 (1989)

    Article  MathSciNet  MATH  Google Scholar 

  23. Jančar, P.: Decidability of a temporal logic problem for Petri nets. TCS 74(1), 71–93 (1990)

    Article  MathSciNet  MATH  Google Scholar 

  24. Jančar, P.: On reachability-related games on vector addition systems with states. In: Bojańczyk, M., Lasota, S., Potapov, I. (eds.) RP 2015. LNCS, vol. 9328, pp. 50–62. Springer, Heidelberg (2015)

    Chapter  Google Scholar 

  25. Juhl, L., Larsen, K., Raskin, J.-F.: Optimal bounds for multiweighted and parametrised energy games. In: Liu, Z., Woodcock, J., Zhu, H. (eds.) Theories of Programming and Formal Methods. LNCS, vol. 8051, pp. 244–255. Springer, Heidelberg (2013)

    Chapter  Google Scholar 

  26. Jurdziński, M., Lazić, R., Schmitz, S.: Fixed-dimensional energy games are in pseudo-polynomial time. In: Halldórsson, M.M., Iwama, K., Kobayashi, N., Speckmann, B. (eds.) ICALP 2015. LNCS, vol. 9135, pp. 260–272. Springer, Heidelberg (2015)

    Google Scholar 

  27. Karp, R., Miller, R.: Parallel program schemata. JCSS 3(2), 147–195 (1969)

    MathSciNet  MATH  Google Scholar 

  28. Lipton, R.: The reachability problem requires exponential space. Technical Report 62, Department of Computer Science, Yale University (1976)

    Google Scholar 

  29. Monica, D.D., Napoli, M., Parente, M.: On a logic for coalitional games with priced-resource agents. ENTCS 278, 215–228 (2011)

    MathSciNet  Google Scholar 

  30. Rackoff, C.: The covering and boundedness problems for vector addition systems. TCS 6(2), 223–231 (1978)

    Article  MathSciNet  MATH  Google Scholar 

  31. Raskin, J.-F., Samuelides, M., Begin, L.V.: Games for counting abstractions. ENTCS 128(6), 69–85 (2005)

    MATH  Google Scholar 

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

  33. Verma, K., Goubault-Larrecq, J.: Karp-miller trees for a branching extension of VASS. Discrete Math. Theor. Comput. Sci. 7, 217–230 (2005)

    MathSciNet  MATH  Google Scholar 

  34. Vester, S.: On the complexity of model-checking branching and alternating-time temporallogics in one-counter systems. In: Finkbeiner, B., Pu, G., Zhang, L. (eds.) ATVA 2015. LNCS, vol. 9364, pp. 361–377. Springer, Heidelberg (2015)

    Chapter  Google Scholar 

Download references

Acknowledgements

We would like to thank the anonymous reviewers for their numerous suggestions that helped us improve the quality of the paper.

Author information

Authors and Affiliations

  1. University of Nottingham, Nottingham, UK

    Natasha Alechina & Brian Logan

  2. TU Delft, Delft, Netherlands

    Nils Bulling

  3. LSV, CNRS, ENS Cachan, Cachan, France

    Stephane Demri

Authors
  1. Natasha Alechina
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Nils Bulling
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Stephane Demri
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Brian Logan
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Nils Bulling .

Editor information

Editors and Affiliations

  1. Aalborg University, Aalborg, Denmark

    Kim Guldstrand Larsen

  2. University of Liverpool, Liverpool, United Kingdom

    Igor Potapov

  3. Aalborg University, Aalborg, Denmark

    Jiří Srba

Rights and permissions

Reprints and permissions

Copyright information

© 2016 Springer International Publishing Switzerland

About this paper

Cite this paper

Alechina, N., Bulling, N., Demri, S., Logan, B. (2016). On the Complexity of Resource-Bounded Logics. In: Larsen, K., Potapov, I., Srba, J. (eds) Reachability Problems. RP 2016. Lecture Notes in Computer Science(), vol 9899. Springer, Cham. https://doi.org/10.1007/978-3-319-45994-3_3

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-45994-3_3

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-45993-6

  • Online ISBN: 978-3-319-45994-3

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation