Skip to main content
SpringerLink
Log in

Model Checking Logics of Strategic Ability: Complexity*

  • Chapter
  • First Online:
Specification and Verification of Multi-agent Systems

Abstract

This chapter is about model checking and its complexity in some of the main temporal and strategic logics, e.g. LTL, CTL, and ATL. We discuss several variants of ATL (perfect vs. imperfect recall, perfect vs. imperfect information) as well as two different measures for model checking with concurrent game structures (explicit vs. implicit representation of transitions). Finally, we summarize some results about higher order representations of the underlying models.

* This work was partly funded by the NTH School for IT Ecosystems. NTH (Niedersächsische Technische Hochschule) is a joint university consisting of Technische Universität Braunschweig, Technische Universität Clausthal, and Leibniz Universität Hannover.

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 129.00
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 169.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info
Hardcover Book
USD 169.99
Price excludes VAT (USA)
  • Durable hardcover 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. Dembiński, P., Janowska, A., Janowski, P., Penczek, W., Półrola, A., Szreter, M., Woźna, B., Zbrzezny, A.: Verics: A tool for verifying timed automata and estelle specifications. In: Proceedings of the of the 9th Int. Conf. on Tools and Algorithms for Construction and Analysis of Systems (TACAS’03), LNCS, vol. 2619, pp. 278–283. Springer (2003)

    Google Scholar 

  2. Bulling, N., Jamroga, W.: Verifying agents with memory is harder than it seemed. In: Proceedings of AAMAS 2010 . ACM Press, Toronto, Canada (2010)

    Google Scholar 

  3. Goranko, V., Jamroga, W.: Comparing semantics of logics for multi-agent systems. Synthese 139(2), 241–280 (2004)

    Article  MATH  MathSciNet  Google Scholar 

  4. Laroussinie, F., Markey, N., Schnoebelen, P.: Model checking CTL+ and FCTL is hard. In: Proceedings of FoSSaCS’01, Lecture Notes in Computer Science, vol. 2030, pp. 318–331. Springer (2001)

    Google Scholar 

  5. Goranko, V., van Drimmelen, G.: Complete axiomatization and decidability of the A lternating-time T emporal L ogic (2003)

    Google Scholar 

  6. Jamroga, W.: A temporal logic for stochastic multi-agent systems. In: Proceedings of PRIMA’08, LNCS, vol. 5357, pp. 239–250 (2008)

    Google Scholar 

  7. Alur, R., Henzinger, T.A., Kupferman, O.: Alternating-time temporal logic. In: Proceedings of the 38th Annual Symposium on Foundations of Computer Science (FOCS), pp. 100–109. IEEE Computer Society Press (1997)

    Google Scholar 

  8. Hintikka, J.: Logic, Language Games and Information. Clarendon Press : Oxford (1973)

    MATH  Google Scholar 

  9. Pnueli, A., Rosner, R.: On the synthesis of a reactive module. In: POPL ’89: Proceedings of the 16th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, pp. 179–190. ACM, New York, NY, USA (1989)

    Google Scholar 

  10. Alur, R., Henzinger, T.A., Kupferman, O.: Alternating-time temporal logic. Journal of the ACM 49, 672–713 (2002)

    Article  MathSciNet  Google Scholar 

  11. Pauly, M.: A modal logic for coalitional power in games. Journal of Logic and Computation 12(1), 149–166 (2002)

    Article  MATH  MathSciNet  Google Scholar 

  12. Jamroga, W., Dix, J.: Model checking abilities of agents: A closer look. Theory of Computing Systems 42(3), 366–410 (2008)

    Article  MATH  MathSciNet  Google Scholar 

  13. Laroussinie, F., Markey, N., Oreiby, G.: On the expressiveness and complexity of atl. LNCS 4, 7 (2008)

    MathSciNet  Google Scholar 

  14. Schobbens, P.Y.: Alternating-time logic with imperfect recall. Electronic Notes in Theoretical Computer Science 85(2) (2004)

    Google Scholar 

  15. Beeri, C.: On the menbership problem for functional and multivalued dependencies in relational databases. ACM Trans. Database Syst. 5(3), 241–259 (1980)

    Article  MATH  Google Scholar 

  16. Kazmierczak, E., Dart, P., Sterling, L., Winikoff, M.: Verifying requirements through mathematical modelling and animation. International Journal of Software Engineering and Knowledge Engineering 10(2), 251–273 (2000)

    Article  Google Scholar 

  17. van Otterloo, S., van der Hoek, W., Wooldridge, M.: Knowledge as strategic ability. Electronic Lecture Notes in Theoretical Computer Science 85(2) (2003)

    Google Scholar 

  18. Jamroga, W., Ågotnes, T.: Modular interpreted systems. In: Proceedings of AAMAS’07, pp. 892–899 (2007)

    Google Scholar 

  19. van der Hoek, W., Lomuscio, A., Wooldridge, M.: On the complexity of practical ATL model checking. In: P. Stone, G. Weiss (eds.) Proceedings of AAMAS’06 , pp. 201–208 (2006)

    Google Scholar 

  20. Jamroga, W., Dix, J.: Do agents make model checking explode (computationally)? In: M. Pĕchouček, P. Petta, L. Varga (eds.) Proceedings of CEEMAS 2005 , Lecture Notes in Computer Science, vol. 3690, pp. 398–407. Springer Verlag (2005)

    Google Scholar 

  21. Jamroga, W., Ågotnes, T.: Modular interpreted systems: A preliminary report. Tech. Rep. IfI-06-15, Clausthal University of Technology (2006)

    Google Scholar 

  22. Raimondi, F.: Model checking multi-agent systems. Ph.D. thesis, University College London (2006)

    Google Scholar 

  23. van der Hoek, W., Wooldridge, M.: Cooperation, knowledge and time: Alternating-time Temporal Epistemic Logic and its applications. Studia Logica 75(1), 125–157 (2003)

    Article  MATH  MathSciNet  Google Scholar 

  24. Clarke, E., Emerson, E.: Design and synthesis of synchronization skeletons using branching time temporal logic. In: Proceedings of Logics of Programs Workshop, LNCS, vol. 131, pp. 52–71 (1981)

    Google Scholar 

  25. Raimondi, F., Lomuscio, A.: Automatic verification of deontic interpreted systems by model checking via OBDD ’s. In: R. de Mántaras, L. Saitta (eds.) Proceedings of ECAI, pp. 53–57 (2004)

    Google Scholar 

  26. Rosner, R.: Modular synthesis of reactive systems. Ph.D. thesis, Weizmann Institute of Science (1992)

    Google Scholar 

  27. van Drimmelen, G.: Satisfiability in alternating-time temporal logic. In: Proceedings of LICS’2003, pp. 208–217. IEEE Computer Society Press (2003)

    Google Scholar 

  28. Vardi, M.Y., Wolper, P.: An automata-theoretic approach to automatic program verification (preliminary report). In: Proceedings of the First Annual IEEE Symposium on Logic in Computer Science (LICS 1986), pp. 332–344. IEEE Computer Society Press (1986)

    Google Scholar 

  29. Alur, R., Henzinger, T.A.: Reactive modules. Formal Methods in System Design 15(1), 7–48 (1999)

    Article  MathSciNet  Google Scholar 

  30. Wilke, T.: CTL+ is exponentially more succint than CTL . In: Proceedings of FST&TCS ’99, LNCS, vol. 1738, pp. 110–121 (1999)

    Google Scholar 

  31. Schnoebelen, P.: The complexity of temporal model checking. In: Advances in Modal Logics, Proceedings of AiML 2002. World Scientific (2003)

    Google Scholar 

  32. Walther, D., Lutz, C., Wolter, F., Wooldridge, M.: ATL satisfiability is indeed EXPTIME -complete. Journal of Logic and Computation 16(6), 765–787 (2006)

    Article  MATH  MathSciNet  Google Scholar 

  33. Lichtenstein, O., Pnueli, A.: Checking that finite state concurrent programs satisfy their linear specification. In: POPL ’85: Proceedings of the 12th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, pp. 97–107. ACM, New York, NY, USA (1985)

    Google Scholar 

  34. Jamroga, W., Ågotnes, T.: Constructive knowledge: What agents can achieve under incomplete information. Journal of Applied Non-Classical Logics 17(4), 423–475 (2007)

    Article  MATH  MathSciNet  Google Scholar 

  35. Emerson, E.A., Lei, C.L.: Modalities for model checking: Branching time logic strikes back. Science of Computer Programming 8(3), 275–306 (1987)

    Article  MATH  MathSciNet  Google Scholar 

  36. Harding, A., Ryan, M., Schobbens, P.Y.: Approximating ATL* in ATL . In: VMCAI ’02: Revised Papers from the Third International Workshop on Verification, Model Checking, and Abstract Interpretation, pp. 289–301. Springer-Verlag, London, UK (2002)

    Google Scholar 

  37. Alur, R., Henzinger, T., Mang, F., Qadeer, S., Rajamani, S., Tasiran, S.: OCHA user manual. In: Proceedings of CAV’98, Lecture Notes in Computer Science, vol. 1427, pp. 521–525 (1998)

    Google Scholar 

  38. Laroussinie, F., Markey, N., Oreiby, G.: Expressiveness and complexity of ATL . Tech. Rep. LSV-06-03, CNRS & ENS Cachan, France (2006)

    Google Scholar 

  39. Broersen, J., Herzig, A., Troquard, N.: A STIT -extension of ATL . In: JELIA, pp. 69–81 (2006)

    Google Scholar 

  40. Jamroga, W., Dix, J.: Model checking ATL ir is indeed \(\Delta _2^P \)-complete. In: Proceedings of EUMAS’06 (2006)

    Google Scholar 

  41. Emerson, E.A., Sistla, A.P.: Deciding branching time logic. In: STOC ’84: Proceedings of EL87 sixteenth annual ACM symposium on Theory of computing, pp. 14–24. ACM, New York, NY, USA (1984)

    Book  Google Scholar 

  42. Fagin, R., Halpern, J.Y., Moses, Y., Vardi, M.Y.: Reasoning about Knowledge. MIT Press: Cambridge, MA (1995)

    MATH  Google Scholar 

  43. Schewe, S.: ATL* satisfiability is 2 E xp T ime-complete. In: Proceedings of ICALP 2008, Lecture Notes in Computer Science, vol. 5126, pp. 373–385. Springer-Verlag (2008)

    Google Scholar 

  44. Clarke, E.M., Emerson, E.A., Sistla, A.P.: A utomatic V erification of F inite- S tate C oncurrent S ystems U sing T emporal L ogic S pecifications. ACM Transactions on Programming Languages and Systems 8(2), 244–263 (1986)

    Article  MATH  Google Scholar 

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

    Article  MATH  MathSciNet  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Dept. of Informatics, Niedersächsische Technische Hochschule, Clausthal-Zellerfeld, Germany

    N. Bulling, J. Dix & W. Jamroga

  2. Computer Science and Communications, University of Luxembourg, Luxembourg, UK

    W. Jamroga

