Invariants and Temporal Logic (3/5)

This part offers a base for reasoning about models; the formalisms presented here allow you to specify and work with properties of models in a way that is less error prone than using textual specifications.

Read chapter 13 of the textbook to understand the following concepts:

• invariants (13.1)
• execution trace for an FSM (p362, for more details see 3.6)
• propositions and formulas in Linear Temporal Logic (13.2.1, 13.2.2)
  • G operator (globally)
  • F operator (finally)
  • X operator (next state)
  • U operator (until)
• using LTL formulas (read the examples in 13.2.3)