Titre :

Logics for Unordered Trees with Data Constraints

Auteur(s) :

Boiret, Adrien [Auteur]
Linking Dynamic Data [LINKS]
Hugot, Vincent [Auteur]
Sécurité des Données et des Systèmes [SDS]
Niehren, Joachim [Auteur]
Linking Dynamic Data [LINKS]
Treinen, Ralf [Auteur]
Preuves, Programmes et Systèmes [PPS]

Titre de la revue :

Journal of Computer and System Sciences

Pagination :

40

Éditeur :

Elsevier

Date de publication :

2019-01-30

ISSN :

0022-0000

Mot(s)-clé(s) en anglais :

data trees
Counting Mso
string comparisons
logics

Discipline(s) HAL :

Informatique [cs]/Théorie et langage formel [cs.FL]
Informatique [cs]/Logique en informatique [cs.LO]

Résumé en anglais : [en]

We study counting monadic second-order logics (CMso) for unordered data trees. Our objective is to enhance this logic with data constraints for comparing string data values. Comparisons between data values at arbitrary ...
Lire la suite >We study counting monadic second-order logics (CMso) for unordered data trees. Our objective is to enhance this logic with data constraints for comparing string data values. Comparisons between data values at arbitrary positions of a data tree quickly lead to undecidability. Therefore, we restrict ourselves to comparing sibling data values of unordered trees. But even in this case CMso remains undecidable when allowing data comparisons that can check the equality of string factors. However, for more restricted data constraints that can only check the equality of string prefixes, it becomes decidable. This decidability result is obtained by reduction to WSkS. Furthermore, we exhibit a restricted class of constraints which can be used in transitions of tree automata, resulting in a model with tractable complexity, which can be extended with structural equality tests between siblings. This practical restriction is relevant to applications such as checking well-formedness properties of file system trees.Lire moins >

Langue :

Anglais

Comité de lecture :

Oui

Audience :

Internationale

Vulgarisation :

Non

Projet ANR :

Correction de scripts Linux

Collections :

• Centre de Recherche en Informatique, Signal et Automatique de Lille (CRIStAL) - UMR 9189

Source :

Harvested from HAL