© 1996-2018

I.2 Features of ITL

Features of ITL [Slide 12]

  • 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.

Features of ITL [Slide 13]

  • 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.

Contact | Home | ITL home | Course | Proofs | Algebra | FL