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) | 
| …   | ||