Objectives:

- Write temporal logic properties
- Master the semantics of temporal logic

**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)*