K. Chatterjee,
L. de Alfaro,
R. Majumdar, V. Raman.
Algorithms for Game Metrics.
In Proceedings of FSTTCS 08: IARCS Annual Conference on Foundations of
Software Technology and Theoretical Computer Science.
Abstract
PDF
An extended version of this paper can be found on
Arxiv.
Abstract
Simulation and bisimulation metrics for stochastic systems provide a
quantitative generalization of the classical simulation and
bisimulation relations.
These metrics capture the similarity of states with respect to
quantitative specifications written in the quantitative mu-calculus
and related probabilistic logics.
We present algorithms for computing the metrics on Markov
decision processes (MDPs), turn-based stochastic games, and concurrent
games.
For turn-based games and MDPs, we provide a polynomial-time algorithm
based on linear programming
for the computation of the one-step metric distance between states.
The algorithm improves on the
previously known exponential-time algorithm based on a reduction to
the theory of
reals.
We then present PSPACE algorithms for both the decision problem and
the
problem of approximating the metric distance between two states,
matching the best known bound for Markov chains.
For the bisimulation kernel of the metric, which corresponds to
probabilistic
bisimulation, our algorithm works in time O(n^4) for both
turn-based games and MDPs; improving the previously best known
O(n^9 log(n)) time algorithm for MDPs.
For a concurrent game G, we show that computing the exact distance
between states is at least as hard as computing the value of
concurrent reachability games and
the square-root-sum problem in computational geometry.
We show that checking whether the metric distance is bounded by a
rational r, can be accomplished via a reduction to the theory of
real closed fields, involving a formula with three quantifier
alternations, yielding O(|G|^O(|G|^5)) time
complexity, improving the previously known reduction with
O(|G|^O(|G|^7)) time complexity.
These algorithms can be iterated to approximate the metrics using
binary search.