zbMATH — the first resource for mathematics

A decision procedure for the propositional \(\mu\)-calculus. (English) Zbl 0564.03012
Logics of programs, Workshop, Pittsburgh/PA 1983, Lect. Notes Comput. Sci. 164, 313-325 (1984).
[For the entire collection see Zbl 0533.00026.]
This is a technical paper, in which the decidability is proven of the propositional \(\mu\)-calculus \(L\mu\), in an unrestricted version. The proof is based on a reduction of \(L\mu\) to the second order theory of n successors, which is shown decidable by Rabin. This reduction in its turn depends on the fact that every satisfiable formula is satisfied in a tree model of finite degree. The decision procedure thus obtained is nonelementary. It is still unknown whether there exists an elementary one.
Reviewer: J.-J.Ch.Meyer

03B25 Decidability of theories and sets of sentences
68Q65 Abstract data types; algebraic specification