research-article

On module checking and strategies

Authors:

Wojciech Jamroga,

Aniello MuranoAuthors Info & Claims

AAMAS '14: Proceedings of the 2014 international conference on Autonomous agents and multi-agent systems

Pages 701 - 708

Published: 05 May 2014 Publication History

Abstract

Two decision problems are very close in spirit: module checking of CTL/CTL* and model checking of ATL/ATL*. The latter appears to be a natural multi-agent extension of the former, and it is commonly believed that model checking of ATL(*) subsumes module checking of CTL(*) in a straightforward way. Perhaps because of that, the exact relationship between the two has never been formally established.

A more careful look at the known complexity results, however, makes one realize that the relationship is somewhat suspicious. In particular, module checking of CTL is Exptime-complete, while model checking of ATL is only time-complete. Thus, the (seemingly) less expressive framework yields significantly higher computational complexity than the (seemingly) more expressive one. This suggests that the relationship may not be as simple as believed. In this paper, we show that the difference is indeed fundamental. The way in which behavior of the environment is understood in module checking cannot be equivalently characterized in ATL(*). Conversely, if one wants to embed module checking in ATL(*) then its semantics must be extended with two essential features, namely nondeterministic strategies and long-term commitment to strategies.

References

[1]

T. Ågotnes. Action and knowledge in alternating-time temporal logic. Synthese, 149(2):377--409, 2006. Section on Knowledge, Rationality and Action.

[2]

T. Ågotnes, V. Goranko, and W. Jamroga. Alternating-time temporal logics with irrevocable strategies. In D. Samet, editor, Proceedings of TARK XI, pages 15--24. Presses Universitaires de Louvain, 2007.

Digital Library

[3]

N. Alechina, B. Logan, H. Nguyen, and A. Rakib. Resource-bounded alternating-time temporal logic. In Proceedings of AAMAS, pages 481--488, 2010.

Digital Library

[4]

R. Alur, L. de Alfaro, R. Grossu, T. Henzinger, M. Kang, C. Kirsch, R. Majumdar, F. Mang, and B.-Y. Wang. jMocha: A model-checking tool that exploits design structure. In Proceedings of ICSE, pages 835--836. IEEE Computer Society Press, 2001.

Digital Library

[5]

R. Alur, L. de Alfaro, T. A. Henzinger, S. Krishnan, F. Mang, S. Qadeer, S. Rajamani, and S. Tasiran. MOCHA: Modularity in model checking. Technical report, University of Berkeley, 2000.

[6]

R. Alur, T. Henzinger, O. Kupferman, and M. Vardi. Alternating refinement relations. In Proceedings of CONCUR, LNCS 1466, pages 163--178.Springer, 1998.

Digital Library

[7]

R. Alur, T. A. Henzinger, and O. Kupferman. Alternating-time Temporal Logic. In Proceedings of the 38th Annual Symposium on Foundations of Computer Science (FOCS), pages 100--109. IEEE Computer Society Press, 1997.

Digital Library

[8]

R. Alur, T. A. Henzinger, and O. Kupferman. Alternating-time Temporal Logic. Journal of the ACM, 49:672--713, 2002.

Digital Library

[9]

B. Aminof, A. Legay, A. Murano, O. Serre, and M. Y. Vardi. Pushdown module checking with imperfect information. Inf. Comput., 223(1):1--17, 2013.

Digital Library

[10]

B. Aminof, A. Murano, and M. Vardi. Pushdown module checking with imperfect information. In Proceedings of CONCUR, LNCS 4703, pages 461--476.Springer, 2007.

Digital Library

[11]

S. Basu, P. S. Roop, and R. Sinha. Local module checking for ctl specifications. Electronic Notes in Theoretical Computer Science, 176(2):125--141, 2007.

Digital Library

[12]

L. Bozzelli. New results on pushdown module checking with imperfect information. In Proceedings of GandALF, volume 54 of EPTCS, pages 162--177, 2011.

[13]

L. Bozzelli, A. Murano, and A. Peron. Pushdown module checking. Formal Methods in System Design, 36(1):65--95, 2010.

Digital Library

[14]

T. Brihaye, A. D. C. Lopes, F. Laroussinie, and N. Markey. ATL with strategy contexts and bounded memory. In Proceedings of LFCS, LNCS 5407, pages 92--106. Springer, 2009.

Digital Library

[15]

N. Bulling, J. Dix, and W. Jamroga. Model checking logics of strategic ability: Complexity. In %M. Dastani, K. Hindriks, and J.-J. Meyer, editors, Specification and Verification of Multi-Agent Systems, pages 125--159.Springer, 2010.

