Abstract
In this paper we study the complexity of computing the game bisimulation metric defined by de Alfaro et al. on Markov Decision Processes. It is proved by de Alfaro et al. that the undiscounted version of the metric is characterized by a quantitative game μ-calculus defined by de Alfaro and Majumdar, which can express reachability and ω-regular specifications. And by Chatterjee et al. that the discounted version of the metric is characterized by the discounted quantitative game μ-calculus. In the discounted case, we show that the metric can be computed exactly by extending the method for Labelled Markov Chains by Chen et al. And in the undiscounted case, we prove that the problem whether the metric between two states is under a given threshold can be decided in NP ∩ coNP, which improves the previous PSPACE upperbound by Chatterjee et al.
Full version available at [13].
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.
Similar content being viewed by others
References
de Alfaro, L., Henzinger, T.A., Majumdar, R.: Discounting the Future in Systems Theory. In: Baeten, J.C.M., Lenstra, J.K., Parrow, J., Woeginger, G.J. (eds.) ICALP 2003. LNCS, vol. 2719, pp. 1022–1037. Springer, Heidelberg (2003)
de Alfaro, L., Majumdar, R.: Quantitative solution of omega-regular games. J. Comput. Syst. Sci. 68(2), 374–397 (2004)
de Alfaro, L., Majumdar, R., Raman, V., Stoelinga, M.: Game relations and metrics. In: LICS, pp. 99–108. IEEE Computer Society (2007)
Aziz, A., Singhal, V., Balarin, F.: It Usually Works: The Temporal Logic of Stochastic Systems. In: Wolper, P. (ed.) CAV 1995. LNCS, vol. 939, pp. 155–165. Springer, Heidelberg (1995)
Baier, C., Engelen, B., Majster-Cederbaum, M.E.: Deciding bisimilarity and similarity for probabilistic processes. J. Comput. Syst. Sci. 60(1), 187–231 (2000)
van Breugel, F., Sharma, B., Worrell, J.: Approximating a behavioural pseudometric without discount for probabilistic systems. Logical Methods in Computer Science 4(2) (2008)
Cattani, S., Segala, R.: Decision Algorithms for Probabilistic Bisimulation. In: Brim, L., Jančar, P., Křetínský, M., Kučera, A. (eds.) CONCUR 2002. LNCS, vol. 2421, pp. 371–385. Springer, Heidelberg (2002)
Chatterjee, K., de Alfaro, L., Majumdar, R., Raman, V.: Algorithms for game metrics (full version). Logical Methods in Computer Science 6(3) (2010)
Chen, D., van Breugel, F., Worrell, J.: On the Complexity of Computing Probabilistic Bisimilarity. In: Birkedal, L. (ed.) FOSSACS 2012. LNCS, vol. 7213, pp. 437–451. Springer, Heidelberg (2012)
Desharnais, J., Laviolette, F., Tracol, M.: Approximate analysis of probabilistic processes: Logic, simulation and games. In: QEST, pp. 264–273. IEEE Computer Society (2008)
Etessami, K., Yannakakis, M.: On the complexity of Nash equilibria and other fixed points. SIAM J. Comput. 39(6), 2531–2597 (2010)
Ferns, N., Panangaden, P., Precup, D.: Metrics for finite Markov decision processes. In: McGuinness, D.L., Ferguson, G. (eds.) AAAI, pp. 950–951. AAAI Press/The MIT Press (2004)
Fu, H.: Computing game metrics on Markov decision processes. Tech. Rep. AIB-2012-08, RWTH Aachen (May 2012), http://aib.informatik.rwth-aachen.de/
Giacalone, A., Jou, C.C., Smolka, S.A.: Algebraic reasoning for probabilistic concurrent systems. In: Proc. IFIP TC2 Working Conference on Programming Concepts and Methods, pp. 443–458. North-Holland (1990)
Gupta, V., Jagadeesan, R., Panangaden, P.: Approximate reasoning for real-time probabilistic processes. In: QEST, pp. 304–313. IEEE Computer Society (2004)
Jonsson, B., Larsen, K.G.: Specification and refinement of probabilistic processes. In: LICS, pp. 266–277. IEEE Computer Society (1991)
Julius, A.A., Girard, A., Pappas, G.J.: Approximate bisimulation for a class of stochastic hybrid systems. In: American Control Conference, pp. 4724–4729. IEEE, Portland (2006)
Larsen, K.G., Skou, A.: Bisimulation through probabilistic testing. Inf. Comput. 94(1), 1–28 (1991)
Milner, R.: Communication and concurrency. Prentice-Hall, Inc., Upper Saddle River (1989)
Panangaden, P.: Labelled Markov Processes. Imperial College Press (2009)
Schrijver, A.: Theory of Linear and Integer Programming. John Wiley & Sons, Inc., New York (1986)
Segala, R., Lynch, N.A.: Probabilistic simulations for probabilistic processes. Nord. J. Comput. 2(2), 250–273 (1995)
Tracol, M., Desharnais, J., Zhioua, A.: Computing distances between probabilistic automata. In: Massink, M., Norman, G. (eds.) QAPL. EPTCS, vol. 57, pp. 148–162 (2011)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2012 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Fu, H. (2012). Computing Game Metrics on Markov Decision Processes. In: Czumaj, A., Mehlhorn, K., Pitts, A., Wattenhofer, R. (eds) Automata, Languages, and Programming. ICALP 2012. Lecture Notes in Computer Science, vol 7392. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-31585-5_23
Download citation
DOI: https://doi.org/10.1007/978-3-642-31585-5_23
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-31584-8
Online ISBN: 978-3-642-31585-5
eBook Packages: Computer ScienceComputer Science (R0)