A Unifying Analytical Framework for Discrete, Linear Time

Ben Moszkowski

In the course of over 50 years, a number of so-called omega-regular logics have been proposed for reasoning about discrete, infinite linear time and systems modelled with this. Formulas in these logics define exactly the omega-regular languages, which are like conventional regular languages, but over infinite words. The distinguished logicians Church and Tarski initiated the study of such formalisms, which permit precisely analysing various basic aspects of discrete-time behaviour such as decidability in a formal, yet simple logical framework. They include versions of temporal logic of practical importance to computer science, some of which are extensively used in industry and are found in IEEE standards.

We describe a promising new analytical approach to omega-regular logics. It is the result of our work on relatively nonconstructive proofs of axiomatic completeness for such logics. Our framework is based on Interval Temporal Logic (ITL), a well-established, stable formalism first studied over 25 years ago, and avoids some of the technical complexities previously encountered. In particular, it totally dispenses with the requirement of embedding nontrivial proofs involving complementing nondeterministic omega-regular automata which recognise infinite words. Instead, we only need to invoke, without embedded proofs, some existing well-established theorems and avoid the need to encode and reason about nondeterministic omega-regular automata in the logics' proof systems.

The resulting axiom system for propositional ITL (PITL) and related theory appear to enable much simpler proofs of axiomatic completeness for the omega-regular logic S1S and quantified propositional linear-time temporal logic (QPTL) with past-time. Moreover, they suggest improved, more natural axiom systems for other omega-regular logics, including quantified PITL (QPITL) and quantified propositional linear-time temporal logic (QPTL) without past-time. Our approach is therefore a definite advance over previous work which has appeared during the last roughly 40 years. In even broader terms, we believe that it provides evidence that ITL might play a fundamental and central role in the proof theory of omega-regular logics, and perhaps in other aspects of them. In particular, our ITL-based framework also provides a formal basis for the study of versions of temporal logic supporting memory, framing and multiple time granularities as well as a calculus for sequential and parallel composition based on Hoare triples having assertions expressed in temporal logic. In view of all of this, ITL might eventually be regarded as a unifying, canonical notation for exploring analytical and computational aspects of discrete, linear time systems as well as associated programming semantics and calculi.