Interval Temporal Logic

Antonio Cau and Ben Moszkowski

Pdf version of the ITL home page


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 [137]. Timing constraints are expressible and furthermore most imperative programming constructs can be viewed as formulas in a slightly modified version of ITL [128]. Tempura provides an executable framework for developing and experimenting with suitable ITL specifications. In addition, ITL and its mature executable subset Tempura [160] 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, Tempura has been applied to hardware simulation and other areas where timing is important.

1  News
     1.1  14-09-2023: Version 3.6 of (Ana)Tempura
     1.2  13-09-2023: Version 3.3 of the Isabelle ITL proof library
     1.3  12-09-2023: New layout of web pages

2  Finite Interval Temporal Logic
     2.1  Syntax
     2.2  Semantics
     2.3  Derived Constructs
     2.4  Propositional proof system
     2.5  First order proof system

3  Finite and Infinite Interval Temporal Logic
     3.1  Syntax
     3.2  Semantics
     3.3  Derived Constructs
     3.4  Propositional proof system
     3.5  First order proof system

4  Tools
     4.1  (Ana)Tempura
     4.2  FLCheck: Fusion Logic decision Procedure
     4.3  ITL library for Isabelle/HOL
     4.4  ITL Theorem Prover based on Prover9
     4.5  ITL Proof Checker based on PVS
     4.6  Automatic Verification of Interval Temporal Logic

5  ITL Related Publications
     5.1  Articles
     5.2  In Collections
     5.3  Conference Papers
     5.4  Books
     5.5  Theses
     5.6  Technical Reports

Contact | Home | ITL home | Course | Proofs | Algebra | FL
© 1996-2023