[16]

N. Bulling and B. Farwer. On the (un-)decidability of model checking resource-bounded agents. In Proceedings of ECAI, volume 215 of Frontiers in Artificial Intelligence and Applications, pages 567--572. IOS Press, 2010.

Digital Library

[17]

N. Bulling and W. Jamroga. Verifying agents with memory is harder than it seemed. AI Communications, 23:380--403, 2010.

Digital Library

[18]

N. Bulling and W. Jamroga. Comparing variants of strategic ability. Journal of Autonomous Agents and Multi-Agent Systems, 2013.

Digital Library

[19]

K. Chatterjee, T. A. Henzinger, and N. Piterman. Strategy logic. In Proceedings of CONCUR, LNCS 4703, pages 59--73.Springer, 2007.

Digital Library

[20]

T. Chen, V. Forejt, M. Kwiatkowska, D. Parker, and A. Simaitis. PRISM-games: A model checker for stochastic multi-player games. In Proceedings of TACAS, LNCS 7795, pages 185--191. Springer, 2013.

Digital Library

[21]

E. Clarke and E. Emerson. Design and synthesis of synchronization skeletons using branching time temporal logic. In Proceedings of Logics of Programs Workshop, LNCS 131, pages 52--71.Springer, 1981.

Digital Library

[22]

M. Dastani and W. Jamroga. Reasoning about strategies of multi-agent programs. In Proceedings of AAMAS2010, pages 625--632, 2010.

Digital Library

[23]

L. de Alfaro, P. Godefroid, and R. Jagadeesan. Three-valued abstractions of games: Uncertainty, but with precision. In Proceedings of LICS, pages 170--179. IEEE Computer Society, 2004.

Digital Library

[24]

E. Emerson and J. Halpern. "sometimes" and "not never" revisited: On branching versus linear time temporal logic. Journal of the ACM, 33(1):151--178, 1986.

Digital Library

[25]

E. A. Emerson. Temporal and modal logic. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science, volume B, pages 995--1072. Elsevier Science Publishers, 1990.

Digital Library

[26]

A. Ferrante, A. Murano, and M. Parente. Enriched μ-calculi module checking. Logical Methods in Computer Science, 4(3:1):1--21, 2008.

[27]

M. Gesell and K. Schneider. Modular verification of synchronous programs. In Proceedings of ACSD, pages 70--79. IEEE, 2013.

Digital Library

[28]

P. Godefroid. Reasoning about abstract open systems with generalized module checking. In Proceedings of EMSOFT, LNCS 2855, pages 223--240. Springer, 2003.

[29]

P. Godefroid and M. Huth. Model checking vs. generalized model checking: Semantic minimizations for temporal logics. In Proceedings of LICS, pages 158--167. IEEE Computer Society, 2005.

Digital Library

[30]

W. Jamroga and J. Dix. Do agents make model checking explode (computationally)? In P. Petta, and L. Varga, editors, Proceedings of CEEMAS 2005, LNCS 3690, pages 398--407. Springer, 2005.

Digital Library

[31]

W. Jamroga, S. Mauw, and M. Melissen. Fairness in non-repudiation protocols. In Proceedings of STM'11, LNCS 7170, pages 122--139. Springer 2012.

Digital Library

[32]

W. Jamroga and W. van der Hoek. Agents that know how to play. Fundamenta Informaticae, 63(2--3):185--219, 2004.

Digital Library

[33]

M. Kacprzak and W. Penczek. Unbounded model checking for Alternating-time Temporal Logic. In Proceedings of AAMAS-04, 2004.

Digital Library

[34]

S. Kremer and J.-F. Raskin. A game-based verification of non-repudiation and fair exchange protocols. Journal of Computer Security, 11(3), 2003.

Digital Library

[35]

O. Kupferman and M. Vardi. Module checking. In Procee- dings of CAV, LNCS 1102, pages 75--86. Springer, 1996.

Digital Library

[36]

O. Kupferman and M. Vardi. Module checking revisited. In Proceedings of CAV, LNCS 1254, pages 36--47.Springer, 1997.

Digital Library

[37]

O. Kupferman, M. Vardi, and P. Wolper. Module checking. Information and Computation, 164(2):322--344, 2001.

Digital Library

[38]

A. Lomuscio and F. Raimondi. MCMAS : A model checker for multi-agent systems. In Proceedings of TACAS, LNCS 4314, pages 450--454. Springer, 2006.

