research-article

Tableau-based decision procedures for logics of strategic ability in multiagent systems

Authors:

Valentin Goranko,

Dmitry ShkatovAuthors Info & Claims

ACM Transactions on Computational Logic (TOCL), Volume 11, Issue 1

Article No.: 3, Pages 1 - 51

https://doi.org/10.1145/1614431.1614434

Published: 06 November 2009 Publication History

Abstract

We develop an incremental tableau-based decision procedure for the alternating-time temporal logic ATL and some of its variants. While running within the theoretically established complexity upper bound, we believe that our tableaux are practically more efficient in the average case than other decision procedures for ATL known so far. Besides, the ease of its adaptation to variants of ATL demonstrates the flexibility of the proposed procedure.

References

[1]

Abate, P., Gorè, R., and Widmann, F. 2007. One-Pass tableaux for computation tree logic. Lecture Notes in Computer Science. Springer-Verlag, 32--46.

Digital Library

[2]

Ågotnes, T., Goranko, V., and Jamroga, W. 2007. Alternating-Time temporal logics with irrevocable strategies. In Proceedings of the 11th International Conference on Theoretical Aspects of Rationality and Knowledge (TARK XI), D. Samet, Ed. 15--24.

Digital Library

[3]

Alur, R., Henzinger, T. A., and Kuperman, O. 1997. Alternating-Time temporal logic. In Proceedings of the 38th IEEE Symposium on Foundations of Computer Science. 100--109.

Digital Library

[4]

Alur, R., Henzinger, T. A., and Kuperman, O. 1998a. Alternating-time temporal logic. Lecture Notes in Computer Science, vol. 1536. Springer-Verlag, 23--60.

Digital Library

[5]

Alur, R., Henzinger, T. A., and Kuperman, O. 2002. Alternating-Time temporal logic. J. ACM 49, 5, 672--713.

Digital Library

[6]

Alur, R., Henzinger, T. A., Mang, F. Y. C., Qadeer, S., Rajamani, S. K., and Tasiran, S. 1998b. Mocha: Modularity in model-checking. Lecture Notes in Computer Science, vol. 1427. Springer-Verlag, 521--525.

Digital Library

[7]

Bradfield, J. and Stirling, C. 2007. Modal μ-calculi. In Handbook of Modal Logic, P. Blackburn, Ed. Elsevier, 721--756.

[8]

Emerson, E. A. 1990. Temporal and modal logics. In Handbook of Theoretical Computer Science, J. van Leeuwen, Ed. Vol. B. MIT Press, 995--1072.

Digital Library

[9]

Emerson, E. A. and Halpern, J. 1985. Decision procedures and expressiveness in the temporal logic of branching time. J. Comput. Syst. Sci. 30, 1, 1--24.

Digital Library

[10]

Fagin, R., Halpern, J. Y., Moses, Y., and Vardi, M. Y. 1995. Reasoning about Knowledge. MIT Press, Cambridge, MA.

Digital Library

[11]

Fitting, M. C. 1983. Proof Methods for Modal and Intuitionistic Logic. D. Reidel Publishing Co.

[12]

Fitting, M. C. 2007. Modal proof theory. In Handbook of Modal Logic, P. Blackburn, J. van Bentem, and F. Wolter, Eds. Elsevier, 85--138.

[13]

Goranko, V. 2001. Coalition games and alternating temporal logics. In Proceedings of the 8th Conference on Theoretical Aspects of Rationality and Knowledge (TARK VIII). J. van Benthem, Ed. Morgan Kaufmann, 259--272.

Digital Library

[14]

Goranko, V. and Jamroga, W. 2004. Comparing semantics of logics for multi-agent systems. Synthese 139, 2, 241--280.

[15]

Goranko, V. and Shkatov, D. 2009. Tableau-Based procedure for deciding satisfiability in the full coalitional multiagent epistemic logic. In Proceedings of Symposium on Logical Foundations of Computer Science (LFCS 2009), S. Artemov and A. Nerode, Eds. Lecture Notes in Computer Science, vol. 5407. Springer-Verlag, 197--213.

Digital Library

[16]

Goranko, V. and Shkatov, D. 2008. Tableau-Based decision procedure for the multi-agent epistemic logic with operators of common and distributed knowledge. In Proceedings of the 6th IEEE International Conference on Sofware Engineering and Formal Methods (SEFM'08), A. Cerone and S. Gunter, Eds. IEEE Computer Society Press, 237--246. Corrected version http://arxiv.org/abs/0808.4133.

Digital Library

[17]

Goranko, V. and van Drimmelen, G. 2006. Complete axiomatization and decidablity of alternating-time temporal logic. Theoretical Comput. Sci. 353, 93--117.

Digital Library

[18]

Goré, R. 1988. Tableau methods for modal and temporal logics. In Handbook of Tableau Methods, M. D'Agostino, D. Gabbay, and R. Hänhle, Eds. Kluwer.

[19]

Hansen, H. H. 2004. Tableau games for coalition logic and alternating-time temporal logic. M.S. thesis, University of Amsterdam.

[20]

Hewitt, C. 1990. The challenge of open systems. In The Foundations of Artificial Intelligence—A Sourcebook, D. Partridge and Y. Wilks, Eds. Cambridge University Press, 383--395.

Digital Library

[21]

Marx, M., Mikulás, S., and Reynolds, M. 2000. The mosaic method for temporal logics. Lecture Notes in Computer Science, vol. 1847. Springer-Verlag, 324--340.

Digital Library

[22]

Pauly, M. 2001a. Logic for social software. Ph.D. thesis. ILLC Dissertation Series 2001-10, University of Amsterdam.

[23]

Pauly, M. 2001b. A logical framework for coalitional effectivity in dynamic procedures. Bull. Econom. Res. 53, 4, 305--324.

[24]

Pauly, M. 2002. A modal logic for coalitional power in games. J. Logic Comput. 12, 1, 149--166.

[25]

Pauly, M. and Parikh, R. 2003. Game logic—An overview. Studia Logica 75, 2, 165--182.

[26]

Shoham, Y. and Leyton-Brown, K. 2008. Multiagent Systems: Algorithmic, Game-Theoretic and Logical Foundations. CUP.

Digital Library

[27]

Smullyan, R. M. 1968. First-Order Logic. Springer-Verlag.

[28]

Thomas, W. 1995. On the synthesis of strategies in infinite games. In Proceedings of the 12th Annual Symposium on Theoretical Aspects of Computer Science (STACS'95), E. Mayr and C. Puech, Eds. Lecture Notes in Computer Science, vol. 900. Springer, 1--13.

[29]

van Drimmelen, G. 2003. Satisfiability in alternating-time temporal logic. In Proceedings of 18th IEEE Symposium on Logic in Computer Science (LICS). 208--217.

Digital Library

[30]

Walther, D., Lutz, C., Wolter, F., and Wooldridge, M. 2006. ATL satisfiability is indeed ExpTime-complete. J. Logic Comput. 16, 6, 765--787.

[31]

Weiss, G., Ed. 1999. Multiagent Systems. MIT Press.

[32]

Wolper, P. 1985. The tableau method for temporal logic: An overview. Logique et Analyse 28, 110--111, 119--136.

[33]

Wooldridge, M. 2002. An Introduction to Multiagent Systems. John Willey and Sons.

Digital Library

Cited By

Arias JOlarte CPenczek WPetrucci LSidoruk T(2024)Model Checking and Synthesis for Strategic Timed CTL using Strategies in Rewriting LogicProceedings of the 26th International Symposium on Principles and Practice of Declarative Programming10.1145/3678232.3678240(1-14)Online publication date: 9-Sep-2024
https://dl.acm.org/doi/10.1145/3678232.3678240
Goranko V(2023)Logics for Strategic Reasoning of Socially Interacting Rational Agents: An Overview and PerspectivesLogics10.3390/logics10100031:1(4-35)Online publication date: 6-Feb-2023
https://doi.org/10.3390/logics1010003
Cheng HMa Z(2023)A tractable temporal description logic for reasoning fuzzy spatiotemporal knowledgeWorld Wide Web10.1007/s11280-023-01180-026:5(3155-3182)Online publication date: 1-Sep-2023
https://dl.acm.org/doi/10.1007/s11280-023-01180-0
Show More Cited By

Index Terms

Tableau-based decision procedures for logics of strategic ability in multiagent systems
1. Computing methodologies
  1. Artificial intelligence
    1. Distributed artificial intelligence
    2. Knowledge representation and reasoning
      1. Temporal reasoning
2. Theory of computation
  1. Logic
    1. Modal and temporal logics

Recommendations

ExpTime Tableau Decision Procedures for Regular Grammar Logics with Converse

Grammar logics were introduced by Fariñas del Cerro and Penttonen in 1988 and have been widely studied. In this paper we consider regular grammar logics with converse (REG ^c logics) and present sound and complete ...
Tableau-based decision procedure for full coalitional multiagent temporal-epistemic logic of linear time
AAMAS '09: Proceedings of The 8th International Conference on Autonomous Agents and Multiagent Systems - Volume 2

We develop a tableau-based decision procedure for the full coalitional multiagent temporal-epistemic logic of linear time CMATEL(CD+LT). It extends LTL with operators of common and distributed knowledge for all coalitions of agents. The tableau ...
Tableau Systems for Some Paraconsistent Modal Logics

In this paper we present tableau-style proof theories for some modal extensions of two paraconsistent propositional logics: RM3, which allows for truth value gluts, and the weaker BN4, which also allows for truth value gaps. These proof theories are ...

Comments

Information & Contributors

Information

Published In

cover image ACM Transactions on Computational Logic

ACM Transactions on Computational Logic Volume 11, Issue 1

October 2009

270 pages

ISSN:1529-3785

EISSN:1557-945X

DOI:10.1145/1614431

Issue’s Table of Contents

Copyright © 2009 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 06 November 2009

Accepted: 01 August 2008

Received: 01 March 2008

Published in TOCL Volume 11, Issue 1

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article
Research
Refereed

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

27
Total Citations
View Citations
212
Total Downloads

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

Reflects downloads up to 07 Mar 2025

Other Metrics

View Author Metrics

Citations

Cited By

Arias JOlarte CPenczek WPetrucci LSidoruk T(2024)Model Checking and Synthesis for Strategic Timed CTL using Strategies in Rewriting LogicProceedings of the 26th International Symposium on Principles and Practice of Declarative Programming10.1145/3678232.3678240(1-14)Online publication date: 9-Sep-2024
https://dl.acm.org/doi/10.1145/3678232.3678240
Goranko V(2023)Logics for Strategic Reasoning of Socially Interacting Rational Agents: An Overview and PerspectivesLogics10.3390/logics10100031:1(4-35)Online publication date: 6-Feb-2023
https://doi.org/10.3390/logics1010003
Cheng HMa Z(2023)A tractable temporal description logic for reasoning fuzzy spatiotemporal knowledgeWorld Wide Web10.1007/s11280-023-01180-026:5(3155-3182)Online publication date: 1-Sep-2023
https://dl.acm.org/doi/10.1007/s11280-023-01180-0
Rybakov MShkatov D(2022)Complexity of finite-variable fragments of propositional temporal and modal logics of computationTheoretical Computer Science10.1016/j.tcs.2022.04.056925(45-60)Online publication date: Aug-2022
https://doi.org/10.1016/j.tcs.2022.04.056
Shkatov DRybakov M(2021)Undecidability of QLTL with two variables and one monadic predicate letterLogical Investigations10.21146/2074-1472-2021-27-2-93-12027:2(93-120)Online publication date: 19-Dec-2021
https://doi.org/10.21146/2074-1472-2021-27-2-93-120
Niewiadomski AKacprzak MKurpiewski DKnapik MPenczek WJamroga WEl Fallah Seghrouchni ASukthankar GAn BYorke-Smith N(2020)MsATLProceedings of the 19th International Conference on Autonomous Agents and MultiAgent Systems10.5555/3398761.3399092(2111-2113)Online publication date: 5-May-2020
https://dl.acm.org/doi/10.5555/3398761.3399092
Goranko VKuusisto ARönnholm R(2019)Alternating-time temporal logic ATL with finitely bounded semanticsTheoretical Computer Science10.1016/j.tcs.2019.05.029Online publication date: Jul-2019
https://doi.org/10.1016/j.tcs.2019.05.029
Bulling NJamroga W(2018)Comparing variants of strategic abilityAutonomous Agents and Multi-Agent Systems10.1007/s10458-013-9231-328:3(474-518)Online publication date: 26-Dec-2018
https://dl.acm.org/doi/10.1007/s10458-013-9231-3
Rybakov MShkatov D(2018)Complexity and Expressivity of Branching- and Alternating-Time Temporal Logics with Finitely Many VariablesTheoretical Aspects of Computing – ICTAC 201810.1007/978-3-030-02508-3_21(396-414)Online publication date: 15-Oct-2018
https://doi.org/10.1007/978-3-030-02508-3_21
Li Y(2017)Tableaux for a combination of propositional dynamic logic and epistemic logic with interactions*Journal of Logic and Computation10.1093/logcom/exx04028:2(451-473)Online publication date: 20-Nov-2017
https://doi.org/10.1093/logcom/exx040
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 Article

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Figures

Tables

Media

View Issue’s Table of Contents