Summary of the syntax of Propositional ITL:
Temporal operators:
skip | (skip), |
; |
(chop), |
(next), |
|
(always), |
|
(sometimes), |
|
∗ |
(chopstar), |
… | |
Syntax of Propositional ITL in BNF:
f ::= | true |Q |¬f | f1 ∧ f2 |skip |f1 ; f2 |f∗ |
Derived ITL operators:
f |
≜ |
skip ; f |
f | ≜ | true ; f |
f | ≜ | ¬( ¬f) |
… | ||