Marking shortest paths on pushdown graphs does not preserve MSO decidability - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Article Dans Une Revue Information Processing Letters Année : 2016

Marking shortest paths on pushdown graphs does not preserve MSO decidability

Résumé

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.
Fichier principal
Vignette du fichier
CS-ArXiV.pdf (213.1 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)
Loading...

Dates et versions

hal-01362289 , version 1 (08-09-2016)

Identifiants

Citer

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

Altmetric

Partager

Gmail Facebook X LinkedIn More