In: Desel, J.: Structures in Concurrency Theory, Proceedings of the International Workshop on Structures in Concurrency Theory (STRICT), Berlin, 11-13 May 1995, pages 190-204. 1995.
Abstract: The linear mu-calculus vTL is a language extending standard linear time temporal logic with fixpoint operators. We present a method for deciding whether a given vTL -formula is satisfiable, and give a direct proof of its completeness. Although simpler than the existing methods, it gives rise to an algorithm working in the same 20(nē log n) time as these or alternatively, to a polynomial space, singly exponential time algorithm. What is more important or computer-aided (as opposed to fully automated) satisfiability checking.