### III.7 Exercises

#### Exercises [Slide 101]

Exercise 8.

 Let σ = σ0σ1σ2σ3 Give all preﬁx intervals of σ Give all suﬃx 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 ∧ﬁn(¬P) ∧while P do (Q ∧skip) skip3 ∧P ∧while P do (Q ∧skip) skip3 ∧keep(¬Q) ∧ﬁn(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 ∧ﬁn P P ∧more ∧halt Q skip∗

Exercise 16.

Given following informal speciﬁcation 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 satisﬁable or valid. Explain why.

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

 2018-03-10 Contact | Home | ITL home | Course | Proofs | Algebra | FL