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.
Article PDF
Similar content being viewed by others
Avoid common mistakes on your manuscript.
References
Ågotnes, T., Goranka, V., Jamroga, W.: Alternating-time temporal logic with irrevocable strategies. In: 11th Confernce on Theoretical Aspects of Rationality and Knowledge (TARK’07), pp. 15–24 (2007)
Alur R., Henzinger T.A., Kupferman O.: Alternating-time temporal logic. J. ACM 49, 672–713 (2002)
Baier, C., Brázdil, T., Größer, M., Kučera, A.: Stocahstic game logic. In: Fourth International Conference on Quantitative Evaluation of Systems (QEST’07), pp. 227–236. IEEE Computer Society Press, Los Alamos (2007)
Baier, C., Größer, M., Leucker, M., Ciesinski, F., Bollig, B.: Controller synthesis for probabilistic systems. In: IFIP Worldcongress, Theoretical Computer Science (2004)
Baier C., Katoen J.-P.: Principles of Model Checking. MIT Press, Cambridge (2008)
Bianco, A., de Alfaro, L.: Model checking of probabilistic and nondeterministic systems. In: Thiagarajan, P.S. (ed.) Proceedings of Foundations of Software Technology and Theoretical Computer Science, 15th Conference, Bangalore, India, December 18–20, Lecture Notes in Computer Science 1026, pp. 499–513 (1995). ISBN 3-540-60692-0
Brázdil, T., Forejt, V., Kučera, A.: Controller Synthesis and Verification for Markov Decision Processes with Qualitative Branching Time Objectives. In: Proceedings of the ICALP 2008, Lecture Notes in Computer Science, vol. 5126, pp. 148–159 (2008)
Brázdil, T., Brožek, V., Forejt, V., Kučera, A.: Stochastic games with branching-time winning objectives. In: Proceedings if the LICS 2006, pp. 349–358 (2006)
Brihaye, T., Da Costa Lopes, A., Laroussinie, F., Markey, N.: ATL with strategy contexts and bounded memory. In: International Symposium on Logical Foundations of Computer Science (LFCS), Lecture Notes in Computer Science, vol. 5407, pp. 92–106 (2009)
Bulling N., Jamroga W.: What agents can probably enforce. Fundam. Inform. 93(1–3), 81–96 (2009)
Canny, J.: Some algebraic and geometric computations in PSPACE. In: Proceedings of the STOC’88, pp. 460–467 (1988)
Chatterjee K., Henzinger T.A., Piterman N.: Strategy logic. Inf. Comput. 208(6), 677–693 (2010)
Clarke E.M., Grumberg O., Kurshan R.P.: A synthesis of two approaches for verifying finite state concurrent systems. J. Log. Comput. 2(5), 605–618 (1992)
Clarke E.M., Peled D., Grumberg O.: Model Checking. MIT Press, Cambridge (1999)
Cook, S.A.: The complexity of theorem-proving procedures. In: IEEE Symposium on Foundations of Computer Science (FOCS), pp. 151–158 (1971)
Courcoubetis C., Yannakakis M.: The complexity of probabilistic verification. J. ACM 42(4), 857–907 (1995)
De Alfaro, L.: Formal Verification of Probabilistic Systems. Ph.D.Thesis. Department of Computer Science, Stanford University (1997)
de Alfaro, L., Henzinger, T.A.: Concurrent omega-regular games. In: Proceedings of the LICS, pp. 141–154 (2000)
de Alfaro, L., Henzinger, T.A., Kupferman, O.: Concurrent reachability games. In: IEEE Symposium on Foundations of Computer Science (FOCS), pp. 564–575 (1998)
Grigoriev D.: Complexity of deciding Tarski algebra. J. Symb. Comput. 5(1–2), 65–108 (1988)
Hopcroft J.E., Ullman J.D.: Introduction to Automata Theory, Languages, and Computation. Addison-Wesley, Reading (1979)
Kučera, A., Stražovský, O.: On the controller synthesis for finite-state Markov decision processes. In: Proceedings of the FSTTCS, Lecture Notes in Computer Science, vol. 3821, pp. 541–552 (2005)
Meyer, A.R., Stockmeyer, L.: The equivalence problem for regular expressions with squaring requires exponential space. In: Proceedings of the 13th Annual IEEE Symposium on Switching and Automata Theory, pp. 125–129 (1972)
Papadimitriou C.: Computational Complexity. Addison-Wesley, Reading (1994)
Safra, S.: On the complexity of ω-automata. In: 29th Annual IEEE Symposium on Foundations of Computer Science, pp. 319–327. White Plains, New York (1988)
Tarski A.: A lattice-theoretical fixpoint theorem and its applications. Pac. J. Math. 5(2), 285–309 (1955)
Thomas, W.: Computation tree logic and regular omega-languages. In: Lecture Notes in Computer Science, vol. 354, pp. 690–713 (1988)
Thomas, W.: Automata on infinite objects. In: van Leeuwen, J. (ed.) Handbook of Theoretical Computer Science, chapt. 4, pp. 133–191. Elsevier Science Publishers B.V., Amsterdam (1990)
Vardi, M.Y.: Probabilistic linear-time model checking: an overview of the automata-theoretic approach Lecture Notes in Computer Science, vol. 1601, pp. 265–276 (1999)
Vardi, M.Y., Wolper, P.:Yet another process logic (preliminary version). In: Lecture Notes in Computer Science, vol. 164, pp. 501–512 (1983)
Author information
Authors and Affiliations
Corresponding author
Rights and permissions
About this article
Cite this article
Baier, C., Brázdil, T., Größer, M. et al. Stochastic game logic. Acta Informatica 49, 203–224 (2012). https://doi.org/10.1007/s00236-012-0156-0
Received:
Accepted:
Published:
Issue Date:
DOI: https://doi.org/10.1007/s00236-012-0156-0