# 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

##### MSC:
 03B25 Decidability of theories and sets of sentences 68Q65 Abstract data types; algebraic specification
##### Keywords:
$$\mu$$ -calculus