Digital Library

[39]

F. Martinelli. Module checking through partial model checking. Technical report, CNR Roma - TR-06, 2002.

[40]

F. Martinelli and I. Matteucci. An approach for the specification, verification and synthesis of secure systems. Electronic Notes in Theoretical Computer Science, 168:29--43, 2007.

Digital Library

[41]

F. Mogavero, A. Murano, and M. Vardi. Reasoning about strategies. In Proceedings of FSTTCS, pages 133--144. LIPIcs, 2010.

[42]

F. Mogavero, A. Murano, and M. Vardi. Relentful Strategic Reasoning in Alternating-Time Temporal Logic. In Proceedings of LPAR, LNCS 6355, pages 371--386. Springer, 2010.

Digital Library

[43]

A. Murano, M. Napoli, and M. Parente. Program complexity in hierarchical module checking. In Proceedings of LPAR, LNCS 5330, pages 318--332. Springer, 2008.

Digital Library

[44]

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

[45]

J. Queille and J. Sifakis. Specification and verification of concurrent programs in Cesar. In Symposium on Programming, LNCS 137, pages 337--351. Springer, 1981.

Digital Library

[46]

F. Raimondi. Model Checking Multi-Agent Systems. PhD thesis, University College London, 2006.

[47]

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

[48]

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

[49]

W. van der Hoek, W. Jamroga, and M. Wooldridge. A logic for strategic reasoning. In Proceedings of AAMAS'05, pages 157--164, 2005.

Digital Library

[50]

W. van der Hoek, A. Lomuscio, and M. Wooldridge. On the complexity of practical ATL model checking. In P. Stone and G. Weiss, editors, Proceedings of AAMAS'06, pages 201--208, 2006.

Digital Library

[51]

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

[52]

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

[53]

D. Walther, W. van der Hoek, and M. Wooldridge. Alternating-time temporal logic with explicit strategies. In D. Samet, editor, Proceedings TARK XI, pages 269--278. Presses Universitaires de Louvain, 2007.

Digital Library

[54]

Y. Wang and F. Dechesne. On expressive power and class invariance. CoRR, abs/0905.4332, 2009.

Cited By

Belardinelli FJamroga WKurpiewski DMalvone VMurano A(2019)Strategy logic with simple goalsProceedings of the 28th International Joint Conference on Artificial Intelligence10.5555/3367032.3367046(88-94)Online publication date: 10-Aug-2019
https://dl.acm.org/doi/10.5555/3367032.3367046
Perelli GElkind EVeloso MAgmon NTaylor M(2019)Enforcing Equilibria in Multi-Agent SystemsProceedings of the 18th International Conference on Autonomous Agents and MultiAgent Systems10.5555/3306127.3331692(188-196)Online publication date: 8-May-2019
https://dl.acm.org/doi/10.5555/3306127.3331692
Di Stasio ALambiase PMalvone VMurano AAndre EKoenig SDastani MSukthankar G(2018)Dynamic Escape GameProceedings of the 17th International Conference on Autonomous Agents and MultiAgent Systems10.5555/3237383.3237984(1806-1808)Online publication date: 9-Jul-2018
https://dl.acm.org/doi/10.5555/3237383.3237984
Show More Cited By

Index Terms

On module checking and strategies
1. Computing methodologies
  1. Artificial intelligence
    1. Distributed artificial intelligence
      1. Multi-agent systems
2. Theory of computation
  1. Logic
    1. Modal and temporal logics

Recommendations

Module Checking of Strategic Ability
AAMAS '15: Proceedings of the 2015 International Conference on Autonomous Agents and Multiagent Systems

Module checking is a decision problem proposed in late 1990s to formalize verification of open systems, i.e., systems that must adapt their behavior to the input they receive from the environment. It was recently shown that module checking offers a ...
Pushdown module checking

Model checking is a useful method to verify automatically the correctness of a system with respect to a desired behavior, by checking whether a mathematical model of the system satisfies a formal specification of this behavior. ...
Local Module Checking for CTL Specifications

