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.
Previous | Index | Next An error occured whilst processing this directive