Game Refinement Relations and Metrics

Luca de Alfaro, D.S. Scott (Editor), B.J. Pierce (Editor), Rupak Majumdar, G.J. Plotkin (Editor), Viswanath Raman, M.Y. Vardi (Editor), Mariëlle Ida Antoinette Stoelinga, J. Adámek (Editor)

Research output: Contribution to journalArticleAcademicpeer-review

23 Citations (Scopus)

Abstract

We consider two-player games played over finite state spaces for an infinite number of rounds. At each state, the players simultaneously choose moves; the moves determine a successor state. It is often advantageous for players to choose probability distributions over moves, rather than single moves. Given a goal, for example, reach a target state, the question of winning is thus a probabilistic one: what is the maximal probability of winning from a given state? On these game structures, two fundamental notions are those of equivalences and metrics. Given a set of winning conditions, two states are equivalent if the players can win the same games with the same probability from both states. Metrics provide a bound on the difference in the probabilities of winning across states, capturing a quantitative notion of state similarity. We introduce equivalences and metrics for two-player game structures, and we show that they characterize the difference in probability of winning games whose goals are expressed in the quantitative mu-calculus. The quantitative mu-calculus can express a large set of goals, including reachability, safety, and omega-regular properties. Thus, we claim that our relations and metrics provide the canonical extensions to games, of the classical notion of bisimulation for transition systems. We develop our results both for equivalences and metrics, which generalize bisimulation, and for asymmetrical versions, which generalize simulation.
Original language Undefined 7 7 27 Logical methods in computer science 4 3 https://doi.org/10.2168/LMCS-4(3:7)2008 Published - Sep 2008

Keywords

• distance
• EC Grant Agreement nr.: FP7-ICT-2007-1
• EC Grant Agreement nr.: FP7/214755
• EC Grant Agreement nr.: IST-004527
• EWI-15212
• Bisimulation
• Games
• METIS-264393
• IR-62780

Cite this

de Alfaro, L., Scott, D. S. (Ed.), Pierce, B. J. (Ed.), Majumdar, R., Plotkin, G. J. (Ed.), Raman, V., ... Adámek, J. (Ed.) (2008). Game Refinement Relations and Metrics. Logical methods in computer science, 4(3), 7. . https://doi.org/10.2168/LMCS-4(3:7)2008
de Alfaro, Luca ; Scott, D.S. (Editor) ; Pierce, B.J. (Editor) ; Majumdar, Rupak ; Plotkin, G.J. (Editor) ; Raman, Viswanath ; Vardi, M.Y. (Editor) ; Stoelinga, Mariëlle Ida Antoinette ; Adámek, J. (Editor). / Game Refinement Relations and Metrics. In: Logical methods in computer science. 2008 ; Vol. 4, No. 3. pp. 7.
@article{dbc29cdaeb5643da916e345418b021ba,
title = "Game Refinement Relations and Metrics",
abstract = "We consider two-player games played over finite state spaces for an infinite number of rounds. At each state, the players simultaneously choose moves; the moves determine a successor state. It is often advantageous for players to choose probability distributions over moves, rather than single moves. Given a goal, for example, reach a target state, the question of winning is thus a probabilistic one: what is the maximal probability of winning from a given state? On these game structures, two fundamental notions are those of equivalences and metrics. Given a set of winning conditions, two states are equivalent if the players can win the same games with the same probability from both states. Metrics provide a bound on the difference in the probabilities of winning across states, capturing a quantitative notion of state similarity. We introduce equivalences and metrics for two-player game structures, and we show that they characterize the difference in probability of winning games whose goals are expressed in the quantitative mu-calculus. The quantitative mu-calculus can express a large set of goals, including reachability, safety, and omega-regular properties. Thus, we claim that our relations and metrics provide the canonical extensions to games, of the classical notion of bisimulation for transition systems. We develop our results both for equivalences and metrics, which generalize bisimulation, and for asymmetrical versions, which generalize simulation.",
keywords = "distance, EC Grant Agreement nr.: FP7-ICT-2007-1, EC Grant Agreement nr.: FP7/214755, EC Grant Agreement nr.: IST-004527, EWI-15212, Bisimulation, Games, METIS-264393, IR-62780",
author = "{de Alfaro}, Luca and D.S. Scott and B.J. Pierce and Rupak Majumdar and G.J. Plotkin and Viswanath Raman and M.Y. Vardi and Stoelinga, {Mari{\"e}lle Ida Antoinette} and J. Ad{\'a}mek",
note = "eemcs-eprint-15212",
year = "2008",
month = "9",
doi = "10.2168/LMCS-4(3:7)2008",
language = "Undefined",
volume = "4",
pages = "7",
journal = "Logical methods in computer science",
issn = "1860-5974",
publisher = "Technischen Universitat Braunschweig",
number = "3",

}

