© 1996-2019

2 Motivation

Motivation [Slide 2]

Temporal Logic:

  • Reasoning about behaviours, i.e., sequences (traces) of system states
  • Linear Temporal Logic (LTL):

    (Next), in the next state,

    (Always), all states in the behaviour,

    (Sometimes), exist a state in the behaviour

  • Interval Temporal Logic (ITL):

    skip, behaviour of two states,

    ; (Chop), fusion of two behaviours,

    (chopstar), fusion of a finite number of behaviours

  • Propositional Interval Temporal Logic (PITL):

    ITL with only propositional variables, i.e., Boolean values.

Motivation [Slide 3]

Verification tools for Propositional Interval Temporal (PITL):

  • Tempura, Ben Moszkowski, Roger Hale, 1985. Executable specification, testing
  • Lite, Shinji Kono, 1991. Tableau-based
  • ITL Library for interactive theorem prover PVS, Antonio Cau, 1997. Axioms via Higher-order Logic
  • AnaTempura, Antonio Cau, Shikun Zhou, 1999. Runtime verification, Tempura
  • DCVALID, Paritosh Pandya, 2000. MONA, decision procedure for WS1S
  • PITL2Mona, Rodolfo Gomez, 2004. MONA, decision procedure for WS1S
  • JavaLite, Shinji Kono, 2008. BDD, Tableau-based
  • PITL Library for automated theorem prover Prover9, Antonio Cau, 2008. Algebra, proof search

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