Algorithmic Game Theory and Applications
Lecture 14: Simulation, Bisimulation, and
other Ehrenfeucht-Fr ̈aisse Games
Kousha Etessami AGTA: Lecture 14
Copyright By PowCoder代写 加微信 powcoder
• A game played on two labelled directed graphs G1 = (V1,E1,l1) and G2 = (V2,E2,l2), whose nodes are labelled by a symbol from alphabet Σ. Namely, li : Vi → Σ, for i = 1,2. We assume that each vertex of both graphs has outdegree at least 1 (this just simplifies the game description).
• Initially, the game starts with a pebble on a start node u0 of G1 and a start node v0 of G2.
• In iteration i, player 1 picks a vertex ui, such that (ui−1,ui) ∈ E1, and player 2 responds by picking a vertex vi such that there is an edge (vi−1, vi) ∈ E2.
• Player 1 wins the game if it is ever the case that l1(ui) ̸= l2(vi), for any iteration i. Player 2 wins the game otherwise.
• This is a win-lose game of perfect information. By Borel determinacy (in fact, by open set determinacy), the game is determined, and one player or the other has a winning strategy.
Simulation
AGTA: Lecture 14
• Same as simulation, except for one thing:
• in each round, i, player 1 gets to choose whether to pick the next vertex vi or the next vertex ui, and player 2 has to respond by picking ui or vi, respectively.
• Obviously, this win-lose game is also determined for similar reasons.
• These games are important in logic/automata theory.
In particular, bisimulation captures the expressive power of propositional modal logic in the following sense: two vertices u0 and v0 of two labelled directed graphs G1 and G2 are not distinguishable by any propositional modal formula if and only if player 2 has a winning strategy in the bisimulation game over G1 and G2 starting at u0 and v0.
• Given G1 and G2, and u0 and v0, how can we efficiently decide which player has a winning strategy in this game? (Hint: you already know the answer from previous lectures.)
Etessami AGTA: Lecture 14
Ehrenfeucht-Fr ̈aisse Games and First-Order Logic
• Just as (bi)simulation captures the expressive power of modal logic, there are games that capture the expressive power of other logics.
• In particular, first-order logic, which can arguably be called “the mother of all logics”, is captured by Ehrenfeucht-Fraisse Games.
Recall: a first-order formula looks like, e.g.:
∀x ∃y ∀z(E(x, y)∧¬E(y, z))∨(E(y, x)∧E(x, y))
• We will stick to Ehrenfeucht-Fr ̈aisse games played on a pair of directed graphs G0 = (V1,E1) and G1 = (V2,E2). The game definition generalizes naturally to games played on arbitrary first-order structures.
• in the k-pebble EF-game, each player has k pebbles. These pebbles come in named pairs (P0,i, P1,i), i = 1, . . . , k, respectively.
In each round, Player 1 chooses some i ∈ {1,…,k}, and picks up one of the two pebbles
AGTA: Lecture 14
Pj,i, where j is either 0 or 1, and it places Pj,i on some vertex v of Gj. Then Player 2 responds by picking up P1−j,i and placing it on some vertex v′ of G1−j.
• Player 1 wins if it is ever the case that the mapping which maps the vertex pebbled by P0,i to the vertex pebbled by P1,i, for i = 1,…,k, is not an isomorphism of the “induced subgraph” induced in G0 by the vertices pebbled by P0,1,…,P0,k, and that induced in G1 by P1,1, . . . , P1,k.
• Theorem: (Ehrenfeucht’61) The two structures G0 and G1 are indistinguishable by a first-order formula with k variables if and only if player 2 has a winning strategy in the k-pebble EF-game on G0 and G1.
• Given G1 and G2, how would can we decide if there is any first-order formula with k variables that distinguishes them?
AGTA: Lecture 14
程序代写 CS代考 加微信: powcoder QQ: 1823890830 Email: powcoder@163.com