Invariants and Temporal Logic (28/4)

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)

Slides: EDAN15 week5 Invariants and Temporal Logic.pdf Download EDAN15 week5 Invariants and Temporal Logic.pdf