On the Controller Synthesis for Finite-State Markov Decision Processes

• Autorzy: Kučera A. , Strazovský O.
• Języki publikacji: EN

Abstrakty

EN

We study the problem of effective controller synthesis for finite-state Markov decision processes (MDPs) and the class of properties definable in the logic PCTL extended with long-run average propositions. We show that the existence of such a controller is decidable, and we give an algorithm which computes the controller if it exists. We also address the issue of "controller robustness", i.e., the problem whether there is a controller which still guarantees the satisfaction of a given property when the probabilities in the considered MDP slightly deviate from their original values. From a practical point of view, this is an important aspect since the probabilities are often determined empirically and hence they are inherently imprecise. We show that the existence of robust controllers is also decidable, and that such controllers are effectively computable if they exist.

Słowa kluczowe

EN

controller synthesis; Markov decision processes; PCTL

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2008
• Tom: Vol. 82, nr 1-2
• Strony: 141--153
• Opis fizyczny: bibliogr. 18 poz.

Twórcy

autor

Kučera A.

autor

Strazovský O.

• Faculty of Informatics, Masaryk University, Botanicka 68a, 60200 Brno, Czech Republic,

Bibliografia

• [1] C. Baier, T. Brázdil, M. Größer, and A. Kučera. Stochastic game logic. In Proceedings of 4th Int. Conf. On Quantitative Evaluation of Systems (QEST'07). IEEE Computer Society Press, 2007.
• [2] C. Baier, M. Größer, M. Leucker, B. Bollig, and F. Ciesinski. Controller synthesis for probabilistic systems. In Proceedings of IFIP TCS'2004, pages 493-506. Kluwer, 2004.
• [3] P. Bouyer, D. D'Souza, P.Madhusudan, and A. Petit. Timed controlwith partial observability. In Proceedings of CAV 2003, volume 2725 of Lecture Notes in Computer Science, pages 180-192. Springer, 2003.
• [4] T. Brázdil, V. Brožek, V. Forejt, and A. Kuˇcera. Stochastic games with branching-time winning objectives. In Proceedings of LICS 2006, pages 349-358. IEEE Computer Society Press, 2006.
• [5] K. Chatterjee and T. Henzinger. Semiperfect-information games. In Proceedings of FST&TCS 2005, volume 3821 of Lecture Notes in Computer Science, pages 1-18. Springer, 2005.
• [6] C. Courcoubetis and M. Yannakakis. The complexity of probabilistic verification. Journal of the Association for Computing Machinery, 42(4):857-907, 1995.
• [7] L. de Alfaro. How to specify and verify the long-run average behavior of probabilistic systems. In Proceedings of LICS'98, pages 454-465. IEEE Computer Society Press, 1998.
• [8] L. de Alfaro, M. Faella, T. Henzinger, R. Majumdar, and M. Stoelinga. The element of surprise in timed games. In Proceedings of CONCUR 2003, volume 2761 of Lecture Notes in Computer Science, pages 144-158. Springer, 2003.
• [9] D. Grigoriev. Complexity of deciding Tarski algebra. Journal of Symbolic Computation, 5(1-2):65-108, 1988.
• [10] H. Hansson and B. Jonsson. A logic for reasoning about time and reliability. Formal Aspects of Computing, 6:512-535, 1994.
• [11] A. Kučera and O. Stražovsk´y. On the controller synthesis for finite-state Markov decision processes. In Proceedings of FST&TCS 2005, volume 3821 of Lecture Notes in Computer Science, pages 541-552. Springer, 2005.
• [12] K. Larsen and A. Skou. Bisimulation through probabilistic testing. Information and Computation, 94(1):1-28, 1991.
• [13] A. Nilim and L. El Ghaoui. Robustness in Markov decision problems with uncertain transition matrices. In Proceedings of NIPS 2003.MIT Press, 2003.
• [14] M.L. Puterman. Markov Decision Processes. Wiley, 1994.
• [15] R. Segala and N.A. Lynch. Probabilistic simulations for probabilistic processes. Nordic Journal of Computing, 2(2):250-273, 1995.
• [16] A. Tarski. A Decision Method for Elementary Algebra and Geometry. Univ. of California Press, Berkeley, 1951.
• [17] W. Thomas. Infinite games and verification. In Proceedings of CAV 2003, volume 2725 of Lecture Notes in Computer Science, pages 58-64. Springer, 2003.
• [18] U. Zwick andM. Paterson. The complexity of mean payoff games on graphs. Theoretical Computer Science, 158(1-2):343-359, 1996.