1 Search Results for "Göttlinger, Merlin"

Document
DOI: 10.4230/LIPIcs.CSL.2021.26
The Alternating-Time μ-Calculus with Disjunctive Explicit Strategies

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

Published in: LIPIcs, Volume 183, 29th EACSL Annual Conference on Computer Science Logic (CSL 2021)

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.
Cite as

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)

Copy BibTex To Clipboard

@InProceedings{gottlinger_et_al:LIPIcs.CSL.2021.26,
  author =	{G\"{o}ttlinger, Merlin and Schr\"{o}der, Lutz and Pattinson, Dirk},
  title =	{{The Alternating-Time \mu-Calculus with Disjunctive Explicit Strategies}},
  booktitle =	{29th EACSL Annual Conference on Computer Science Logic (CSL 2021)},
  pages =	{26:1--26:22},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-175-7},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{183},
  editor =	{Baier, Christel and Goubault-Larrecq, Jean},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2021.26},
  URN =		{urn:nbn:de:0030-drops-134605},
  doi =		{10.4230/LIPIcs.CSL.2021.26},
  annote =	{Keywords: Alternating-time logic, multi-agent systems, coalitional strength}
}
  • Refine by Author
  • 1 Göttlinger, Merlin
  • 1 Pattinson, Dirk
  • 1 Schröder, Lutz

  • Refine by Classification
  • 1 Computing methodologies → Multi-agent systems
  • 1 Theory of computation → Modal and temporal logics

  • Refine by Keyword
  • 1 Alternating-time logic
  • 1 coalitional strength
  • 1 multi-agent systems

  • Refine by Type
  • 1 document

  • Refine by Publication Year
  • 1 2021

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