| HAL-Inria | Publications, software ... of Inria's scientists |
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.
Cited literature [2 references]
https://hal.inria.fr/hal-01362289
Contributor : Olivier Serre <>
Submitted on : Thursday, September 8, 2016 - 3:01:47 PM
Last modification on : Wednesday, February 3, 2021 - 7:54:27 AM
Long-term archiving on: : Friday, December 9, 2016 - 12:50:12 PM
Contributor : Olivier Serre <>
Submitted on : Thursday, September 8, 2016 - 3:01:47 PM
Last modification on : Wednesday, February 3, 2021 - 7:54:27 AM
Long-term archiving on: : Friday, December 9, 2016 - 12:50:12 PM
File
CS-ArXiV.pdf
Files produced by the author(s)