Temporal Access to the Iteration Sequences: A Unifying Approach to Fixed Point Logics

The semantics of fixed point constructions is commonly defined in terms of iteration sequences. For example, the least fixed point of a monotone operator consists of all points which eventually appear in the approximations computed iteratively. We take this temporal reading as the starting point and develop a systematic approach to temporal definitions over iteration sequences. As a result, we propose an extension of first-order predicate logic with an iterative operator, in which iteration steps may be accessed by temporal logic formulae. We show that proposed logic FO+TAI subsumes virtually all known deterministic fixed point extentions of first-order logic as its natural fragments. On the other hand we show that over finite structures FO+TAI has the same expressive power as FO+PFP (FO with partial fixed point operator), but in many cases providing with more concise definitions. Finally, we show that the extension of modal mu-calculus with the temporal access leads to the more expressive logic closed under assume-guarantee specifications operator.