© 1996-2015

2 Motivation

Temporal Logic:

  • Reasoning about behaviours, i.e., sequences (traces) of system states
  • Linear Temporal Logic (LTL): C (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.

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