Stochastic Game Logic

Christel BaierChristel Baier, Tomás BrázdilTomás Brázdil, Marcus GrößerMarcus Größer, Antonín KuceraAntonín Kucera

DOI Link

Christel Baier, Tomás Brázdil, Marcus Größer, Antonín Kucera
Stochastic Game Logic
Acta Informatica, 49(4):203--224, 2012

Details
Bibtex

KurzfassungAbstract
Stochastic game logic (SGL) is a new temporal logic for multi-agent systems modeled by turn-based multi-player games with discrete transition probabilities. It combines features of alternating-time temporal logic (ATL), probabilistic computation tree logic and extended temporal logic. SGL contains an ATL-like modality to specify the individual cooperation and reaction facilities of agents in the multi-player game to enforce a certain winning objective. While the standard ATL modality states the existence of a strategy for a certain coalition of agents without restricting the range of strategies for the semantics of inner SGL formulae, we deal with a more general modality. It also requires the existence of a strategy for some coalition, but imposes some kind of strategy binding to inner SGL formulae. This paper presents the syntax and semantics of SGL and discusses its model checking problem for different types of strategies. The model checking problem of SGL turns out to be undecidable when dealing with the full class of history-dependent strategies. We show that the SGL model checking problem for memoryless deterministic strategies as well as the model checking problem of the qualitative fragment of SGL for memoryless randomized strategies is PSPACE-complete, and we establish a close link between natural syntactic fragments of SGL and the polynomial hierarchy. Further, we give a reduction from the SGL model checking problem under memoryless randomized strategies into the Tarski algebra which proves the problem to be in EXPSPACE.
Forschungsgruppe:Research Group: Algebraische und logische Grundlagen der InformatikAlgebraic and Logical Foundations of Computer Science

@article{BBGK2012,
  author  = {Christel Baier and Tom{\'{a}}s Br{\'{a}}zdil and Marcus
             Gr{\"{o}}{\ss}er and Anton{\'{\i}}n Kucera},
  title   = {Stochastic Game Logic},
  journal = {Acta Informatica},
  volume  = {49},
  number  = {4},
  year    = {2012},
  pages   = {203--224},
  doi     = {10.1007/s00236-012-0156-0}
}