Exercise 26.  

Give for each of the following intervals the corresponding Interval Temporal Logic formula

1.

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

2.

●	●	●	●
P	P	¬P	¬P

3.

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

4.

●	●	●	●
I = 1	I = 3	I = 9	I = 27

Exercise 27.  

Give an English description of the interval that correspond to each of the following Interval Temporal Logic formulae

1.

(halt Q) ∧skip⁴

2.

(P ∧skip² ∧fin(Q)) ; (¬P ∧skip ∧fin(Q))

3.

(( Q) ; (skip³ ∧halt P)) ∧skip⁵

4.

(skip³)^∗

Exercise 28.  

Give the informal semantics (picture) of following formulae:

• A = 0 ∧skip ∧ A := A + 1
• len(6)
• A = 0 ∧len(2) ∧ A ← A + 1
• len(4) ∧ A = 3 ∧ A gets A + 1
• len(3) ∧ A = 2 ∧stable A

Exercise 29.  

Given informal specification

• the system’s behaviour consists of only two states,
• in the initial state the variable Account is equal to 50 and
• in the next state it is increased by 100.

Give the corresponding ITL formula.

Exercise 30.  

Given the following informal specification

An interval where in the initial state the value of variable I is 6 and the value of variable Q is false. The value of I in each next state is decremented by 1 until the value of I reaches 0 whereas the value of Q in each next state is the negation of the value of Q in the current state.

1.

Give its corresponding Interval Temporal Logic formula.

2.

Give its corresponding semantics in pictorial form.

Exercise 31.  

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

• ((A + B) = (B + A))
• ∃A (skip ; (A = 0))
• ∃A (A = 0 ∧ A ← A + 1 ∧len(5))
• ∀A (IsOdd(A) ; skip)