Abstract
This paper focuses on the so called controller synthesis problem, which addresses the question of how to limit the internal behavior of a given system implementation to meet its specification, regardless of the behavior enforced by the environment. We consider this problem in the probabilistic setting, where the underlying model has both probabilism and nondeterminism and the nondeterministic choices in some states are assumed to be controllable while the others are under the control of an unpredictable environment. As for the specification, it is defined by probabilistic computation tree logic. We show that under the restriction that the controller exploits only Markovian randomized strategy, the existence of such a controller is decidable, which is done by a reduction to the decidability of first-order theory for reals. This also gives rise to an algorithm which can synthesize the controller if it does exist.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Baier, C., Größer, M., Leucker, M., Bollig, B., Ciesinski, F.: Controller synthesis for probabilistic systems. In: Proceeding of IFIP TCS 2004, Kluwer, Dordrecht (2004)
Bianco, A., de Alfaro, L.: Model checking of probabilistic and nondeterministic systems. In: Thiagarajan, P.S. (ed.) FSTTCS 1995. LNCS, vol. 1026, pp. 499–513. Springer, Heidelberg (1995)
Basu, S., Pollack, R., Roy, M.: On the combinatorial and algebraic complexity of quantifier elimination. Journal of ACM 43(6), 1002–1045 (1996)
Chatterjee, K., Jurdzinski, M., Henzinger, T.: Simple stochastic parity games. In: Baaz, M., Makowsky, J.A. (eds.) CSL 2003. LNCS, vol. 2803, pp. 100–113. Springer, Heidelberg (2003)
Chatterjee, K., Jurdzinski, M., Henzinger, T.: Quantitative simple stochastic partity games. In: Proceeding of SODA 2004, SIAM, Philadelphia (2004)
Courcoubetis, C., Yannakakis, M.: The compleixity of probabilistic verification. Journal of ACM 42(4), 857–907 (1995)
Filar, J., Vrieze, K.: Competitive Markov Decision Processes. Springer, Heidelberg (1997)
Grigoriev, D.: Complexity of deciding Tarski algebra. Journal of Symbolic Computation 5(1-2), 65–108 (1988)
Hansson, H., Jonsson, B.: A Logic for reasoning about time and reliability. Formal Aspects of Computing 6(5), 512–535 (1994)
Kupferman, O., Vardi, M., Wolper, P.: Module checking. Information and Computation 164(2), 322–344 (2001)
Owen, G.: Game Theory. Academic Press, London (1995)
Puterman, M.: Markov Decision Processes. Wiley, Chichester (1994)
Traski, A.: A Decision Method for Elementary Algebra and Geometry. Univ. of California Press, Berkeley (1951)
Thomas, W.: Infinite games and verification. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 58–64. Springer, Heidelberg (2003)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2006 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Chen, T., Han, T., Lu, J. (2006). On the Markovian Randomized Strategy of Controller for Markov Decision Processes. In: Wang, L., Jiao, L., Shi, G., Li, X., Liu, J. (eds) Fuzzy Systems and Knowledge Discovery. FSKD 2006. Lecture Notes in Computer Science(), vol 4223. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11881599_17
Download citation
DOI: https://doi.org/10.1007/11881599_17
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-45916-3
Online ISBN: 978-3-540-45917-0
eBook Packages: Computer ScienceComputer Science (R0)