Axiomatising Linear Time Mu-calculus

Roope Kaivola

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