Rooted directed graph ($(G,E,r_G)$)

A rooted directed graph has a distinguished root. Root-connectedness means each vertex can be reached by a finite directed path from that root. This is directed reachability, rather than connectedness of the underlying undirected graph.

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.

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.