QUESTION 1:
When an aircraft is in mid-flight, its wheels are retracted and brakes applied. When the aircraft comes to land, the wheels are deployed but the brakes remain in place. The brakes are released when the friction sensors on the wheels sense friction. Formalize these properties in LTL.
QUESTION 2:
This question is open-ended but a useful exercise to get a sense of how real-life model checking works. This scenario has a lot to do with recent news. An aircraft manufacturer introduces a new model of aircraft in which the center of gravity of the aircraft is moved closer to the front of the aircraft to achieve fuel efficiency. This causes the nose of the aircraft to tilt downwards during flight. Consequently, the aircraft avionics system is designed to continually lift the nose upward. This leads to settings where the pilot sometimes has to ”fight” the avionics system to take the aircraft’s nose downwards. The avionics is now being redesigned to prevent such situations. Write, in LTL, some of the properties that you might want to check against a state transition model of the new avionics system.
