- Specify with five properties, which you want to check against your automaton.
- Explain for each formula how this formula will be interpreted either as satisfied or as non satisfied.
- Give for every property reachability, safety, liveness, deadlock freeness an example, whether they are true in your model or not.

Assume that and construct a minimal execution graph for each of the following formulas which satisfies the following formulas:

Gerd Doeben-Henisch 2010-03-03