Skip to Main content Skip to Navigation
Journal articles

Marking shortest paths on pushdown graphs does not preserve MSO decidability

Abstract : 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 outgoing 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.
Document type :
Journal articles
Complete list of metadata

Cited literature [2 references]  Display  Hide  Download
Contributor : Olivier Serre Connect in order to contact the contributor
Submitted on : Thursday, September 8, 2016 - 3:01:47 PM
Last modification on : Saturday, January 15, 2022 - 3:57:12 AM
Long-term archiving on: : Friday, December 9, 2016 - 12:50:12 PM


Files produced by the author(s)



Arnaud Carayol, Olivier Serre. Marking shortest paths on pushdown graphs does not preserve MSO decidability. Information Processing Letters, Elsevier, 2016, 116 (10), pp.638-643. ⟨10.1016/j.ipl.2016.04.015⟩. ⟨hal-01362289⟩



Record views


Files downloads