
 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 ﬁnite number of behaviours
 Propositional Interval Temporal Logic (PITL):
ITL with only propositional variables, i.e., Boolean values.
Motivation [Slide 3]
Veriﬁcation tools for Propositional Interval Temporal (PITL):
 Tempura, Ben Moszkowski, Roger Hale, 1985. Executable
speciﬁcation, testing
 Lite, Shinji Kono, 1991. Tableaubased
 ITL Library for interactive theorem prover PVS, Antonio Cau,
1997. Axioms via Higherorder Logic
 AnaTempura, Antonio Cau, Shikun Zhou, 1999. Runtime
veriﬁcation, Tempura
 DCVALID, Paritosh Pandya, 2000. MONA, decision procedure
for WS1S
 PITL2Mona, Rodolfo Gomez, 2004. MONA, decision procedure
for WS1S
 JavaLite, Shinji Kono, 2008. BDD, Tableaubased
 PITL Library for automated theorem prover Prover9, Antonio
Cau, 2008. Algebra, proof search
  