---
res:
bibo_abstract:
- "Simulation and bisimulation metrics for stochastic systems provide a quantitative
gen- eralization of the classical simulation and bisimulation relations. These
metrics capture the similarity of states with respect to quantitative specifications
written in the quantitative μ-calculus and related probabilistic logics.\r\nWe
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 algo- rithm 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(n4)
for both turn-based games and MDPs; improving the previously best known O(n9 ·
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\r\nformula 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\r\nto approximate the metrics using binary search.@eng"
bibo_authorlist:
- foaf_Person:
foaf_givenName: Krishnendu
foaf_name: Chatterjee, Krishnendu
foaf_surname: Chatterjee
foaf_workInfoHomepage: http://www.librecat.org/personId=2E5DCA20-F248-11E8-B48F-1D18A9856A87
orcid: 0000-0002-4561-241X
- foaf_Person:
foaf_givenName: Luca
foaf_name: De Alfaro, Luca
foaf_surname: De Alfaro
- foaf_Person:
foaf_givenName: Ritankar
foaf_name: Majumdar, Ritankar
foaf_surname: Majumdar
- foaf_Person:
foaf_givenName: Vishwanath
foaf_name: Raman, Vishwanath
foaf_surname: Raman
bibo_doi: 10.4230/LIPIcs.FSTTCS.2008.1745
bibo_volume: 2
dct_date: 2008^xs_gYear
dct_language: eng
dct_publisher: Schloss Dagstuhl - Leibniz-Zentrum für Informatik@
dct_title: Algorithms for game metrics@
...