Abstract
We show that the controller synthesis and verification problems for Markov decision processes with qualitative PECTL* objectives are 2-EXPTIME complete. More precisely, the algorithms are polynomial in the size of a given Markov decision process and doubly exponential in the size of a given qualitative PECTL* formula. Moreover, we show that if a given qualitative PECTL* objective is achievable by some strategy, then it is also achievable by an effectively constructible one-counter strategy, where the associated complexity bounds are essentially the same as above. For the fragment of qualitative PCTL objectives, we obtain EXPTIME completeness and the algorithms are only singly exponential in the size of the formula.
Supported by the research center Institute for Theoretical Computer Science (ITI), project No. 1M0545.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Baier, C., Größer, M., Leucker, M., Bollig, B., Ciesinski, F.: Controller synthesis for probabilistic systems. In: Proceedings of IFIP TCS 2004, pp. 493–506. Kluwer, Dordrecht (2004)
Brázdil, T., Brožek, V., Forejt, V.: Branching-time model-checking of probabilistic pushdown automata. In: Proceedings of INFINITY 2007, pp. 24–33 (2007)
Brázdil, T., Brožek, V., Forejt, V., Kučera, A.: Stochastic games with branching-time winning objectives. In: Proceedings of LICS 2006, pp. 349–358. IEEE, Los Alamitos (2006)
Brázdil, T., Forejt, V.: Strategy synthesis for Markov decision processes and branching-time logics. In: Caires, L., Vasconcelos, V.T. (eds.) CONCUR. LNCS, vol. 4703, pp. 428–444. Springer, Heidelberg (2007)
Brázdil, T., Forejt, V., Kučera, A.: Controller synthesis and verification for Markov decision processes with qualitative branching time objectives. Technical report FIMU-RS-2008-05, Faculty of Informatics, Masaryk University (2008)
Chatterjee, K., de Alfaro, L., Henzinger, T.: Trading memory for randomness. In: Proceedings of 2nd Int. Conf. on Quantitative Evaluation of Systems (QEST 2004), pp. 206–217. IEEE, Los Alamitos (2004)
Chatterjee, K., Majumdar, R., Henzinger, T.: Markov decision processes with multiple objectives. In: Durand, B., Thomas, W. (eds.) STACS 2006. LNCS, vol. 3884, pp. 325–336. Springer, Heidelberg (2006)
de Alfaro, L.: Quantitative verification and control via the mu-calculus. In: Amadio, R.M., Lugiez, D. (eds.) CONCUR 2003. LNCS, vol. 2761, pp. 102–126. Springer, Heidelberg (2003)
Emerson, E.A.: Temporal and modal logic. Handbook of TCS B, 995–1072 (1991)
Etessami, K., Kwiatkowska, M., Vardi, M., Yannakakis, M.: Multi-objective model checking of Markov decision processes. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol. 4424, pp. 50–65. Springer, Heidelberg (2007)
Filar, J., Vrieze, K.: Competitive Markov Decision Processes. Springer, Heidelberg (1996)
Grädel, E.: Positional determinacy of infinite games. In: Diekert, V., Habib, M. (eds.) STACS 2004. LNCS, vol. 2996, pp. 4–18. Springer, Heidelberg (2004)
Hansson, H., Jonsson, B.: A logic for reasoning about time and reliability. Formal Aspects of Computing 6, 512–535 (1994)
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 FST&TCS 2005. LNCS, vol. 3821, pp. 541–552. Springer, Heidelberg (2005)
Puterman, M.L.: Markov Decision Processes. Wiley, Chichester (1994)
Stirling, C.: Modal and temporal logics. Handbook of Logic in Comp. Sci. 2, 477–563 (1992)
Vardi, M.: Automatic verification of probabilistic concurrent finite-state programs. In: Proceedings of FOCS 1985, pp. 327–338. IEEE, Los Alamitos (1985)
Walukiewicz, I.: A landscape with games in the background. In: Proceedings of LICS 2004, pp. 356–366. IEEE, Los Alamitos (2004)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2008 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Brázdil, T., Forejt, V., Kučera, A. (2008). Controller Synthesis and Verification for Markov Decision Processes with Qualitative Branching Time Objectives. In: Aceto, L., Damgård, I., Goldberg, L.A., Halldórsson, M.M., Ingólfsdóttir, A., Walukiewicz, I. (eds) Automata, Languages and Programming. ICALP 2008. Lecture Notes in Computer Science, vol 5126. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-70583-3_13
Download citation
DOI: https://doi.org/10.1007/978-3-540-70583-3_13
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-70582-6
Online ISBN: 978-3-540-70583-3
eBook Packages: Computer ScienceComputer Science (R0)