Give the informal semantics (picture) of following formulae:

empty∧P∧((P∧Q)∨(¬P∧R))

empty∧¬P∧((P∧Q)∨(¬P∧R))

skip^{2}∧(skip⊃P)

Exercise 10.

Give the informal semantics (picture) of following formulae:

skip^{3}∧keepP∧ﬁn(¬P)∧whilePdo(Q∧skip)

skip^{3}∧P∧whilePdo(Q∧skip)

skip^{3}∧keep(¬Q)∧ﬁn(Q)∧repeat(P∧skip)untilQ

skip^{3}∧(Q)∧repeat(P∧empty)untilQ

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 ITLformulae

⚫

⚫

⚫

⚫

⚫

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 thefollowing propositional formulae

P∧¬P∧skip

P∧empty

(P);Q

more∧P

more∧P

P∧ﬁnP

P∧more∧haltQ

skip^{∗}

Exercise 16.

Given following informal speciﬁcation give its correspondingpropositional ITL formula

All intervals of up to length 10 where in the initial state thevalue of variable P istrueand the value of variable Q isfalse. Thevalue of P in each next state is the complemented value of P inthe current state whereas the value of Q in each next state is thelogical or of the value of P in the next state and the current value ofQ.

Exercise 17.

Determine which of the following formula is satisﬁable or valid. Explainwhy.