Seminar 11 May 10:00, 2012
Computing Game Metrics on Markov Decision Processes
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.
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.
