Bisimulation game
= Bisimulation game
{title2=$G_{\mathrm{bisim}}(G,H)$}
The Spoiler takes one successor step from the current vertex of either <rooted directed graph>; the Duplicator must take a matching successor step in the other. The Duplicator wins by never failing at a finite stage, including when the Spoiler cannot move. A winning strategy gives a <bisimulation> by collecting endpoint pairs of all finite plays consistent with it.