Change search
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf
Game-theoretic semantics for ATL(+) with applications to model checking
Stockholm University, Faculty of Humanities, Department of Philosophy. University of Johannesburg, South Africa.
Number of Authors: 32021 (English)In: Information and Computation, ISSN 0890-5401, E-ISSN 1090-2651, Vol. 276, article id 104554Article in journal (Refereed) Published
Abstract [en]

We develop a game-theoretic semantics (GTS) for the fragment ATL(+) of the alternating-time temporal logic ATL*, thereby extending the recently introduced GTS for ATL. We show that the game-theoretic semantics is equivalent to the standard compositional semantics of ATL(+) with perfect-recall strategies. Based on the new semantics, we provide an analysis of the memory and time resources needed for model checking ATL(+) and show that strategies of the verifier that use only a very limited amount of memory suffice. Furthermore, using the GTS, we provide a new algorithm for model checking ATL(+) and identify a natural hierarchy of tractable fragments of ATL(+) that substantially extend ATL.

Place, publisher, year, edition, pages
2021. Vol. 276, article id 104554
Keywords [en]
Game-theoretic semantics, Alternating-time temporal logic, Algorithmic model checking, Tractable fragments, Finite memory strategies
National Category
Computer and Information Sciences
Identifiers
URN: urn:nbn:se:su:diva-191334DOI: 10.1016/j.ic.2020.104554ISI: 000607516300005OAI: oai:DiVA.org:su-191334DiVA, id: diva2:1537611
Available from: 2021-03-16 Created: 2021-03-16 Last updated: 2022-02-25Bibliographically approved

Open Access in DiVA

No full text in DiVA

Other links

Publisher's full text

Authority records

Goranko, Valentin

Search in DiVA

By author/editor
Goranko, Valentin
By organisation
Department of Philosophy
In the same journal
Information and Computation
Computer and Information Sciences

Search outside of DiVA

GoogleGoogle Scholar

doi
urn-nbn

Altmetric score

doi
urn-nbn
Total: 104 hits
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf