1. (12 points) For the transition system, which states satisfy the formulas. L(s1) = {a}. L(s2) = {a}. L(s3) = {a,b}. L(s4) = {b}. s1 → s2. s2 → s3. s3 → s1. s4 → s2. s3 and s4 are initial states.

• A(X a)
• A(XXX a)
• A([] b)
• A([]<>a)
• A([](b U a))
• A(<>(b U a))

Hint: consider each state as the starting state for the formula.

2. (16 points) This problem is Exercise 5.5 in Principles of Model Checking (page 321 of the PDF document), consider an elevator system that services N > 0 floors numbered 0 through N-1. There is an elevator door at each floor with a call-button and an indicator light that signals whether or not the elevator has been called. For simplicity, consider N=4. Present a set of atomic propositions-try to minimize that set-that are needed to describe the following properties of the elevator as LTL formulae and give the LTL formulae:

• Any door on any floor is never open when the elevator is not present
• A requested floor will be served eventually
• The elevator repeatedly returns to floor 0
• When the top floor is requested, the elevator serves it immediately and does not stop on any floor on the way up

3. (16 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

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

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

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

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

6. (8 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.

7. (5 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)