FO2(<,+1,~) on data trees, data tree automata and branching vector addition systems.

Florent Jacquemard 1, 2 Luc Segoufin 3 Jérémie Dimino 4
1 Repmus - Représentations musicales
STMS - Sciences et Technologies de la Musique et du Son
2 MuTant - Synchronous Realtime Processing and Programming of Music Signals
UPMC - Université Pierre et Marie Curie - Paris 6, IRCAM, CNRS - Centre National de la Recherche Scientifique, Inria de Paris
3 DAHU - Verification in databases
LSV - Laboratoire Spécification et Vérification [Cachan], ENS Cachan - École normale supérieure - Cachan, Inria Saclay - Ile de France, CNRS - Centre National de la Recherche Scientifique : UMR8643
Abstract : A data tree is an unranked ordered tree where each node carries a label from a finite alphabet and a datum from some infinite domain. We consider the two variable first order logic FO 2 (<, +1, ∼) over data trees. Here +1 refers to the child and the next sibling relations while < refers to the descendant and following sibling relations. Moreover, ∼ is a binary predicate testing data equality. We exhibit an automata model, denoted DTA # , that is more expressive than FO 2 (<, +1, ∼) but such that emptiness of DTA # and satisfiability of FO 2 (<, +1, ∼) are inter-reducible. This is proved via a model of counter tree automata, denoted EBVASS, that extends Branching Vector Addition Systems with States (BVASS) with extra features for merging counters. We show that, as decision problems, reachability for EBVASS, satisfiability of FO 2 (<, +1, ∼) and emptiness of DTA # are equivalent.
Type de document :
Article dans une revue
Logical Methods in Computer Science, Logical Methods in Computer Science Association, 2016, 12 (2), pp.32
Liste complète des métadonnées

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

https://hal.inria.fr/hal-00769249
Contributeur : Luc Segoufin <>
Soumis le : vendredi 26 février 2016 - 11:40:23
Dernière modification le : mercredi 21 mars 2018 - 18:58:22

Fichier

tdafo.pdf
Fichiers produits par l'(les) auteur(s)

Licence


Distributed under a Creative Commons Paternité - Pas d'utilisation commerciale 4.0 International License

Identifiants

  • HAL Id : hal-00769249, version 3
  • ARXIV : 1601.01579

Citation

Florent Jacquemard, Luc Segoufin, Jérémie Dimino. FO2(<,+1,~) on data trees, data tree automata and branching vector addition systems.. Logical Methods in Computer Science, Logical Methods in Computer Science Association, 2016, 12 (2), pp.32. 〈hal-00769249v3〉

Partager

Métriques

Consultations de la notice

396

Téléchargements de fichiers

92