The following technical report is available from http://aib.informatik.rwth-aachen.de:
Computing Game Metrics on Markov Decision Processes Hongfei Fu AIB 2012-08
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 \mu-calculus defined by de Alfaro and Majumdar, which can express reachability and \omega-regular specifications. And by Chatterjee et al. that the discounted version of the metric is characterized by the discounted quantitative game \mu-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 and coNP, which improves the previous PSPACE upperbound by Chatterjee et al.