Simulation Games Michael Maurer

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/