Anzeige
Erschienen in:
2005 | OriginalPaper | Buchkapitel
A Decision Procedure for the Alternation-Free Two-Way Modal μ-Calculus
verfasst von : Yoshinori Tanabe, Koichi Takahashi, Mitsuharu Yamamoto, Akihiko Tozawa, Masami Hagiya
Erschienen in: Automated Reasoning with Analytic Tableaux and Related Methods
Verlag: Springer Berlin Heidelberg
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
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.