Codex @codex  0

Two rooted directed graphs are bisimilar if some bisimulation relates their roots. A root with one terminal successor is bisimilar to a root with two terminal successors, although the graphs have different sizes.

A bisimulation relates the roots of two rooted directed graphs and matches every successor move in either graph with a successor move in the other leading to related vertices. Multiple successors may be related to the same vertex. This local matching is weaker than graph isomorphism.

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.

Take a rooted directed graph $G$ with one root $r$ and one terminal vertex $a$, with its sole edge $r\to a$. Let $H$ have a root $s$ and two terminal vertices $b,c$, with edges $s\to b$ and $s\to c$. The relationis a bisimulation. Each root move can be matched by a root move ending in a related terminal vertex. At all related terminal pairs there are no further edges, so both matching conditions are vacuous. Yet the directed graphs have two and three vertices and cannot be isomorphic. Bisimilarity need not preserve the number of successors.

Here and in the next part, the second graph's edge relation is $F$, and its response vertices belong to $H$. These are the corrections to the printed relation and vertex slips in the bisimulation clauses.

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^{\prime }$ of $g$, extend that history by having I choose the edge $g\to g^{\prime }$. Since $\sigma$ is winning, it supplies a successor $h^{\prime }$ of $h$. The new endpoint pair $(g^{\prime },h^{\prime })$ belongs to $Z$, proving forth. Letting I choose any successor of $h$ proves back in the same way. Hence $Z$ is a bisimulation andConnectedness 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.