Efficiently Deciding µ-calculus with Converse over Finite Trees - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Article Dans Une Revue ACM Transactions on Computational Logic Année : 2015

Efficiently Deciding µ-calculus with Converse over Finite Trees

Pierre Genevès
Nabil Layaïda
Nils Gesbert
  • Fonction : Auteur
  • PersonId : 899056

Résumé

We present a sound and complete satisfiability-testing algorithm and its effective implementation for an alternation-free modal µ-calculus with converse, where formulas are cycle-free and are interpreted over finite ordered trees. The time complexity of the satisfiability-testing algorithm is 2^O(n) in terms of formula size n. The algorithm is implemented using symbolic techniques (BDD). We present crucial implementation techniques and heuristics that we used to make the algorithm as fast as possible in practice. Our implementation is available online, and can be used to solve logical formulas of significant size and practical value. We illustrate this in the setting of XML trees.
Fichier principal
Vignette du fichier
tree-calculus.pdf (605.64 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)
Loading...

Dates et versions

hal-00868722 , version 1 (01-10-2013)
hal-00868722 , version 2 (31-01-2014)
hal-00868722 , version 3 (03-06-2014)
hal-00868722 , version 4 (14-01-2015)
hal-00868722 , version 5 (30-01-2015)

Licence

Copyright (Tous droits réservés)

Identifiants

Citer

Pierre Genevès, Nabil Layaïda, Alan Schmitt, Nils Gesbert. Efficiently Deciding µ-calculus with Converse over Finite Trees. ACM Transactions on Computational Logic, 2015, 16 (2), pp.41. ⟨10.1145/2724712⟩. ⟨hal-00868722v5⟩
743 Consultations
634 Téléchargements

Altmetric

Partager

Gmail Facebook X LinkedIn More