Advertisement

On the Complexity of Resource-Bounded Logics

  • Natasha Alechina
  • Nils BullingEmail author
  • Stephane Demri
  • Brian Logan
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 9899)

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.

Keywords

Temporal Logic Atomic Formula Pareto Frontier State Reachability Unary Rule 
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.

Notes

Acknowledgements

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

References

  1. 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)CrossRefGoogle Scholar
  2. 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. 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. 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. 5.
    Alur, R., Henzinger, T., Kupferman, O.: Alternating-time temporal logic. JACM 49(5), 672–713 (2002)MathSciNetCrossRefzbMATHGoogle Scholar
  6. 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)CrossRefGoogle Scholar
  7. 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)CrossRefGoogle Scholar
  8. 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. 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)CrossRefGoogle Scholar
  10. 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)CrossRefGoogle Scholar
  11. 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. 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)CrossRefGoogle Scholar
  13. 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. 14.
    Demri, S.: On selective unboundedness of VASS. JCSS 79(5), 689–713 (2013)MathSciNetzbMATHGoogle Scholar
  15. 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)MathSciNetzbMATHGoogle Scholar
  16. 16.
    Emerson, A.: Temporal and modal logic. In: Handbook of Theoretical Computer Science, pp. 996–1072. Elsevier (1990)Google Scholar
  17. 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. 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. 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)MathSciNetCrossRefzbMATHGoogle Scholar
  20. 20.
    Haase, C.: On the complexity of model checking counter automata. Ph.D. thesis, University of Oxford (2012)Google Scholar
  21. 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)CrossRefGoogle Scholar
  22. 22.
    Howell, R., Rosier, L.: Problems concerning fairness and temporal logic for conflict-free Petri nets. TCS 64, 305–329 (1989)MathSciNetCrossRefzbMATHGoogle Scholar
  23. 23.
    Jančar, P.: Decidability of a temporal logic problem for Petri nets. TCS 74(1), 71–93 (1990)MathSciNetCrossRefzbMATHGoogle Scholar
  24. 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)CrossRefGoogle Scholar
  25. 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)CrossRefGoogle Scholar
  26. 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. 27.
    Karp, R., Miller, R.: Parallel program schemata. JCSS 3(2), 147–195 (1969)MathSciNetzbMATHGoogle Scholar
  28. 28.
    Lipton, R.: The reachability problem requires exponential space. Technical Report 62, Department of Computer Science, Yale University (1976)Google Scholar
  29. 29.
    Monica, D.D., Napoli, M., Parente, M.: On a logic for coalitional games with priced-resource agents. ENTCS 278, 215–228 (2011)MathSciNetGoogle Scholar
  30. 30.
    Rackoff, C.: The covering and boundedness problems for vector addition systems. TCS 6(2), 223–231 (1978)MathSciNetCrossRefzbMATHGoogle Scholar
  31. 31.
    Raskin, J.-F., Samuelides, M., Begin, L.V.: Games for counting abstractions. ENTCS 128(6), 69–85 (2005)zbMATHGoogle Scholar
  32. 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)CrossRefGoogle Scholar
  33. 33.
    Verma, K., Goubault-Larrecq, J.: Karp-miller trees for a branching extension of VASS. Discrete Math. Theor. Comput. Sci. 7, 217–230 (2005)MathSciNetzbMATHGoogle Scholar
  34. 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)CrossRefGoogle Scholar

Copyright information

© Springer International Publishing Switzerland 2016

Authors and Affiliations

  • Natasha Alechina
    • 1
  • Nils Bulling
    • 2
    Email author
  • Stephane Demri
    • 3
  • Brian Logan
    • 1
  1. 1.University of NottinghamNottinghamUK
  2. 2.TU DelftDelftNetherlands
  3. 3.LSV, CNRS, ENS CachanCachanFrance

Personalised recommendations