Simulation Games Michael Maurer



Yüklə 454 b.
tarix06.03.2018
ölçüsü454 b.
#44847


Simulation Games

  • Michael Maurer


Overview

  • Motivation

  • 4 Different (Bi)simulation relations and their rules to determine the winner

  • Problem with delayed simulation

  • Parity Games

  • Construction of (Bi)simulations as Parity Games



Motivation

  • Capability of mimicking the behavior of another automaton (structural similarities, language containment)

  • Efficiently reducing the size of finite-state automata (known as quotienting)



Simulation Games

  • 4 different Simulation Game Definitions for a given Büchi automaton A :

  • 1) ordinary simulation game,

  • 2) direct (strong) simulation game,

  • 3) delayed simulation game,

  • 4) fair simulation game,



Simulation Games

  • Played by 2 players: Spoiler and Duplicator

  • At the start: two pebbles (Red and Blue) are placed on two vertices q0 and q’0

  • Spoiler chooses a transition

  • and moves Red to qi+1

  • Duplicator also chooses a transition

  • and moves Blue to q‘i+1

  • If Duplicator can‘t move, the game halts and Spoiler wins



Who will be the winner?

  • Either the game halts, in which case Spoiler wins

  • Or the game produces two infinite runs:

  • and

  • For each of the 4 simulation games there exist different rules to determine the winner



Rules for the winner

  • Ordinary simulation:

    • Duplicator wins in any case
    • Fairness conditions are ignored
  • Duplicator wins as long as the game does not halt

  • Direct simulation:

    • D wins iff for all i, if then


Rules for the winner

  • Delayed simulation:

    • D wins iff for all i, if then there exists j ≥ i such that
  • Fair simulation:

    • D wins iff there are infinitely many j such that
    • or only finitely many i such that
    • In other words: if there are infinitely many i such that
    • , then there are also infinitely many j such that


Simulation Relation

  • A state q‘ ordinary, direct, delayed, fair simulates a state q, if there is a winning strategy for D

  • The simulation relation is denoted by , where * stands for one of the 4 simulations

  • The relations are ordered by containment:

  • (preorder)

  • For di, de, f: if then



Bisimulation Games

  • For all of the mentioned simulations corresponding notions of bisimulation via modification of the game

  • S can choose in each round which pebble he will move and D has to respond with the other one

  • Bisimulations define an equivalence relation



Bisimulation winning rules

  • Fair: an accept state appears infinitely often on one of the 2 runs π and π‘ an accept state must appear infinitely often on the other as well

  • Delayed: an accept state at position i of either run an accept state at j ≥ i of the other run

  • Direct: an accept state at position i of either run

  • an accept state at position i of both runs



Problem with delayed simulation

  • Quotienting: states that simulate each other are merged

  • Difficult to find a working definition of a simulation preserving quotient with respect to delayed simulation

  • Not at all clear how such a quotient should be defined



Problem with delayed simulation

  • Example for the quotienting problem:

  • B accepts aω, but A does not

  • Removing transition (1‘,a,1‘) would provide a simulation-equivalent quotient for A



Parity Games

  • A parity game graph has two disjoint sets of vertices V0 and V1, their union is V

  • It also has an edge set and a priority function that assigns a priority to each vertex

  • Played by two players, Zero and One and the game starts by placing a pebble on



Parity Games

  • Rule for moving the pebble: pebble on vi, Zero (One) moves the pebble to vi+1, such that

  • If a player can not move, the other one wins

  • Otherwise the game produces an infinite run

  • Considering the minimum priority kπ that occurs infinitely often in the run π; Zero wins, if kπ is even, One otherwise



(Bi)Simulations from Parity Games

  • Example: Parity game graph for the fair simulation game

  • The set of vertices for Zero:

  • The set of vertices for One:

  • The set of the edges for Zero and One:

  • The priority function:



(Bi)Simulations from Parity Games

  • Example Büchi automaton:

  • kjhjk

  • V0f = {(2,1,a),(2,2,a),(2,3,a),(2,1,b),(2,2,b),(2,3,b),(2,1,c),(2,2,c),(2,3,c), (3,1,a),(3,2,a),(3,3,a)}

  • Jhkjh

  • V1f = {(1,1),(1,2),(1,3),(2,1),(2,2),(2,3),(3,1),(3,2),(3,3)}

  • Hghjg Player 0

  • Player 1

  • EAf={((2,1,a),(2,2)),((3,1,a),(3,2)),((2,2,b),(2,2)),((2,2,a),(2,3)),..} U {((1,1),(2,1,a)),((1,2),(2,2,a)),((2,2),(2,3,b)),..}



(Bi)Simulations from Parity Games

  • Example Büchi automaton:

  • kjhjk

  • pAf ((2,1,a)) = 2 ;

  • pAf ((2,3,c)) = 0 ;

  • pAf ((3,1)) = 1 ;

  • pAf ((1,3)) = 0 ;



(Bi)Simulations from Paritiy Games

  • Parity Game constructed:

    • Zero has a winning strategy from (q,q’), iff q is fairly simulated by q’
    • Jurdzinkis algorithm as fast algorithm for computing fair (bi)simulation relations and delayed simulations
    • Other relations can be constructed from the fair simulation formulas (Handout)


References

  • Carsten Fritz, Thomas Wilke: Simulation Relations for Alternating Parity Automata and Parity Games. DLT 2006, LNCS 4036, pp. 59-70, Springer-Verlag (2006)

  • Kousha Etessami, Thomas Wilke, Rebecca A. Schuller: Fair Simulation Relations, Parity Games and State Space Reduction for Büchi Automata. ICALP 2001, LNCS 2076, pp. 694-707, Springer-Verlag (2001)

  • Carsten Fritz: Simulation-Based Simplification of omega-Automata. PhD thesis, Technische Fakultät der Christian Albrecht Universität zu Kiel (2005) available at http:/e-diss.uni-kiel.de/diss_1644/




Yüklə 454 b.

Dostları ilə paylaş:




Verilənlər bazası müəlliflik hüququ ilə müdafiə olunur ©muhaz.org 2022
rəhbərliyinə müraciət

    Ana səhifə