CMP.13:5.1 - A graph summary invents a path

The original graph has vertices a,b,c,d, edges a->b and c->d, and initial vertex a. The question is whether d is reachable. Merge b and c into abstract vertex q, while keeping a and d separate. An abstract edge exists when any original edge connects the corresponding classes.

The abstract graph has a->q and q->d. Searching it returns the path a,q,d. Each edge has an original witness, yet the first edge arrives at b and the second leaves c.

Reconstruction gives X0={a}, X1={b} and X2=empty, since b has no successor. Split q into {b} and {c}. The recomputed reachable set is {a,b}, so d is unreachable. The useful result is both the answer and the reason the original summary could not establish it.

Changed condition: add edge b->c. The abstract path a,q,q,d now reconstructs to a,b,c,d; this is a real path. The shorter path a,q,d still has no consecutive realization, but its failure no longer excludes reachability. The transition change requires the affected search and reconstruction to be updated.