Tampere University of Technology

TUTCRIS Research Portal

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

Research output: Contribution to journalArticleScientificpeer-review


Original languageEnglish
Article number104554
Number of pages23
JournalInformation and Computation
Publication statusE-pub ahead of print - 2020
Publication typeA1 Journal article-refereed


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.


  • Algorithmic model checking, Alternating-time temporal logic, Finite memory strategies, Game-theoretic semantics, Tractable fragments

Publication forum classification

Field of science, Statistics Finland