Objectives:

- Practice writing CTL* properties
- Create minimal paths that satisfy properties
- Practice writing LTL properties
- Describe the difference in expressiveness between LTL, CTL, and CTL*

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.