ATL with Strategy Contexts: Expressiveness and Model Checking

Da Costa, Arnaud; Laroussinie, François; Markey, Nicolas

doi:10.4230/LIPIcs.FSTTCS.2010.120

Document

ATL with Strategy Contexts: Expressiveness and Model Checking

Authors Arnaud Da Costa, François Laroussinie, Nicolas Markey

Part of: Volume: IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2010)
Part of: Series: Leibniz International Proceedings in Informatics (LIPIcs)
Part of: Conference: IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS)
License: Creative Commons Attribution-NonCommercial-NoDerivs 3.0 Unported license
Publication Date: 2010-12-14

PDF

File

PDF

LIPIcs.FSTTCS.2010.120.pdf

Filesize: 0.57 MB
13 pages

Document Identifiers

DOI: 10.4230/LIPIcs.FSTTCS.2010.120
URN: urn:nbn:de:0030-drops-28589

Subject Classification

Keywords

alternating temporal logic
agent
strategy quantifier

Metrics

Access Statistics
Total Accesses (updated on a weekly basis)

0

PDF Downloads

0

Metadata Views

Abstract

We study the alternating-time temporal logics ATL and ATL* extended with strategy contexts: these make agents commit to their strategies during the evaluation of formulas, contrary to plain ATL and ATL* where strategy quantifiers reset previously selected strategies.

We illustrate the important expressive power of strategy contexts by proving that they make the extended logics, namely ATLsc and ATLsc*, equally expressive: any formula in ATLsc* can be translated into an equivalent, linear-size ATLsc formula.  Despite the high expressiveness of these logics, we~prove that their model-checking problems remain decidable by~designing a tree-automata-based algorithm for model-checking ATLsc* on the full class of $n$-player concurrent game structures.

Cite As Get BibTex

Arnaud Da Costa, François Laroussinie, and Nicolas Markey. ATL with Strategy Contexts: Expressiveness and Model Checking. In IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2010). Leibniz International Proceedings in Informatics (LIPIcs), Volume 8, pp. 120-132, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2010) https://doi.org/10.4230/LIPIcs.FSTTCS.2010.120

Author Details

Arnaud Da Costa

François Laroussinie

Nicolas Markey

Questions / Remarks / Feedback

Feedback for Dagstuhl Publishing

Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail