Anzeige
Erschienen in:
2009 | OriginalPaper | Buchkapitel
A Tableau System for the Modal μ-Calculus
verfasst von : Natthapong Jungteerapanich
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
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.