Author(s):

Chatterjee, Krishnendu; de Alfaro, Luca; Majumdar, Ritankar S; Raman, Vishwanath

Article Title: 
Algorithms for game metrics

Affiliation 
IST Austria 
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 mucalculus and related probabilistic logics. We first show that the metrics provide a bound for the difference in longrun average and discounted average behavior across states, indicating that the metrics can be used both in system verification, and in performance evaluation. For turnbased games and MDPs, we provide a polynomialtime algorithm for the computation of the onestep metric distance between states. The algorithm is based on linear programming; it improves on the previous 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 algorithms for Markov chains. For the bisimulation kernel of the metric our algorithm works in time O(n(4)) for both turnbased 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 be tween 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 done via a reduction to the theory of real closed fields, involving a formula with three quantifier alternations, yielding O(vertical bar G vertical bar(O(vertical bar G vertical bar 5))) time complexity, improving the previously known reduction, which yielded O(vertical bar G vertical bar(O(vertical bar G vertical bar 7))) time complexity. These algorithms can be iterated to approximate the metrics using binary search

Keywords: 
Metrics; game semantics; minimax theorem; ωregular properties; quantitative μcalculus; probabilistic choice; equivalence of states; refinement of states

Journal Title:

Logical Methods in Computer Science

Volume: 
6

Issue 
3:13

ISSN:

18605974

Publisher:

International Federation of Computational Logic

Date Published:

20100901

Start Page: 
1

End Page:

27

Copyright Statement: 
CCBYND 2.0

Sponsor: 
The first, second and fourth author were supported in part by the National Science Foundation grants CNS0720884 and CCR01 32780. The third author was supported in part by the National Science Foundation grants CCF0427202, CCF0546170.

URL: 

DOI: 
10.2168/LMCS6(3:13)2010

Notes: 
A preliminary version of this paper titled “Algorithms for Game Metrics” appeared in the IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, December 2008. This is a version with full proofs and extensions.

Open access: 
yes (OA journal) 