摘要 : We present a sound and complete satisfiability-testing algorithm and its effective implementation for an alternation-free modal mu-calculus with converse, where formulas are cycle-free and are interpreted over finite ordered trees... 展开 We present a sound and complete satisfiability-testing algorithm and its effective implementation for an alternation-free modal mu-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 p 收起