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.
Type de document :
Article dans une revue
Information Processing Letters, Elsevier, 2016, 〈10.1016/j.ipl.2016.04.015〉
Liste complète des métadonnées

Littérature citée [2 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-01362289
Contributeur : Olivier Serre <>
Soumis le : jeudi 8 septembre 2016 - 15:01:47
Dernière modification le : mercredi 11 avril 2018 - 12:12:03
Document(s) archivé(s) le : vendredi 9 décembre 2016 - 12:50:12

Fichier

CS-ArXiV.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Collections

Citation

Arnaud Carayol, Olivier Serre. Marking shortest paths on pushdown graphs does not preserve MSO decidability. Information Processing Letters, Elsevier, 2016, 〈10.1016/j.ipl.2016.04.015〉. 〈hal-01362289〉

Partager

Métriques

Consultations de la notice

155

Téléchargements de fichiers

43