Exercise 8.  

Let σ = σ₀σ₁σ₂σ₃

• 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))
• skip² ∧(skip ⊃ P)

Exercise 10.  

Give the informal semantics (picture) of following formulae:

• skip³ ∧ keep P ∧fin(¬P) ∧while P do (Q ∧skip)
• skip³ ∧ P ∧while P do (Q ∧skip)
• skip³ ∧keep(¬Q) ∧fin(Q) ∧repeat(P ∧skip)until Q
• skip³ ∧(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 formal semantics of the following formulae:

• P ∧ Q
• skip²
• skip ; 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

1.

●	●	●

2.

●	●
P	¬P

3.

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

4.

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