Efficiently Deciding μ-Calculus with Converse over Finite Trees

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 interp...