A temporal fixpoint calculus

Abstract

Two distinct extensions of temporal logic has been recently advocated in the literature. The first extension is the addition of fixpoint operators that enable the logic to make assertions about arbitrary regular events. The second extension is the addition of past temporal connectives that enables the logic to refer directly to the history of the computation. Both extensions are motivated by the desire to adapt temporal logic to modular, i.e, compositional, verification (as opposed to global verification). We introduce and study here the logic μTL, which is the extension of temporal logic by fixpoint operators and past temporal connectives. We extend the automata-theoretic paradigm to μTL. That is, we show how, given an μTL formula φ, we can produce a finite-state Biichi automaton Aφ, whose size is at most exponentially bigger than the size of φ, such that Aφ accepts precisely the computations that satisfy φ. The result has immediate applications, e.g., an optimal decision procedure and a model-checking algorithm for μTL.