On Gabbay's temporal fixed point operator

    I. Hodkinson

    Theoretical Computer Science 139 (1995) 1--25.

    We discuss the temporal logic 'USF', involving Until, Since, and the fixed point operator $\varphi$ of Gabbay, with semantics over the natural numbers. We show that any formula not involving Until is equivalent to one without nested fixed point operators. We then prove that USF has expressive power matching that of the monadic second-order logic S1S. The proof shows that any USF-formula is equivalent to one with at most two nested fixed point operators -- i.e., no branch of its formation tree has more than two fs. We then axiomatise USF and prove that it is decidable, with PSPACE-complete satisfiability problem. Finally, we discuss an application of these results to the executable temporal logic system 'MetateM'.