2009 | OriginalPaper | Chapter
A Tableau System for the Modal μ-Calculus
Author : Natthapong Jungteerapanich
Published in: Automated Reasoning with Analytic Tableaux and Related Methods
Publisher: Springer Berlin Heidelberg
Activate our intelligent search to find suitable subject content or patents.
Select sections of text to find matching patents with Artificial Intelligence. powered by
Select sections of text to find additional relevant content using AI-assisted search. powered by
This paper presents a tableau system for determining satisfiability of modal
μ
-calculus formulas. The modal
μ
-calculus, which can be seen as an extension of modal logic with the least and greatest fixpoint operators, is a logic extensively studied in verification and has been shown to subsume many well-known temporal and modal logics including CTL, CTL
*
, and PDL. Concerning the satisfiability problem, the known methods in literature employ results from the theory of automata on infinite objects. The tableau system presented here provides an alternative solution which does not rely on automata theory. Since every tableau in the system is a finite tree structure (bounded by the size of the initial formula), this leads to a decision procedure for satisfiability and a small model property. The key features are the use of names to keep track of the unfolding of variables and the notion of name signatures used in the completeness proof.