© 1996-2019


Interval Temporal Logic
Antonio Cau and Ben Moszkowski

Abstract

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 [129]. Timing constraints are expressible and furthermore most imperative programming constructs can be viewed as formulas in a slightly modified version of ITL [120]. Tempura provides an executable framework for developing and experimenting with suitable ITL specifications. In addition, ITL and its mature executable subset Tempura [152] 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  Finite Interval Temporal Logic
     1.1  Syntax
     1.2  Semantics
     1.3  Derived Constructs
     1.4  Propositional proof system
     1.5  First order proof system

2  Finite and Infinite 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  Tools
     3.1  (Ana)Tempura
     3.2  FLCheck: Fusion Logic decision Procedure
     3.3  ITL library for Isabelle/HOL
     3.4  ITL Theorem Prover based on Prover9
     3.5  ITL Proof Checker based on PVS
     3.6  Automatic Verification of Interval Temporal Logic

4  ITL Related Publications
     4.1  Articles
     4.2  In Collections
     4.3  Conference Papers
     4.4  Books
     4.5  Theses
     4.6  Technical Reports








2019-01-03
Contact | Home | ITL home | Course | Proofs | Algebra | FL