Model checking is a well known technique for the verification of finite state models using temporal logic specification. While model checking is suitable for transformational systems (also called closed systems), it is unsuitable for open systems (also ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Other conferences

AAMAS '14: Proceedings of the 2014 international conference on Autonomous agents and multi-agent systems

May 2014

1774 pages

ISBN:9781450327381

General Chairs:
Ana Bazzan
UFRGS, Brazil
,
Michael Huhns
University of South Carolina, USA
,
Program Chairs:
Alessio Lomuscio
Imperial College London, UK
,
Paul Scerri
Carnegie Mellon University, USA

Sponsors

IFAAMAS

In-Cooperation

SIGAI: ACM Special Interest Group on Artificial Intelligence

Publisher

International Foundation for Autonomous Agents and Multiagent Systems

Richland, SC

Publication History

Published: 05 May 2014

Check for updates

Author Tags

Qualifiers

Research-article

Conference

AAMAS '14

Sponsor:

AAMAS '14: International conference on Autonomous Agents and Multi-Agent Systems

May 5 - 9, 2014

Paris, France

Acceptance Rates

AAMAS '14 Paper Acceptance Rate 169 of 709 submissions, 24%;

Overall Acceptance Rate 1,155 of 5,036 submissions, 23%

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

12
Total Citations
View Citations
96
Total Downloads

Downloads (Last 12 months)3
Downloads (Last 6 weeks)0

Reflects downloads up to 19 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Belardinelli FJamroga WKurpiewski DMalvone VMurano A(2019)Strategy logic with simple goalsProceedings of the 28th International Joint Conference on Artificial Intelligence10.5555/3367032.3367046(88-94)Online publication date: 10-Aug-2019
https://dl.acm.org/doi/10.5555/3367032.3367046
Perelli GElkind EVeloso MAgmon NTaylor M(2019)Enforcing Equilibria in Multi-Agent SystemsProceedings of the 18th International Conference on Autonomous Agents and MultiAgent Systems10.5555/3306127.3331692(188-196)Online publication date: 8-May-2019
https://dl.acm.org/doi/10.5555/3306127.3331692
Di Stasio ALambiase PMalvone VMurano AAndre EKoenig SDastani MSukthankar G(2018)Dynamic Escape GameProceedings of the 17th International Conference on Autonomous Agents and MultiAgent Systems10.5555/3237383.3237984(1806-1808)Online publication date: 9-Jul-2018
https://dl.acm.org/doi/10.5555/3237383.3237984
Kong JLomuscio AAndre EKoenig SDastani MSukthankar G(2018)Model Checking Multi-Agent Systems against LDLK Specifications on Finite TracesProceedings of the 17th International Conference on Autonomous Agents and MultiAgent Systems10.5555/3237383.3237414(166-174)Online publication date: 9-Jul-2018
https://dl.acm.org/doi/10.5555/3237383.3237414
Malvone VMurano ASorrentino LLarson KWinikoff MDas SDurfee E(2017)Hiding Actions in Multi-Player GamesProceedings of the 16th Conference on Autonomous Agents and MultiAgent Systems10.5555/3091125.3091293(1205-1213)Online publication date: 8-May-2017
https://dl.acm.org/doi/10.5555/3091125.3091293
Huang XChen QMeng JSu K(2016)Reconfigurability in reactive multiagent systemsProceedings of the Twenty-Fifth International Joint Conference on Artificial Intelligence10.5555/3060621.3060666(315-321)Online publication date: 9-Jul-2016
https://dl.acm.org/doi/10.5555/3060621.3060666
Chen TSong FWu Z(2016)Verifying pushdown multi-agent systems against strategy logicsProceedings of the Twenty-Fifth International Joint Conference on Artificial Intelligence10.5555/3060621.3060647(180-186)Online publication date: 9-Jul-2016
https://dl.acm.org/doi/10.5555/3060621.3060647
Malvone VMurano ASorrentino LJonker CMarsella SThangarajah JTuyls K(2016)Concurrent Multi-Player Parity GamesProceedings of the 2016 International Conference on Autonomous Agents & Multiagent Systems10.5555/2936924.2937026(689-697)Online publication date: 9-May-2016
https://dl.acm.org/doi/10.5555/2936924.2937026
Malvone VMurano ASorrentino L(2016)Hiding actions in concurrent gamesProceedings of the Twenty-second European Conference on Artificial Intelligence10.3233/978-1-61499-672-9-1686(1686-1687)Online publication date: 29-Aug-2016
https://dl.acm.org/doi/10.3233/978-1-61499-672-9-1686
Jamroga WMurano AWeiss GYolum PBordini RElkind E(2015)Module Checking of Strategic AbilityProceedings of the 2015 International Conference on Autonomous Agents and Multiagent Systems10.5555/2772879.2772911(227-235)Online publication date: 4-May-2015
https://dl.acm.org/doi/10.5555/2772879.2772911
Show More Cited By

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Table of Contents