Efficiently Deciding µ-calculus with Converse over Finite Trees

Pierre Genevès 1 Nabil Layaïda 1 Alan Schmitt 2 Nils Gesbert 1
1 TYREX - Types and Reasoning for the Web
Inria Grenoble - Rhône-Alpes, LIG - Laboratoire d'Informatique de Grenoble
2 CELTIQUE - Software certification with semantic analysis
Inria Rennes – Bretagne Atlantique , IRISA-D4 - LANGAGE ET GÉNIE LOGICIEL
Abstract : 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.
Keywords : Modal Logic implementation satisfiability verification
Type de document :
Article dans une revue
ACM Transactions on Computational Logic, Association for Computing Machinery, 2015, 16 (2), pp.41. 〈http://tocl.acm.org/〉. 〈10.1145/2724712〉
Liste complète des métadonnées

Littérature citée [30 références]  Voir  Masquer  Télécharger
https://hal.inria.fr/hal-00868722
Contributeur : Tyrex Equipe <>
Soumis le : vendredi 30 janvier 2015 - 15:28:14
Dernière modification le : mercredi 16 mai 2018 - 11:23:28
Document(s) archivé(s) le : samedi 15 avril 2017 - 23:40:17

Fichier

tree-calculus.pdf
Fichiers produits par l'(les) auteur(s)

Licence

Copyright (Tous droits réservés)

Identifiants

Collections

INRIA | LIG | UGA | CENTRALESUPELEC | IRISA | IRISA-D4 | LIG_SRCPR | UR1-UFR-ISTIC | UNIV-RENNES

Citation

Pierre Genevès, Nabil Layaïda, Alan Schmitt, Nils Gesbert. Efficiently Deciding µ-calculus with Converse over Finite Trees. ACM Transactions on Computational Logic, Association for Computing Machinery, 2015, 16 (2), pp.41. 〈http://tocl.acm.org/〉. 〈10.1145/2724712〉. 〈hal-00868722v5〉

Exporter

BibTeX TEI DC DCterms EndNote

Partager

Métriques

Consultations de la notice

1236

Téléchargements de fichiers

267

Contact


archive-ouverte@inria.fr