Game-Theoretic Semantics for ATL+ with Applications to Model Checking
Logic
2019-06-17 v2 Computer Science and Game Theory
Logic in Computer Science
Abstract
We develop game-theoretic semantics (GTS) for the fragment ATL+ of the full Alternating-time Temporal Logic ATL*, essentially extending a recently introduced GTS for ATL. We first show that the new game-theoretic semantics is equivalent to the standard semantics of ATL+ (based on perfect recall strategies). We then provide an analysis, based on the new semantics, of the memory and time resources needed for model checking ATL+. Based on that, we establish that strategies that use only a very limited amount of memory suffice for ATL+. Furthermore, using the GTS we provide a new algorithm for model checking of ATL+ and identify a natural hierarchy of tractable fragments of ATL+ that extend ATL.
Cite
@article{arxiv.1702.08405,
title = {Game-Theoretic Semantics for ATL+ with Applications to Model Checking},
author = {Valentin Goranko and Antti Kuusisto and Raine Rönnholm},
journal= {arXiv preprint arXiv:1702.08405},
year = {2019}
}
Comments
Extended version of a paper in AAMAS2017