Game-theoretic semantics for ATL+ with applications to model checking
Research output: Contribution to journal › Article › Scientific › peer-review
|Journal||Information and Computation|
|Publication status||E-pub ahead of print - 2020|
|Publication type||A1 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.
ASJC Scopus subject areas
- Algorithmic model checking, Alternating-time temporal logic, Finite memory strategies, Game-theoretic semantics, Tractable fragments