Chapters 1, 2, 3, and 9 in the course text.

1. (6 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.
   1. X a
   2. XXX a
   3. [] b
   4. []<>a
   5. [](b U a)
   6. <>(b U a)
2. (4 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:
   1. Any door on any floor is never open when the elevator is not present
   2. A requested floor will be served eventually
   3. The elevator repeatedly returns to floor 0
   4. When the top floor is requested, the elevator serves it immediately and does not stop on any floor on the way up
3. (5 points) Which equivalences are true (justify your answer with a proof or counter-example)
   1. []f → <>g ⇔ f U (g \/ !f)
   2. X <> f1 ⇔ <> X f1
   3. (f U g) U g ⇔ f U g
   4. [] f /\ X <> f ⇔ []f
   5. <> f /\ X []f ⇔ <>f
4. (2 points) Add a fairness constraint to your Promela model of dining philosophers and use Spin to verify the same property from Homework 3: f = [] (fork1/2 –> <> !fork1/2). The fairness constraint cannot be the same as the property being verified. The spin verification should pass now where before it failed. Tips on Spin installation and basics are found in the Tools page.
5. (6 points) Write a Promela model of the elevator system in Problem 2, and very each of your properties on that system. Submit the Promela model and the verification results for your answer to this question.
6. (4 points) Consider the Kripke structure on page 26 of the course text for the mutual exclusion algorithm. Use CTL model checking to verify AG (turn = 1 → AF turn = 0) subject to the fairness constraint $P = \{s \mid l_0 \in \mathit{Label}(s) \wedge l_1 \in \mathit{Label}(s)\}$. Be sure to show the states that receive each label. Remember you need to convert the formula to only use EG, EF, EX, and boolean operations.