Tampere University of Technology

TUTCRIS Research Portal

Game-theoretic semantics for ATL+ with applications to model checking

Research output: Contribution to journalArticleScientificpeer-review

Standard

Game-theoretic semantics for ATL+ with applications to model checking. / Goranko, Valentin; Kuusisto, Antti; Rönnholm, Raine.

In: Information and Computation, 2020.

Research output: Contribution to journalArticleScientificpeer-review

Harvard

APA

Vancouver

Author

Goranko, Valentin ; Kuusisto, Antti ; Rönnholm, Raine. / Game-theoretic semantics for ATL+ with applications to model checking. In: Information and Computation. 2020.

Bibtex - Download

@article{209f3ab296484ae9ac6b18e5c6286297,
title = "Game-theoretic semantics for ATL+ with applications to model checking",
abstract = "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.",
keywords = "Algorithmic model checking, Alternating-time temporal logic, Finite memory strategies, Game-theoretic semantics, Tractable fragments",
author = "Valentin Goranko and Antti Kuusisto and Raine R{\"o}nnholm",
year = "2020",
doi = "10.1016/j.ic.2020.104554",
language = "English",
journal = "Information and Computation",
issn = "0890-5401",
publisher = "Elsevier",

}

RIS (suitable for import to EndNote) - Download

TY - JOUR

T1 - Game-theoretic semantics for ATL+ with applications to model checking

AU - Goranko, Valentin

AU - Kuusisto, Antti

AU - Rönnholm, Raine

PY - 2020

Y1 - 2020

N2 - 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.

AB - 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.

KW - Algorithmic model checking

KW - Alternating-time temporal logic

KW - Finite memory strategies

KW - Game-theoretic semantics

KW - Tractable fragments

U2 - 10.1016/j.ic.2020.104554

DO - 10.1016/j.ic.2020.104554

M3 - Article

JO - Information and Computation

JF - Information and Computation

SN - 0890-5401

M1 - 104554

ER -