Document Open Access Logo

The Alternating-Time μ-Calculus with Disjunctive Explicit Strategies

Authors Merlin Göttlinger , Lutz Schröder , Dirk Pattinson

PDF
Thumbnail PDF

File

LIPIcs.CSL.2021.26.pdf
  • Filesize: 0.61 MB
  • 22 pages

Document Identifiers

Author Details

Merlin Göttlinger
  • Friedrich-Alexander-Universität Erlangen-Nürnberg, Erlangen, Germany
Lutz Schröder
  • Friedrich-Alexander-Universität Erlangen-Nürnberg, Erlangen, Germany
Dirk Pattinson
  • The Australian National University, Canberra, Australia

Funding

  • Göttlinger, Merlin: Work performed under the DFG Project Reconstructing Arguments from Noisy Text (RANT), SCHR 1118/14-1 / SCHR 1118/14-2.
  • Schröder, Lutz: Work performed under the DFG Project RANT, SCHR 1118/14-1 / SCHR 1118/14-2.

Cite AsGet BibTex

Merlin Göttlinger, Lutz Schröder, and Dirk Pattinson. The Alternating-Time μ-Calculus with Disjunctive Explicit Strategies. In 29th EACSL Annual Conference on Computer Science Logic (CSL 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 183, pp. 26:1-26:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
https://doi.org/10.4230/LIPIcs.CSL.2021.26

Abstract

Alternating-time temporal logic (ATL) and its extensions, including the alternating-time µ-calculus (AMC), serve the specification of the strategic abilities of coalitions of agents in concurrent game structures. The key ingredient of the logic are path quantifiers specifying that some coalition of agents has a joint strategy to enforce a given goal. This basic setup has been extended to let some of the agents (revocably) commit to using certain named strategies, as in ATL with explicit strategies (ATLES). In the present work, we extend ATLES with fixpoint operators and strategy disjunction, arriving at the alternating-time µ-calculus with disjunctive explicit strategies (AMCDES), which allows for a more flexible formulation of temporal properties (e.g. fairness) and, through strategy disjunction, a form of controlled non-determinism in commitments. Our main result is an ExpTime upper bound for satisfiability checking (which is thus ExpTime-complete). We also prove upper bounds QP (quasipolynomial time) and NP∩coNP for model checking under fixed interpretations of explicit strategies, and NP under open interpretation. Our key technical tool is a treatment of the AMCDES within the generic framework of coalgebraic logic, which in particular reduces the analysis of most reasoning tasks to the treatment of a very simple one-step logic featuring only propositional operators and next-step operators without nesting; we give a new model construction principle for this one-step logic that relies on a set-valued variant of first-order resolution.

Subject Classification

ACM Subject Classification
  • Theory of computation → Modal and temporal logics
  • Computing methodologies → Multi-agent systems
Keywords
  • Alternating-time logic
  • multi-agent systems
  • coalitional strength

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

References

  1. Rajeev Alur, Thomas Henzinger, and Orna Kupferman. Alternating-time temporal logic. J. ACM, 49:672-713, 2002. URL: https://doi.org/10.1145/585265.585270.
  2. Cristian Calude, Sanjay Jain, Bakhadyr Khoussainov, Wei Li, and Frank Stephan. Deciding parity games in quasipolynomial time. In Theory of Computing, STOC 2017, pages 252-263. ACM, 2017. Google Scholar
  3. Krishnendu Chatterjee, Thomas A. Henzinger, and Nir Piterman. Strategy logic. Inf. Comput., 208(6):677-693, 2010. URL: https://doi.org/10.1016/j.ic.2009.07.004.
  4. Corina Cîrstea, Clemens Kupke, and Dirk Pattinson. EXPTIME tableaux for the coalgebraic μ-calculus. Log. Methods Comput. Sci., 7(3), 2011. URL: https://doi.org/10.2168/LMCS-7(3:3)2011.
  5. Corina Cîrstea, Alexander Kurz, Dirk Pattinson, Lutz Schröder, and Yde Venema. Modal logics are coalgebraic. Comput. J., 54(1):31-41, 2011. URL: https://doi.org/10.1093/comjnl/bxp004.
  6. Melvin Fitting. First-Order Logic and Automated Theorem Proving. Springer, 2nd edition, 1996. URL: https://doi.org/10.1007/978-1-4612-2360-3.
  7. Valentin Goranko and Fengkui Ju. Towards a logic for conditional local strategic reasoning. In Patrick Blackburn, Emiliano Lorini, and Meiyun Guo, editors, Logic, Rationality, and Interaction, LORI 2019, volume 11813 of LNCS, pages 112-125. Springer, October 2019. URL: https://doi.org/10.1007/978-3-662-60292-8_9.
  8. Valentin Goranko and Govert van Drimmelen. Complete axiomatization and decidability of alternating-time temporal logic. Theor. Comput. Sci., 353(1-3):93-–117, March 2006. URL: https://doi.org/10.1016/j.tcs.2005.07.043.
  9. Rajeev Goré, Clemens Kupke, Dirk Pattinson, and Lutz Schröder. Global caching for coalgebraic description logics. In Automated Reasoning, IJCAR 2010, volume 6173 of LNCS, pages 46-60. Springer, 2010. URL: https://doi.org/10.1007/978-3-642-14203-1.
  10. Erich Grädel, Wolfgang Thomas, and Thomas Wilke, editors. Automata, Logics, and Infinite Games: A Guide to Current Research, volume 2500 of LNCS. Springer, 2002. URL: https://doi.org/10.1007/3-540-36387-4.
  11. Daniel Hausmann and Lutz Schröder. Game-based local model checking for the coalgebraic mu-calculus. In Concurrency Theory, CONCUR 2019, volume 140 of LIPIcs, pages 35:1-35:16. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, August 2019. URL: https://doi.org/10.4230/LIPIcs.CONCUR.2019.35.
  12. Andreas Herzig, Emiliano Lorini, and Dirk Walther. Reasoning about actions meets strategic logics. In Logic, Rationality, and Interaction, LORI 2013, volume 8196 of LNCS, pages 162-175. Springer, 2013. URL: https://doi.org/10.1007/978-3-642-40948-6_13.
  13. Marc-Uwe Kling. Das Känguru-Manifest. Ullstein, Berlin, 2011. Google Scholar
  14. Marc-Uwe Kling. The Kangaroo Chronicles. Voland & Quist, 2016. Translated by Sarah Cossaboon and Paul-Henri Campbell. Google Scholar
  15. Fabio Mogavero, Aniello Murano, Giuseppe Perelli, and Moshe Vardi. Reasoning about strategies: On the model-checking problem. ACM Trans. Comput. Log., 15(4):34:1-34:47, 2014. URL: https://doi.org/10.1145/2631917.
  16. Fabio Mogavero, Aniello Murano, Giuseppe Perelli, and Moshe Vardi. Reasoning about strategies: on the satisfiability problem. LMCS, 13(1), 2017. URL: https://doi.org/10.23638/LMCS-13(1:9)2017.
  17. Robert Myers, Dirk Pattinson, and Lutz Schröder. Coalgebraic hybrid logic. In Foundations of Software Science and Computational Structures, FOSSACS 2009, volume 5504 of LNCS, pages 137-151. Springer, 2009. URL: https://doi.org/10.1007/978-3-642-00596-1.
  18. Rocco De Nicola and Frits W. Vaandrager. Action versus state based logics for transition systems. In Irène Guessarian, editor, Semantics of Systems of Concurrent Processes, LITP Spring School on Theoretical Computer Science 1990, volume 469 of LNCS, pages 407-419. Springer, April 1990. URL: https://doi.org/10.1007/3-540-53479-2_17.
  19. Dirk Pattinson and Lutz Schröder. Cut elimination in coalgebraic logics. Inf. Comput., 208(12):1447-1468, 2010. URL: https://doi.org/10.1016/j.ic.2009.11.008.
  20. Marc Pauly. A modal logic for coalitional power in games. J. Log. Comput., 12(1):149-166, 2002. URL: https://doi.org/10.1093/logcom/12.1.149.
  21. Sven Schewe. Synthesis of Distributed Systems. PhD thesis, Universität des Saarlandes, 2008. Google Scholar
  22. Lutz Schröder and Dirk Pattinson. PSPACE bounds for rank-1 modal logics. ACM Trans. Comput. Log., 10(2):13:1-13:33, 2009. URL: https://doi.org/10.1145/1462179.1462185.
  23. Lutz Schröder and Dirk Pattinson. Modular algorithms for heterogeneous modal logics via multi-sorted coalgebra. Math. Struct. Comput. Sci., 21(2):235-266, 2011. URL: https://doi.org/10.1017/S0960129510000563.
  24. Lutz Schröder, Dirk Pattinson, and Clemens Kupke. Nominals for everyone. In International Joint Conference on Artificial Intelligence, IJCAI 2009, pages 917-922, July 2009. URL: http://ijcai.org/proceedings/2009.
  25. Lutz Schröder and Yde Venema. Completeness of flat coalgebraic fixpoint logics. ACM Trans. Comput. Log., 19(1):4:1-4:34, 2018. URL: https://doi.org/10.1145/3157055.
  26. Wiebe van der Hoek, Wojciech Jamroga, and Michael Wooldridge. A logic for strategic reasoning. In Autonomous Agents and Multiagent Systems, AAMAS 2005, pages 157-164. ACM, 2005. URL: https://doi.org/10.1145/1082473.1082497.
  27. Govert van Drimmelen. Satisfiability in alternating-time temporal logic. In Logic in Computer Science, LICS 2003, pages 208-217. IEEE Comp. Soc., June 2003. URL: https://doi.org/10.1109/LICS.2003.1210060.
  28. Dirk Walther. Strategic Logics: Complexity, Completeness and Expressivity. PhD thesis, University of Liverpool, 2007. Google Scholar
  29. Dirk Walther, Wiebe van der Hoek, and Michael Wooldridge. Alternating-time temporal logic with explicit strategies. In Theoretical Aspects of Rationality and Knowledge, TARK 2007, pages 269-278. ACM Press, 2007. URL: https://doi.org/10.1145/1324249.1324285.
  30. Thomas Ågotnes. Action and knowledge in alternating-time temporal logic. Synthese, 149(2):375–407, March 2006. URL: https://doi.org/10.1007/s11229-005-3875-8.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact