Name
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. |
Year | DOI | Venue |
|---|---|---|
2012 | 10.1007/s00236-012-0156-0 | Acta Inf. |
Keywords | Field | DocType |
atl-like modality,new temporal logic,sgl model checking problem,alternating-time temporal logic,stochastic game logic,memoryless randomized strategy,probabilistic computation tree logic,inner sgl formula,model checking problem,extended temporal logic | Polynomial hierarchy,Discrete mathematics,Combinatorics,Model checking,Computer science,Probabilistic CTL,EXPSPACE,Temporal logic,Semantics,Stochastic game,Undecidable problem | Journal |
Volume | Issue | ISSN |
49 | 4 | 1432-0525 |
Citations | PageRank | References |
2 | 0.39 | 20 |
Authors | ||
4 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Christel Baier | 1 | 3053 | 185.85 |
| Tomáš Brázdil | 2 | 194 | 13.11 |
| Marcus Größer | 3 | 334 | 18.23 |
| Antonín Kučera | 4 | 262 | 18.04 |