Abstract: We present a sound and complete axiomatisation for the linear time mu-calculus nu T L, a language extending standard linear time temporal logic with fixpoint operators. The completeness proof is based on a new bi-aconjunctive non-alternating normal form for nu T L-formulae.
LFCS report ECS-LFCS-95-324, June 1995.
Previous | Index | Next