The linear time
μ-calculus extends LTL with arbitrary least and greatest fixpoint operators. This gives it the power to express all
ω-regular languages, i.e. strictly more than LTL. The validity problem is PSPACE-complete for both LTL and the linear time
μ-calculus. In practice it is more difficult for the latter because of nestings of fixpoint operators and variables with several
occurrences.
We present a simple sound and complete infinitary proof system for the linear time μ-calculus and then present two decision procedures for provability in the system, hence validity of formulas. One uses nondeterministic
Büchi automata, the other one a generalisation of size-change termination analysis (SCT) known from functional programming.
The main novelties of this paper are the connection with SCT and the fact that both decision procedures have a better asymptotic
complexity than earlier ones and have been implemented.