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

Valentin Goranko, Antti Kuusisto, Raine Rönnholm

Research output: Contribution to journalArticleScientificpeer-review


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.

Original languageEnglish
Article number104554
Number of pages23
JournalInformation and Computation
Early online date2020
Publication statusPublished - 2021
Publication typeA1 Journal article-refereed


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

Publication forum classification

  • Publication forum level 2

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Information Systems
  • Computer Science Applications
  • Computational Theory and Mathematics


Dive into the research topics of 'Game-theoretic semantics for ATL+ with applications to model checking'. Together they form a unique fingerprint.

Cite this