Marking shortest paths on pushdown graphs does not preserve MSO decidability

• We consider pushdown graphs where some vertices are designated as being final.
• We built, in a breadth-first manner, a marking of edges leading to final vertices.
• Edge-marked version of a pushdown graph may itself no longer be a pushdown graph.
• Edge-marked version of a pushdown graph may have an undecidable MSO theory.

In this paper we consider pushdown graphs, i.e. infinite graphs that can be described as transition graphs of deterministic real-time pushdown automata. We consider the case where some vertices are designated as being final and we build, in a breadth-first manner, a marking of edges that lead to such vertices (i.e., for every vertex that can reach a final one, we mark all out-going edges laying on some shortest path to a final vertex).Our main result is that the edge-marked version of a pushdown graph may itself no longer be a pushdown graph, as we prove that the MSO theory of this enriched graph may be undecidable.