Stochastic Game Logic

Research output: Contribution to journalResearch articleContributedpeer-review

Contributors

Abstract

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.

Details

Original languageEnglish
Pages (from-to)203-224
Number of pages22
JournalActa Informatica
Volume49
Issue number4
Publication statusPublished - 2012
Peer-reviewedYes

External IDs

Scopus 84862328345
ORCID /0000-0002-5321-9343/work/142236665

Keywords

Keywords

  • turn-based multiplayer games, model checking

Library keywords