(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: