| | ### 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. Tableau-based
- ITL Library for interactive theorem prover PVS, Antonio Cau,
1997. Axioms via Higher-order 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, Tableau-based
- PITL Library for automated theorem prover Prover9, Antonio
Cau, 2008. Algebra, proof search
| | |