Yoshinori Tanabe, Koichi Takahashi, Mitsuharu Yamamoto, Akihiko Tozawa, and Masami Hagiya: A Decision Procedure for the Alternation-free Two-way Modal μ-calculus. TABLEAUX 2005, to appear in Lecture Notes in Artificial Intelligence, vol 3702.


The satisfiability checking problem is known to be decidable for a variety of modal/temporal logics such as the modal μ-calculus, but effective implementation has not necessarily been developed for all such logics. In this paper, we propose a decision procedure using the tableau method for the alternation-free two-way modal μ-calculus. Although the size of the tableau set maintained in the method might be large for complex formulas, the set and the operations on it can be expressed using BDD and therefore we can implement the method in an effective way.



The source is written mostly in Java. You need Java BDD and Java CC for compilation. Unfortunately, there is no document on the usage.