(Bi)Simulation Games

Finite Model Theorists are most familiar with the simulation and bisimulation games. These games appeared first when Roland Fraisse developed a sort of bounded back-and-forth technique for proving that two first order structures were first order equivalent to a given "depth"; in a 1961 paper, Andrzej Ehrenfeucht published a paper in Fund. Math. characterizing this back-and-forth construction as a combinatorial game. During the 1970s, similar games were developed by Jon Barwise and Neil Immerman, Ron Fagin, Johan van Benthem, etc., etc., etc.: by the late 1980s, development of simulation and bisimulation games had become a cottage industry.

As an example of this sort of thing, let's look at (an updated version of) the k-pebble Barwise-Immerman game. The board is a pair of structures A, B of a common signature. There are 2k pebbles, k for each structure, labelled 1, 2, 3, ..., k. There are two players, the Spoiler and the Duplicator.

• After k pairs of moves, there vertices a(1), ..., a(k) in A and b(1), ..., b(k) in B pebbled by the 1st, ..., kth pebbles of their respective structures.
• The Spoiler wins here if the map a(l) |--> b(l), c(i)^A |--> c(i)^B is not a partial isomorphism.
• If the Spoiler does not win, she moves by shifting a pebble, and the Duplicator shifts the corresponding pebble of the other structure, and the game goes back to (2).

Notice that the Spoiler's position, of having to win, is analogous to Eloise's position, while the Duplicator's, like Abelard's, is merely a matter of not losing.

The BiSimulation Theorem

We continue to use the Barwise-Immerman bisimulation game as a model.

If the Duplicator has a winning strategy to win the k-pebble game for A versus B, write A =_k B.

Theorem. For each k, =_k is an equivalence relation.

Theorem. Let PHI be a GTS game program whose states have at most k variables. (So PHI corresponds to an FO + LFP formula of at most k variables.) If A =_k B, then Eloise wins PHI on A iff she wins PHI on B.

Actually, this Theorem works for FO + PFP queries, and hence for the corresponding GTS games (which use "clocks"). This leads to a point: for a class G of GTS games, we can develop a corresponding Simulation or Bisimulation game. There are two consequences:

• We can reduce G to combinatorial games on the equivalence classes of the bisimulation games.
• We find that some classes of GTS games do not seem to have precisely appropriate (bi)simulation games --- and this limits what descriptive complexity results can be proven about the corresponding logics using (bi)simulation games.

Limitations of (Bi)Simulation

(Bi)simulation can be a blunt instrument. For example, in the Barwise-Immerman bisimulation game, all equivalence classes are FO + LFP expressible, while the equivalence relation preserves FO + PFP queries. So unless FO + LFP $\equiv$ FO + PFP (!), the fit is looser than we would like.

Sometimes we KNOW that the fit is too loose. Recall that FO + pos UFP is the set of queries whose GTS game programs have no existential recursive queries, while FO + pos EFP is the set of qeuries whose programs have no universal recursive queries.

The obvious simulation game for these is: given k, A, and B, there may be at most k pebbles on a structure at a time, and the Spoiler can make at most k moves in B in the entire game.

If the Duplicator wins, write A =>_k B. So if phi was a FO + pos EFP query and psi was a FO + pos UFP query, both of at most k variables and alternations, then A =>_k B implies that