My PhD research over thirty years ago at Stanford University introduced the formalism Interval Temporal Logic (ITL), originally intended for use in Computer Hardware Verification. I subsequently showed how ITL could serve as the basis of a Programming Language for Executable Specifications and additionally as a framework for Compositional Reasoning about Concurrency. I have also done work on Complete Axiom Systems for versions of ITL and investigated Hierarchical Connections between it and other temporal logics. My recent work, which builds on research over the last two decades, concerns new compositional properties of ITL and associated techniques for Time Reversal. These involve remarkably simple mathematics and are also relevant to some other standard temporal logics, yet were apparently not known until now. In hindsight, the core ITL formalism has changed rather little since the time of my PhD dissertation, but the body of results concerning its theory and application have continued to expand, sometimes in quite surprising ways!
Here is a link to more information about ITL: http://www.tech.dmu.ac.uk/STRL/ITL/
Almost since its inception, ITL has inspired and influenced others and been used and adapted in research undertaken around the world. This process has in turn also helped contribute to a greater understanding about ITL itself. Below is a list of various projects:
HOL interactive theorem prover, originally developed by Professor M. C. J. Gordon, FRS.
Provable Correct Systems (ProCoS) European research projects headed by Prof Sir C. A. R. Hoare, FRS. A central formalism in ProCoS was the Duration Calculus, a real-time/hybrid variant of ITL developed by Prof Zhou Chaochen (previously Director of UNU-IIST in Macau, and now a member of the Chinese Academy of Sciences) and others.
IEEE Standard 1647 (published in 2006 and revised in 2008, with a further revision in the works) for the Functional Verification Language 'e'. This includes the assertion language temporal 'e', which has been influenced by Interval Temporal Logic and the Tempura programming language based on it.
MetateM, a framework for executable temporal formulas developed by Profs H. Barringer, M. Fisher, D. Gabbay and others.
ITL-based formalisation of Security Requirements and Access Control Policies by A. Cau, H. Janicke, F. Siewe and H. Zedan at DMU. Some of this research has been funded through the Data Information Fusion Defence Technology Centre (DIF DTC), which was headed, on behalf of the UK Ministry of Defence (MOD), by General Dynamics UK. It was established to form a research community of excellence in the field of data and information fusion. De Montfort University was a member of the consortium and so were BT, QinetiQ, Imperial College and the Universities of Bristol, Cardiff, Cambridge, Southampton, Surrey and Cranfield.
The KIV interactive theorem prover at the University of Augsburg, Germany. Applications involving ITL include showing the correctness of the following:
- Lock-free algorithms using rely-guarantee conditions
- Safety critical systems represented with Statecharts.
Projection Temporal Logic, an ITL-based notation investigated by Prof Z Duan and his group at Xidian University, Xi'an, China for reasoning about concurrent programs.
Three recent textbooks about temporal logic include material on ITL and other research influenced by it:
Real-Time Systems: Formal Specification and Automatic Verification.
E.-R. Olderog and H. Dierks, Cambridge University Press, 2008.
Temporal Logic and State Systems.
F. Kröger and S. Merz, Springer, 2008.
An Introduction to Practical Formal Methods Using Temporal Logic.
M. Fisher, John Wiley & Sons, Ltd., 2011.
The first of these extensively uses the Duration Calculus as the core logical formalism. Its co-author Prof. E.-R. Olderog is a 1994 recipient of the Leibniz Prize of the German Research Foundation (DFG) ("The highest honour awarded in German research") and also a member of Academia Europaea.