© 1996-2015


This course will give a not so short introduction to Interval Temporal Logic (ITL)

ITL is a

  • discrete, linear temporal logic
  • for both finite and infinite intervals (sequences of states) which includes
  • a basic construct for sequential composition and
  • an analog of Kleene star (regular expressions)
  • Combines temporal logic, automata and regular expressions
  • Modular reasoning about time (e.g., hardware, software, multimedia)
  • Flexible notation for discrete linear order
  • Analytical framework for going from infinite-time behaviour to finite-time behaviour.
  • Supports sequential operators found in programs, etc.
  • Compositionality with assumptions and commitments
  • Refinement to derive concrete programs from abstract specifications.
  • ITL with memory and framing can embed various kinds of imperative programs, including parallel ones.
  • Executable specifications and imperative subsets.
  • Temporal projection between different time granularities; enables imperative constructs for interleaved processes.
  • ITL helped influence Prof Mike Gordon, FRS to switch from LCF to HOL in his theorem proving tools. (E.g., see his article From LCF to HOL: A short history).
  • Hybrid systems: Duration Calculus (real and discrete time).
  • ITL is used to give semantics to Verilog (EPSRC project with Oxford University).
  • ITL is used in hardware/software codesign (EPSRC projects with University of Newcastle upon Tyne and Oxford University).
  • ITL is used for security and trust policies (DTC-DIF projects).
  • ITL used in the projects Safemos (UK) and ProCoS (EU).
  • Mexitl (Kent, Winnipeg) is based on ITL, Multimedia in Executable Interval Temporal Logic.
  • AnaTempura runtime verification tool uses executable subset of ITL.
  • Influenced Verisity Ltd.’s language temporal e (part of IEEE Standard 1647). Verisity acquired by Cadence Design Systems, Inc., a major supplier of electronic design tools and services.
  • Used in the KIV theorem prover (University of Augsburg, Germany) - e.g., for Statecharts, UML and medical protocols.
  • ITL with framing and temporal projection extensively studied by Duan and group (Xidian University, Xi’an, China).