ITL
© 1996-2018







III.7 Exercises

Exercises [Slide 101]

Exercise 8.  

Let σ = σ0σ1σ2σ3
Give all prefix intervals of σ
Give all suffix intervals of σ
Give all sub-intervals of σ

Exercise 9.  

Give the informal semantics (picture) of following formulae:

empty P ((P Q) (¬P R))
empty ¬P ((P Q) (¬P R))
skip2 (skip P)

Exercise 10.  

Give the informal semantics (picture) of following formulae:

skip3 keep P fin(¬P) while P do (Q skip)
skip3 P while P do (Q skip)
skip3 keep(¬Q) fin(Q) repeat(P skip) until Q
skip3 (Q) repeat(P empty) until Q

Exercise 11.  

Give the informal semantics of the following formulae:

(skip ( P))
(skip ( P))
(skip ( P))

Exercise 12.  

Give the informal semantics of the following formulae:

(empty P)
(empty P)
(empty P)

Exercise 13.  

Give the informal semantics of the following formulae:

(more (P Q))
(more (P Q))
(more (P Q))

Exercise 14.  

Give for the following intervals their corresponding propositional ITL formulae

P
¬P
P, ¬Q
P, Q
P, ¬Q
P
P
P,¬Q

Exercise 15.  

Give an English description of the set intervals that correspond to the following propositional formulae

P ¬P skip
P empty
( P) ; Q
more P
more P
P fin P
P more halt Q
skip

Exercise 16.  

Given following informal specification give its corresponding propositional ITL formula

All intervals of up to length 10 where in the initial state the value of variable P is true and the value of variable Q is false. The value of P in each next state is the complemented value of P in the current state whereas the value of Q in each next state is the logical or of the value of P in the next state and the current value of Q.

Exercise 17.  

Determine which of the following formula is satisfiable or valid. Explain why.

(skip ; empty) (empty ; skip)
skip ; skip ; skip ; (P empty)
((P empty) ; f) (P f)
(true)
(true)







2018-02-25
Contact | Home | ITL home | Course | Proofs | Algebra | FL