Name
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. |
Year | DOI | Venue |
|---|---|---|
2005 | 10.1007/11554554_21 | TABLEAUX |
Keywords | DocType | ISBN |
temporal logic,decision procedure,tableau method,effective implementation,alternation-free two-way modal,satisfiability checking problem,complex formula | Conference | 3-540-28931-3 |
Citations | PageRank | References |
9 | 0.58 | 9 |
Authors | ||
5 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Yoshinori Tanabe | 1 | 124 | 13.96 |
| Koichi Takahashi | 2 | 38 | 6.30 |
| Mitsuharu Yamamoto | 3 | 91 | 11.09 |
| Akihiko Tozawa | 4 | 246 | 20.56 |
| Masami Hagiya | 5 | 649 | 102.85 |