Tableau systems for the modal μ-calculus

Abstract

The main content of this thesis concerns a tableau method for solving the satisfiability problem for the modal μ-calculus. A sound and complete tableau system for the modal μ-calculus is given. Since every tableau in such tableau system is finite and bounded by the length of the formula, the tableau system may be used as a decision procedure for determining the satisfiability of the formula. An alternative proof of the small model property is obtained: every satisfiable formula has a model of size singleexponential in the length of the formula. Contrary to known proofs in literature, the results presented here do not rely on automata theory. Two simplifications of the tableau system are given. One is for the class of aconjunctive formulae. The resulting tableau system has been used to prove the completeness of Kozen’s axiomatisation with respect to the aconjunctive fragment of the modal μ- calculus. Another is for the formulae in the class Πμ 2 . In addition to the tableau method, the thesis explores some model-surgery techniques with the aim that such techniques may be used to directly prove the small model theorem. The techniques obtained so far have been used to show the small model property for Πμ 2 -formulae and for formulae with linear models.