| HAL-Inria | Publications, software ... of Inria's scientists |
Journal articles
Efficiently Deciding µ-calculus with Converse over Finite Trees
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.
Cited literature [30 references]
https://hal.inria.fr/hal-00868722
Contributor : Tyrex Equipe <>
Submitted on : Friday, January 30, 2015 - 3:28:14 PM
Last modification on : Wednesday, February 10, 2021 - 3:34:23 AM
Long-term archiving on: : Saturday, April 15, 2017 - 11:40:17 PM
Contributor : Tyrex Equipe <>
Submitted on : Friday, January 30, 2015 - 3:28:14 PM
Last modification on : Wednesday, February 10, 2021 - 3:34:23 AM
Long-term archiving on: : Saturday, April 15, 2017 - 11:40:17 PM
File
tree-calculus.pdf
Files produced by the author(s)