= Solution
Suppose first that $Z$ is a <bisimulation> containing the root pair. II maintains the invariant that the current pair lies in $Z$. If I moves in the first <rooted directed graph>, the forth clause supplies a matching successor in the second; if I moves in the second, the back clause supplies a matching successor in the first. II can choose such a response every time I can move. Therefore II never loses after finitely many steps and wins the <bisimulation game>.
Conversely, let $\sigma$ be a winning strategy for II. Define $Z$ to consist of all endpoint pairs of finite legal plays starting at the roots and consistent with $\sigma$, including the initial root pair. This definition keeps every possible history; it does not assume that $\sigma$ depends only on the current position.
Take $(g,h)\in Z$ and a finite history realizing it. For any successor $g'$ of $g$, extend that history by having I choose the edge $g\to g'$. Since $\sigma$ is winning, it supplies a successor $h'$ of $h$. The new endpoint pair $(g',h')$ belongs to $Z$, proving forth. Letting I choose any successor of $h$ proves back in the same way. Hence $Z$ is a <bisimulation> and
$$
\boxed{\text{II wins the bisimulation game}\iff G\text{ and }H\text{ are bisimilar}.}
$$
Connectedness ensures that both projections of $Z$ cover all vertices: I can walk any finite directed path from either root and II's strategy supplies the matching path. The equivalence itself only concerns the rooted reachable behaviour and remains valid without connectedness.
Back to article page
