Fixed points

Go to home page

On Gabbay's temporal fixed point operator

Ian Hodkinson
Theoretical Computer Science 139 (1995) 1-25
We discuss the temporal logic USF, involving Until, Since and the fixed point operator 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 fixed point operators.

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'.

Sahlqvist theorem for modal fixed point logic

Nick Bezhanishvili and Ian Hodkinson
Theoretical Computer Science 424 (2012) 1-19.
We define Sahlqvist fixed point formulas. By extending the technique of Sambin and Vaccaro we show that (1) for each Sahlqvist fixed point formula $\varphi$ there exists an LFP-formula $\chi(\varphi)$, with no free first-order variable or predicate symbol, such that a descriptive $\mu$-frame (an order-topological structure that admits topological interpretations of least fixed point operators as intersections of clopen pre-fixed points) validates $\varphi$ iff $\chi(\varphi)$ is true in this structure, and (2) every modal fixed point logic axiomatized by a set $\Phi$ of Sahlqvist fixed point formulas is sound and complete with respect to the class of descriptive $\mu$-frames satisfying $\{\chi(\varphi): \varphi\in \Phi\}$. We also give some concrete examples of Sahlqvist fixed point logics and classes of descriptive $\mu$-frames for which these logics are sound and complete.

Sahlqvist correspondence for modal mu-calculus

Johan van Benthem, Nick Bezhanishvili, Ian Hodkinson
Studia Logica 100 (2012) 31-60.
We define analogues of modal Sahlqvist formulas for the modal mu-calculus, and prove a correspondence theorem for them.

Preservation of Sahlqvist fixed point equations in completions of relativized fixed point BAOs

Nick Bezhanishvili and Ian Hodkinson
Algebra Universalis 68 (2012) 43-56.
We define Sahlqvist fixed point equations and relativized fixed point Boolean algebras with operators (relativized fixed point BAOs). We show that every Sahlqvist fixed point equation is preserved under completions of conjugated relativized fixed point BAOs. This extends the result of Givant and Venema (1999) to the setting of relativized fixed point BAOs.