EDAN15 week5 Invariants and Temporal Logic.pdf