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.