de Alfaro, L, Scott, DS (ed.), Pierce, BJ (ed.), Majumdar, R, Plotkin, GJ (ed.), Raman, V, Vardi, MY (ed.), Stoelinga, MIA & Adámek, J (ed.) 2008, 'Game Refinement Relations and Metrics' Logical methods in computer science, vol. 4, no. 3, 7, pp. 7. https://doi.org/10.2168/LMCS-4(3:7)2008

Game Refinement Relations and Metrics. / de Alfaro, Luca; Scott, D.S. (Editor); Pierce, B.J. (Editor); Majumdar, Rupak; Plotkin, G.J. (Editor); Raman, Viswanath; Vardi, M.Y. (Editor); Stoelinga, Mariëlle Ida Antoinette; Adámek, J. (Editor).

In: Logical methods in computer science, Vol. 4, No. 3, 7, 09.2008, p. 7.

Research output: Contribution to journalArticleAcademicpeer-review

TY - JOUR

T1 - Game Refinement Relations and Metrics

AU - de Alfaro, Luca

AU - Majumdar, Rupak

AU - Raman, Viswanath

AU - Stoelinga, Mariëlle Ida Antoinette

A2 - Scott, D.S.

A2 - Pierce, B.J.

A2 - Plotkin, G.J.

A2 - Vardi, M.Y.

A2 - Adámek, J.

N1 - eemcs-eprint-15212

PY - 2008/9

Y1 - 2008/9

N2 - We consider two-player games played over finite state spaces for an infinite number of rounds. At each state, the players simultaneously choose moves; the moves determine a successor state. It is often advantageous for players to choose probability distributions over moves, rather than single moves. Given a goal, for example, reach a target state, the question of winning is thus a probabilistic one: what is the maximal probability of winning from a given state? On these game structures, two fundamental notions are those of equivalences and metrics. Given a set of winning conditions, two states are equivalent if the players can win the same games with the same probability from both states. Metrics provide a bound on the difference in the probabilities of winning across states, capturing a quantitative notion of state similarity. We introduce equivalences and metrics for two-player game structures, and we show that they characterize the difference in probability of winning games whose goals are expressed in the quantitative mu-calculus. The quantitative mu-calculus can express a large set of goals, including reachability, safety, and omega-regular properties. Thus, we claim that our relations and metrics provide the canonical extensions to games, of the classical notion of bisimulation for transition systems. We develop our results both for equivalences and metrics, which generalize bisimulation, and for asymmetrical versions, which generalize simulation.

AB - We consider two-player games played over finite state spaces for an infinite number of rounds. At each state, the players simultaneously choose moves; the moves determine a successor state. It is often advantageous for players to choose probability distributions over moves, rather than single moves. Given a goal, for example, reach a target state, the question of winning is thus a probabilistic one: what is the maximal probability of winning from a given state? On these game structures, two fundamental notions are those of equivalences and metrics. Given a set of winning conditions, two states are equivalent if the players can win the same games with the same probability from both states. Metrics provide a bound on the difference in the probabilities of winning across states, capturing a quantitative notion of state similarity. We introduce equivalences and metrics for two-player game structures, and we show that they characterize the difference in probability of winning games whose goals are expressed in the quantitative mu-calculus. The quantitative mu-calculus can express a large set of goals, including reachability, safety, and omega-regular properties. Thus, we claim that our relations and metrics provide the canonical extensions to games, of the classical notion of bisimulation for transition systems. We develop our results both for equivalences and metrics, which generalize bisimulation, and for asymmetrical versions, which generalize simulation.

KW - distance

KW - EC Grant Agreement nr.: FP7-ICT-2007-1

KW - EC Grant Agreement nr.: FP7/214755

KW - EC Grant Agreement nr.: IST-004527

KW - EWI-15212

KW - Bisimulation

KW - Games

KW - METIS-264393

KW - IR-62780

U2 - 10.2168/LMCS-4(3:7)2008

DO - 10.2168/LMCS-4(3:7)2008

M3 - Article

VL - 4

SP - 7

JO - Logical methods in computer science

JF - Logical methods in computer science

SN - 1860-5974

IS - 3

M1 - 7

ER -

de Alfaro L, Scott DS, (ed.), Pierce BJ, (ed.), Majumdar R, Plotkin GJ, (ed.), Raman V et al. Game Refinement Relations and Metrics. Logical methods in computer science. 2008 Sep;4(3):7. 7. https://doi.org/10.2168/LMCS-4(3:7)2008