Luca de Alfaro ; Rupak Majumdar ; Vishwanath Raman ; Mariëlle Stoelinga - Game Refinement Relations and Metrics

lmcs:781 - Logical Methods in Computer Science, September 11, 2008, Volume 4, Issue 3 - https://doi.org/10.2168/LMCS-4(3:7)2008
Game Refinement Relations and MetricsArticle

Authors: Luca de Alfaro ; Rupak Majumdar ; Vishwanath Raman ; Mariëlle Stoelinga

    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.


    Volume: Volume 4, Issue 3
    Published on: September 11, 2008
    Imported on: January 4, 2008
    Keywords: Computer Science - Logic in Computer Science,F.4.1,F.1.1
    Funding:
      Source : OpenAIRE Graph
    • Quantitative System Properties in Model-Driven Design of Embedded Systems; Funder: European Commission; Code: 214755
    • CAREER: Structured Design of Embedded Software; Funder: National Science Foundation; Code: 0132780
    • ITR - ASE - int: Event Driven Software Quality; Funder: National Science Foundation; Code: 0427202
    • Modeling and Analysis of QoS of Component-Based Designs; Funder: Netherlands Organisation for Scientific Research (NWO); Code: 642.000.505
    • CSR---EHS: Collaborative: Directed Real-Time Testing; Funder: National Science Foundation; Code: 0720884
    • CAREER: Modular Verification of Software; Funder: National Science Foundation; Code: 0546170

    21 Documents citing this article

    Consultation statistics

    This page has been seen 1509 times.
    This article's PDF has been downloaded 488 times.