ITL
© 1996-2015







7 Syntax Propositional ITL

Syntax of Propositional ITL:

  • Boolean values: true,false
  • Boolean static variables: p,q,...
  • Boolean state variables: P,Q, ...
  • Boolean operators: ∧,∨,, ⊃, ≡
  • Temporal operators:
    skip   (skip),
;     (chop),
*     (chopstar),
C     (next),
!     (always),
      (sometim es),.....

Syntax of Propositional ITL in BNF:

f ::=  true|q|Q |f |f ∧ f |skip|f  ;f |f *
                   1   2      1   2

Derived ITL operators:

C f   =^  skip ;f
inf   =^  true ;false
finite  =^  inf
  f   =^  finite; f
! f   =^  (  f )
...