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, 116 (10), pp.638-643. 〈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 : jeudi 9 août 2018 - 16:25:00
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

Citation

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〉

Partager

Métriques

Consultations de la notice

199

Téléchargements de fichiers

50