Stochastic Game Logic

Warning

This publication doesn't include Faculty of Arts. It includes Faculty of Informatics. Official publication website can be found on muni.cz.
Authors

BAIER Christel BRÁZDIL Tomáš GRÖßER Marcus KUČERA Antonín

Year of publication 2007
Type Article in Proceedings
Conference Fourth International Conference on the Quantitative Evaluation of Systems (QEST 2007)
MU Faculty or unit

Faculty of Informatics

Citation
Field Informatics
Keywords stochastic systems; temporal logic; model checking
Description Stochastic game logic (SGL) is a new temporal logic that combines features of alternating temporal logic (to formalize the individual views and cooperation and reaction facilities of agents in a multiplayer game), probabilistic computation tree logic and extended temporal logic (to reason about qualitative and quantitative, linear or branching time winning objectives). The paper presents the syntax and semantics of SGL and discusses its model checking problem. The model checking problem of SGL turns out to be undecidable when the strategies are history-dependent. We show PSPACE completeness for memoryless deterministic strategies and the EXPSPACE upper bound for memoryless randomized strategies. For the qualitative fragment of SGL we show PSPACE completeness for memoryless strategies.
Related projects:

You are running an old browser version. We recommend updating your browser to its latest version.