Article

The complexity of model checking succinct multiagent systems

Authors:

Qingliang Chen,

Kaile SuAuthors Info & Claims

IJCAI'15: Proceedings of the 24th International Conference on Artificial Intelligence

Pages 1076 - 1082

Published: 25 July 2015 Publication History

Abstract

This paper studies the complexity of model checking multiagent systems, in particular systems succinctly described by two practical representations: concurrent representation and symbolic representation. The logics we concern include branching time temporal logics and several variants of alternating time temporal logics.

References

[1]

Rajeev Alur, Thomas A. Henzinger, and Orna Kupferman. Alternating-Time Temporal Logic. Journal of the ACM, 49(5):672-713, 2002.

Digital Library

[2]

Simon Busard, Charles Pecheur, Hongyang Qu, and Franco Raimondi. Reasoning about strategies under partial observability and fairness constraints. In 1st Workshop on Strategic Reasoning 2013 (SR'13), pages 71-79, 2013.

[3]

Petr Cermák, Alessio Lomuscio, Fabio Mogavero, and Aniello Murano. Mcmas-slk: A model checker for the verification of strategy logic specifications. In 26th International Conference on Computer Aided Verification (CAV2014), pages 525-532, 2014.

Digital Library

[4]

Ashok K. Chandra, Dexter C. Kozen, and Larry J. Stockmeyer. Alternation. Journal of the ACM, 28(1):114-133, 1980.

Digital Library

[5]

Alessandro Cimatti, Edmund Clarke, Enrico Giunchiglia, Fausto Giunchiglia, Marco Pistore, Marco Roveri, Roberto Sebastiani, and Armando Tacchella. Nusmv 2: An opensource tool for symbolic model checking. In 14th International Conference on Computer Aided Verification (CAV2002), pages 359-364, 2002.

Digital Library

[6]

E. M. Clarke, E. Allen Emerson, and A. P. Sistla. Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM Transactions on Programming Languages and Systems, 8(2):244-263, 1986.

Digital Library

[7]

E. Clarke, O. Grumberg, and D. Peled. Model Checking. The MIT Press, 1999.

Digital Library

[8]

E. Allen Emerson and Chin-Laung Lei. Modalities for model checking: branching time logic strikes back. Science of Computer Programming, 8(3):275-306, 1987.

Digital Library

[9]

Ronald Fagin, Joseph Y. Halpern, Yoram Moses, and Moshe Y. Vardi. Reasoning About Knowledge. The MIT Press, 1995.

Digital Library

[10]

P. Gammie and R. van der Meyden. MCK: Model Checking the Logic of Knowledge. In Proc. Conf. on Computer-Aided Verification, CAV, pages 479-483, 2004.

[11]

Dimitar P. Guelev, Catalin Dima, and Constantin Enea. An alternating-time temporal logic with knowledge, perfect recall and past: axiomatisation and model-checking. Journal of Applied Non-Classical Logics, 21(1):93-131, 2011.

[12]

Xiaowei Huang and Ron van der Meyden. The complexity of epistemic model checking: Clock semantics and branching time. In 19th European Conference on Artificial Intelligence (ECAI2010), pages 549-554, 2010.

Digital Library

[13]

Xiaowei Huang and Ron van der Meyden. An epistemic strategy logic. In the 2nd International Workshop on Strategic Reasoning (SR2014), pages 35-41, 2014.

[14]

Xiaowei Huang and Ron van der Meyden. Symbolic model checking epistemic strategy logic. In Proceedings of the the Twenty-Eighth AAAI Conference on Artificial Intelligence (AAAI- 14), 2014.

Digital Library

[15]

Xiaowei Huang and Ron van der Meyden. A temporal logic of strategic knowledge. In the 14th International Conference on Principles of Knowledge Representation and Reasoning (KR2014), 2014.

[16]

Xiaowei Huang. Bounded model checking of strategy ability with perfect recall. Artificial Intelligence, pages 182-200, 2015.

Digital Library

[17]

Wojciech Jamroga and Thomas Agotnes. Modular interpreted systems. In Proceedings of the Sixth International Joint Conference on Autonomous Agents and Multiagent Systems (AAMAS'07), page 131, 2007.

Digital Library

[18]

Wojciech Jamroga and Jurgen Dix. Model checking abilities of agents: A closer look. Theory of Computing Systems, 42(3):366-410, 2008.

Digital Library

[19]

Magdalena Kacprzak, Wojciech Nabialek, Artur Niewiadomski, Wojciech Penczek, Agata Półrola, Maciej Szreter, Bozena Wozna, and Andrzej Zbrzezny. VerICS 2007 - a Model Checker for Knowledge and Real-Time. Fundamenta Informaticae, 85(1):313-328, 2008.

Digital Library

[20]

Orna Kupferman, Moshe Y. Vardi, and Pierre Wolper. An automata-theoretic approach to branching-time model checking. J. ACM, 47(2):312-360, 2000.

Digital Library

[21]

Alessio Lomuscio and Franco Raimondi. Model Checking Knowledge, Strategies, and Games in Multi-Agent Systems. In the proceedings of the 5th international joint conference on Autonomous agents and multiagent systems (AAMAS 2006), pages 161-168, 2006.

Digital Library

[22]

Alessio Lomuscio, Hongyang Qu, and Franco Raimondi. MCMAS: A Model Checker for the Verification of Multi-Agent Systems. In Proc. Conf. on Computer-Aided Verification, pages 682-688, 2009.

Digital Library

[23]

Gary Peterson, John Reif, and Salman Azhar. Lower bounds for multiplayer non-cooperative games of incomplete information. Computers and Mathematics with Applications, 41:957-992, 2001.

[24]

Amir Pnueli. The Temporal Logic of Programs. In Symp. on Foundations of Computer Science, pages 46-57, 1977.

Digital Library

[25]

Walter J. Savitch. Relationships between nondeterministic and deterministic tape complexities. Journal of Computer and System Sciences, 4(2):177-192, 1970.

Digital Library

[26]

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

[27]

Ron van der Meyden and Nikolay V. Shilov. Model Checking Knowledge and Time in Systems with Perfect Recall. In Foundations of Software Technology and Theoretical Computer Science, pages 432-445, 1999.

Digital Library

[28]

Moshe Y. Vardi and Pierre Wolper. Automata theoretic techniques for modal logics of programs. Journal of Computer and System Sciences, 32(2):183-221, 1986.

Digital Library

Cited By

Bozzelli LMaubert BMurano A(2019)The complexity of model checking knowledge and timeProceedings of the 28th International Joint Conference on Artificial Intelligence10.5555/3367243.3367260(1595-1601)Online publication date: 10-Aug-2019
https://dl.acm.org/doi/10.5555/3367243.3367260
Huang XChen QSu K(2016)Strengthening agents strategic ability with communicationProceedings of the Thirtieth AAAI Conference on Artificial Intelligence10.5555/3016100.3016251(2509-2515)Online publication date: 12-Feb-2016
https://dl.acm.org/doi/10.5555/3016100.3016251

The complexity of model checking succinct multiagent systems
1. Software and its engineering
  1. Software organization and properties
    1. Software functional properties
      1. Formal methods
2. Theory of computation
  1. Logic

Recommendations

On the complexity of practical ATL model checking
AAMAS '06: Proceedings of the fifth international joint conference on Autonomous agents and multiagent systems

We investigate the computational complexity of reasoning about multi-agent systems using the cooperation logic ATL of Alur, Henzinger, and Kupferman. It is known that satisfiability checking is EXPTIME-complete for "full" ATL, and PSPACE-complete (in ...
Complexity of model checking for modal dependence logic
SOFSEM'12: Proceedings of the 38th international conference on Current Trends in Theory and Practice of Computer Science

Modal dependence logic (MDL) was introduced recently by Väänänen. It enhances the basic modal language by an operator = (·). For propositional variables <em>p</em> ₁ ,…,<em>p</em> _<em>n</em> the atomic formula = (<em>p</em> ₁ ,…,<em>p</em> _{<em>n</em> −...}
Well-structured model checking of multiagent systems
PSI'06: Proceedings of the 6th international Andrei Ershov memorial conference on Perspectives of systems informatics

We address model checking problem for combination of Computation Tree Logic (CTL) and Propositional Logic of Knowledge (PLK) in finite systems with the perfect recall synchronous semantics. We have published already an (update+abstraction)-algorithm for ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Guide Proceedings

IJCAI'15: Proceedings of the 24th International Conference on Artificial Intelligence

July 2015

4429 pages

ISBN:9781577357384

Editors:
Qiang Yang
Hong Kong University of Science and Technology
,
Michael Wooldridge
University of Oxford

Sponsors

The International Joint Conferences on Artificial Intelligence, Inc. (IJCAI)

Publisher

AAAI Press

Publication History

Published: 25 July 2015

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

2
Total Citations
View Citations
0
Total Downloads

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

Reflects downloads up to 18 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Bozzelli LMaubert BMurano A(2019)The complexity of model checking knowledge and timeProceedings of the 28th International Joint Conference on Artificial Intelligence10.5555/3367243.3367260(1595-1601)Online publication date: 10-Aug-2019
https://dl.acm.org/doi/10.5555/3367243.3367260
Huang XChen QSu K(2016)Strengthening agents strategic ability with communicationProceedings of the Thirtieth AAAI Conference on Artificial Intelligence10.5555/3016100.3016251(2509-2515)Online publication date: 12-Feb-2016
https://dl.acm.org/doi/10.5555/3016100.3016251

View Options

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

Media

Figures

Other

Tables

View Table of Contents