| Article ID | Journal | Published Year | Pages | File Type |
|---|---|---|---|---|
| 427029 | Information Processing Letters | 2016 | 6 Pages |
•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.
