Editing Bisimulation (section)

===  Ehrenfeucht–Fraïssé game definition  ===
Bisimulation can also be thought of in terms of a game between two players:  attacker and defender.

"Attacker" goes first and may choose any valid transition, <math>\lambda</math>, from <math>(p,q)</math>. That is,
<math display="block">
(p,q) \overset{\lambda}{\rightarrow} (p',q)
</math>
or 
<math display="block">
(p,q) \overset{\lambda}{\rightarrow} (p,q')
</math>

The "Defender" must then attempt to match that transition, <math>\lambda</math> from either <math>(p',q)</math> or <math>(p,q')</math> depending on the attacker's move.
I.e., they must find an  <math>\lambda</math> such that:
<math display="block">
(p',q) \overset{\lambda}{\rightarrow} (p',q')
</math>
or 
<math display="block">
(p,q') \overset{\lambda}{\rightarrow} (p',q')
</math>

Attacker and defender continue to take alternating turns until:

* The defender is unable to find any valid transitions to match the attacker's move.  In this case the attacker wins.
* The game reaches states <math>(p,q)</math> that are both 'dead' (i.e., there are no transitions from either state) In this case the defender wins
* The game goes on forever, in which case the defender wins.
* The game reaches states <math>(p,q)</math>, which have already been visited.  This is equivalent to an infinite play and counts as a win for the defender.

By the above definition the system is a bisimulation if and only if there exists a winning strategy for the defender.