Title
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.
Abstract
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.
Files
source
The source is written mostly in Java. You need Java BDD and Java CC for compilation.
Unfortunately, there is no document on the usage.