| | 2
Motivation
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): , 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
| | |