© 1996-2016

Interval Temporal Logic
Antonio Cau and Ben Moszkowski

June 7, 2016


Interval Temporal Logic (ITL) is a flexible notation for both propositional and first-order reasoning about periods of time found in descriptions of hardware and software systems. Unlike most temporal logics, ITL can handle both sequential and parallel composition and offers powerful and extensible specification and proof techniques for reasoning about properties involving safety, liveness and projected time[124]. Timing constraints are expressible and furthermore most imperative programming constructs can be viewed as formulas in a slightly modified version of ITL [115]. Tempura provides an executable framework for developing and experimenting with suitable ITL specifications. In addition, ITL and its mature executable subset Tempura [147] have been extensively used to specify the properties of real-time systems where the primitive circuits can directly be represented by a set of simple temporal formulae. In addition, various researchers have applied Tempura to hardware simulation and other areas where timing is important.

1  Syntax

2  Semantics

3  Derived Constructs

4  Propositional proof system

5  First order proof system

6  Tools
     6.1  (Ana)Tempura
     6.2  ITL Theorem Prover based on Prover9
     6.3  FLCheck: Fusion Logic decision Procedure
     6.4  ITL Proof Checker based on PVS
     6.5  Automatic Verification of Interval Temporal Logic

7  Tempura Book

8  ITL Related Publications
     8.1  Articles
     8.2  In Collections
     8.3  Conference Papers
     8.4  Books
     8.5  Theses
     8.6  Technical Reports