A Unifying Analytical Framework for Discrete Linear Time

Add to your list(s) Download to your calendar using vCal

• Ben Moszkowski, De Montfort University, Leicester
• Thursday 21 January 2010, 16:00-17:00
• UG40 Computer Science.

If you have a question about this talk, please contact Paul Levy.

Joint Theory/Departmental Seminar

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 these logics and establishing axiomatic completeness. Our framework is based on Interval Temporal Logic (ITL), a well- established, stable formalism first studied over 25 years ago. Previous proofs of axiomatic completeness developed over approximately 40 years for the hardest logics contained deductions involving explicit embeddings of nontrivial techniques such as the complementation of nondeterministic finite-state automata which recognise infinite words. Our greatly simplified approach avoids the need to encode these automata and techniques in logic. Instead, it just applies some standard results from the 60s and 70s which can be understood without any knowledge of automata for infinite words! In addition, it suggests new improved axioms and inference rules for some of the logics.

Our work also offers intriguing evidence that Propositional ITL (PITL) might play a central role in the overall proof theory of the class of decidable notations for discrete linear time, even for less succinct logics with lower computational complexity. Therefore PITL could eventually be seen as the canonical propositional logic for this model of time. Furthermore, PITL provides a starting point for less explored decidable calculi which formalise memory, framing and multiple time granularities as well as for a calculus of sequential and parallel composition based on nestable Hoare triples having assertions expressed in temporal logic. Potential applications include the Rely-Guarantee paradigm and some kinds of Separation Logic. This all suggests that ITL could serve as the basis for a “logical physics” of discrete linear time. Consequently, ITL might come to be regarded as a key analytical formalism for investigating programming semantics and calculi based on this model of time.

This talk is part of the Theoretical computer science seminar series.

This talk is included in these lists:

• Computer Science Departmental Series
• Computer Science Distinguished Seminars
• Theoretical computer science seminar
• UG40 Computer Science
• computer sience

Note that ex-directory lists are not shown.