Authors
  1. N. Bulling
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. J. Dix
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. W. Jamroga
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to N. Bulling .

Editor information

Editors and Affiliations

  1. Dept. Information & Computing Sciences, Utrecht University, Padualaan 14, Utrecht, 3584 CH, Netherlands

    Mehdi Dastani

  2. Delft University of Technology, Mekelweg 4, Delft, 2628 CD, Netherlands

    Koen V. Hindriks

  3. Dept. Information & Computer Sciences, Utrecht University, Utrecht, Netherlands

    John-Jules Charles Meyer

Rights and permissions

Reprints and permissions

Copyright information

© 2010 Springer Science+Business Media, LLC

About this chapter

Cite this chapter

Bulling, N., Dix, J., Jamroga, W. (2010). Model Checking Logics of Strategic Ability: Complexity*. In: Dastani, M., Hindriks, K., Meyer, JJ. (eds) Specification and Verification of Multi-agent Systems. Springer, Boston, MA. https://doi.org/10.1007/978-1-4419-6984-2_5

Download citation

  • DOI: https://doi.org/10.1007/978-1-4419-6984-2_5

  • Published:

  • Publisher Name: Springer, Boston, MA

  • Print ISBN: 978-1-4419-6983-5

  • Online ISBN: 978-1-4419-6984-2

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation