De Montfort University, UK
4pm Tuesday, 3rd November, 2009
Room 4.31/33, Informatics Forum
Discrete linear state-sequences provide a compellingly natural and flexible way to model many dynamic computational processes involving hardware or software. Over 50 years ago, the distinguished logicians Church and Tarski initiated the study of a fundamental and powerful class of decidable calculi for rigorously describing and analysing various basic aspects of discrete linear-time behaviour. The number of such formalisms has significantly grown to include many temporal logics, some of which are employed in industry, and even found in IEEE standards. They are intimately connected with regular languages, analogues for infinite words called omega-regular languages and the associated finite-state automata.
We describe a promising hierarchical approach for systematically analysing and relating such logics. Our framework is based on Interval Temporal Logic (ITL), a well-established, stable formalism first studied over 25 years ago. It offers a greatly simplified way to show axiomatic completeness for such logics and for some of them even suggests new improved axioms and inference rules. This is in itself a definite advance over previous work of the last roughly 40 years on axiomatic completeness which in contrast embedded complicated deductions involving nontrivial techniques such as the complementation of nondeterministic finite-state automata which recognise infinite words. Our presentation also offers intriguing evidence that Propositional ITL (PITL) might play a central role in the overall proof theory of this class of notations, and perhaps will eventually come to be regarded as the canonical propositional logic of linear, discrete time.
Furthermore, PITL also provides a starting point for decidable calculi which formalise memory, framing and multiple time granularities as well as for a calculus of sequential and parallel composition based on Hoare triples having assertions expressed in temporal logic. In view of all of this, ITL in the future might be recognised as more than just a unifying, canonical notation for exploring discrete linear time systems. It could also be seen as a key analytical formalism for investigating associated programming semantics and calculi as well as both regular and omega-regular languages.