Syntax Propositional ITL

III.2 Syntax Propositional ITL

Propositional ITL [Slide 90]

Summary of the syntax of Propositional ITL:

Boolean values: true,false
Boolean state variables: P,Q,…
Boolean operators: ∧,∨,¬,⊃,≡
Temporal operators:

skip
(skip),

;

(chop),

(next),

(always),

(sometimes),

^∗

(chopstar),

…

Propositional ITL [Slide 91]

Syntax of Propositional ITL in BNF:

f ::=

true |Q |¬f | f₁ ∧ f₂ |skip |f₁ ; f₂ |f^∗

Derived ITL operators:

f	≜	skip ; f
f	≜	true ; f
f	≜	¬( ¬f)
…

2023-09-12

Contact | Home | ITL home | Course | Proofs | Algebra | FL

© 1996-2023