Chatterjee, Krishnendu ;
de Alfaro, Luca ;
Majumdar, Rupak ;
Raman, Vishwanath
Algorithms for Game Metrics
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), turnbased stochastic games, and concurrent
games.
For turnbased games and MDPs, we provide a polynomialtime algorithm
based on linear programming
for the computation of the onestep metric distance between states.
The algorithm improves on the
previously known exponentialtime 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 $\calo(n^4)$ for both
turnbased games and MDPs; improving the previously best known
$\calo(n^9\cdot\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 squarerootsum 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 $\calo(G^{\calo(G^5)})$ time
complexity, improving the previously known reduction with
$\calo(G^{\calo(G^7)})$ time complexity.
These algorithms can be iterated to approximate the metrics using
binary search.
BibTeX  Entry
@InProceedings{chatterjee_et_al:LIPIcs:2008:1745,
author = {Krishnendu Chatterjee and Luca de Alfaro and Rupak Majumdar and Vishwanath Raman},
title = {{Algorithms for Game Metrics}},
booktitle = {IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science},
pages = {107118},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {9783939897088},
ISSN = {18688969},
year = {2008},
volume = {2},
editor = {Ramesh Hariharan and Madhavan Mukund and V Vinay},
publisher = {Schloss DagstuhlLeibnizZentrum fuer Informatik},
address = {Dagstuhl, Germany},
URL = {http://drops.dagstuhl.de/opus/volltexte/2008/1745},
URN = {urn:nbn:de:0030drops17455},
doi = {10.4230/LIPIcs.FSTTCS.2008.1745},
annote = {Keywords: Algorithms, Metrics, Kernel, Simulation, Bisimulation, Linear Programming, Theory of Reals}
}
05.12.2008
Keywords: 

Algorithms, Metrics, Kernel, Simulation, Bisimulation, Linear Programming, Theory of Reals 
Seminar: 

IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science

Issue date: 

2008 
Date of publication: 

05.12.2008 