Abstract
We consider synchronizing properties of Markov decision processes (MDP), viewed as generators of sequences of probability distributions over states. A probability distribution is p-synchronizing if the probability mass is at least p in some state, and a sequence of probability distributions is weakly p-synchronizing, or strongly p-synchronizing if respectively infinitely many, or all but finitely many distributions in the sequence are p-synchronizing.
For each synchronizing mode, an MDP can be (i) sure winning if there is a strategy that produces a 1-synchronizing sequence; (ii) almost-sure winning if there is a strategy that produces a sequence that is, for all ε > 0, a (1-ε)-synchronizing sequence; (iii) limit-sure winning if for all ε > 0, there is a strategy that produces a (1-ε)-synchronizing sequence.
For each synchronizing and winning mode, we consider the problem of deciding whether an MDP is winning, and we establish matching upper and lower complexity bounds of the problems, as well as the optimal memory requirement for winning strategies: (a) for all winning modes, we show that the problems are PSPACE-complete for weak synchronization, and PTIME-complete for strong synchronization; (b) we show that for weak synchronization, exponential memory is sufficient and may be necessary for sure winning, and infinite memory is necessary for almost-sure winning; for strong synchronization, linear-size memory is sufficient and may be necessary in all modes; (c) we show a robustness result that the almost-sure and limit-sure winning modes coincide for both weak and strong synchronization.
This work was partially supported by the Belgian Fonds National de la Recherche Scientifique (FNRS), and by the PICS project Quaverif funded by the French Centre National de la Recherche Scientifique (CNRS).
Fuller version: [1].
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
ArXiv CoRR (2014), http://arxiv.org/abs/1402.2840 (Full version)
Agrawal, M., Akshay, S., Genest, B., Thiagarajan, P.S.: Approximate verification of the symbolic dynamics of Markov chains. In: LICS, pp. 55–64. IEEE (2012)
de Alfaro, L., Henzinger, T.A.: Concurrent omega-regular games. In: Proc. of LICS, pp. 141–154 (2000)
de Alfaro, L., Henzinger, T.A., Kupferman, O.: Concurrent reachability games. Theor. Comput. Sci. 386(3), 188–217 (2007)
Baier, C., Bertrand, N., Größer, M.: On decision problems for probabilistic Büchi automata. In: Amadio, R.M. (ed.) FOSSACS 2008. LNCS, vol. 4962, pp. 287–301. Springer, Heidelberg (2008)
Baldoni, R., Bonnet, F., Milani, A., Raynal, M.: On the solvability of anonymous partial grids exploration by mobile robots. In: Baker, T.P., Bui, A., Tixeuil, S. (eds.) OPODIS 2008. LNCS, vol. 5401, pp. 428–445. Springer, Heidelberg (2008)
Burkhard, H.D.: Zum längenproblem homogener experimente an determinierten und nicht-deterministischen automaten. Elektronische Informationsverarbeitung und Kybernetik 12(6), 301–306 (1976)
Cerný, J.: Poznámka k. homogénnym experimentom s konecnymi automatmi. Matematicko-fyzikálny Časopis 14(3), 208–216 (1964)
Chadha, R., Korthikanti, V.A., Viswanathan, M., Agha, G., Kwon, Y.: Model checking MDPs with a unique compact invariant set of distributions. In: QEST, pp. 121–130. IEEE (2011)
Courcoubetis, C., Yannakakis, M.: The complexity of probabilistic verification. J. ACM 42(4), 857–907 (1995)
Doyen, L., Massart, T., Shirmohammadi, M.: Infinite synchronizing words for probabilistic automata. In: Murlak, F., Sankowski, P. (eds.) MFCS 2011. LNCS, vol. 6907, pp. 278–289. Springer, Heidelberg (2011)
Doyen, L., Massart, T., Shirmohammadi, M.: Synchronizing objectives for Markov decision processes. In: Proc. of iWIGP. EPTCS, vol. 50, pp. 61–75 (2011)
Doyen, L., Massart, T., Shirmohammadi, M.: Infinite synchronizing words for probabilistic automata (Erratum). CoRR abs/1206.0995 (2012)
Doyen, L., Massart, T., Shirmohammadi, M.: Limit synchronization in Markov decision processes. In: Muscholl, A. (ed.) FOSSACS 2014. LNCS, vol. 8412, pp. 58–72. Springer, Heidelberg (2014)
Filar, J., Vrieze, K.: Competitive Markov Decision Processes. Springer (1997)
Gimbert, H., Oualhadj, Y.: Probabilistic automata on finite words: Decidable and undecidable problems. In: Abramsky, S., Gavoille, C., Kirchner, C., Meyer auf der Heide, F., Spirakis, P.G. (eds.) ICALP 2010, Part II. LNCS, vol. 6199, pp. 527–538. Springer, Heidelberg (2010)
Henzinger, T.A., Mateescu, M., Wolf, V.: Sliding window abstraction for infinite Markov chains. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 337–352. Springer, Heidelberg (2009)
Imreh, B., Steinby, M.: Directable nondeterministic automata. Acta Cybern. 14(1), 105–115 (1999)
Kfoury, D.: Synchronizing sequences for probabilistic automata. Studies in Applied Mathematics 29, 101–103 (1970)
Korthikanti, V.A., Viswanathan, M., Agha, G., Kwon, Y.: Reasoning about MDPs as transformers of probability distributions. In: QEST, pp. 199–208. IEEE (2010)
Martyugin, P.: Computational complexity of certain problems related to carefully synchronizing words for partial automata and directing words for nondeterministic automata. Theory Comput. Syst. 54(2), 293–304 (2014)
Vardi, M.Y.: Automatic verification of probabilistic concurrent finite-state programs. In: Proc. of FOCS, pp. 327–338. IEEE Computer Society (1985)
Volkov, M.V.: Synchronizing automata and the Cerny conjecture. In: Martín-Vide, C., Otto, F., Fernau, H. (eds.) LATA 2008. LNCS, vol. 5196, pp. 11–27. Springer, Heidelberg (2008)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2014 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Doyen, L., Massart, T., Shirmohammadi, M. (2014). Robust Synchronization in Markov Decision Processes. In: Baldan, P., Gorla, D. (eds) CONCUR 2014 – Concurrency Theory. CONCUR 2014. Lecture Notes in Computer Science, vol 8704. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-662-44584-6_17
Download citation
DOI: https://doi.org/10.1007/978-3-662-44584-6_17
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-662-44583-9
Online ISBN: 978-3-662-44584-6
eBook Packages: Computer ScienceComputer Science (R0)