TUTCRIS - Tampereen teknillinen yliopisto

TUTCRIS

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

Tutkimustuotosvertaisarvioitu

Yksityiskohdat

AlkuperäiskieliEnglanti
Artikkeli104554
Sivumäärä23
JulkaisuInformation and Computation
DOI - pysyväislinkit
TilaE-pub ahead of print - 2020
OKM-julkaisutyyppiA1 Alkuperäisartikkeli

Tiivistelmä

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.