Chapter 2 of the course text.

1. (4 points) For each of the following properties: label as either safety or liveness, express in a CTL* formula, and create a minimal label trace to satisfy written formula.

• The number of items in a buffer may not exceed n
• If a process reaches a location li just before a critical section, it should not be blocked forever
• Clients may not retain resources forever
• It is always cloudy before it rains

2. (1 points) Express the following property in LTL (the '!' operator is a logical not):

the transition from !p to p will happen at most once

3. (1 points) Express the following property in LTL:

there are infinitely many transitions from !p to p (and vice versa)

4. (3 points) Express the following property in LTL using r, y, g as atomic propositions denoting the states of the traffic light (r = red, y = yellow, g = green):

The lights of a traffic signal light in the following periodic sequence: red, yellow, green, red, yellow, green,… and only one light is on at any given time, starting with red. You cannot make any assumptions on how long a light is on other than it will be on for a finite length of time.

5. (3 points) Express the following property in LTL:

if q holds in a state si and r holds in some subsequent state (sj , j > i) then p must not hold in any state sk in between si and sj (i < k < j , where j is the first such subsequent state)

6. (5 points) The CTL formula AF (AG p) is stronger than the LTL formula FG p meaning that a particular Kripke structure may model FG p but not AF (AG p). Draw such a Kripke structure and explain why that Kripke structure does not satisfy the CTL formula. Also prove that if a system satisfies the CTL formula, it must also satisfy the LTL formula. In what situation might you want to use the stronger formula (finding bugs or verifying correctness)? Hint: there are only three states in the Kripke structure.

7. (5 points) The LTL formula GF p is stronger than the CTL formula AG (EF p) meaning a Kripke structure may model AG (EF p) but not model GF p. Draw such a Kripke structure and explain why that Kripke structure does not satisfy the LTL formula. Also prove that if a system satisfies the LTL formula, it must also satisfy the CTL formula. Hint: there are only two states in the Kripke structure.

8. (3 points) Explain why the CTL* formula E(GF p) is not equivalent to either of the CTL formulas EG(EF p) and EG(AF p). For each pair of (CTL*, CTL) formula, state which property is stronger, and draw a Kripke structure that satisfies the weaker property but not the stronger property.

9. (3 points) Is [(EF p) || (EF q)] equivalent to EF(p || q) where the '||' operator is logical OR? Justify your answer.

10. (3 points) Is [(AF p) || (AF q)] equivalent to AF(p || q)? Justify your answer.