Bisimulation game ($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.