Exercise 3: CTL

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

Assume that $\Phi, \Psi \in L_{CTL}$ and construct a minimal execution graph for each of the following formulas which satisfies the following formulas:

1. $\textbf{E}\textbf{X} (\Phi \wedge \neg \Psi)$
2. $\textbf{E}\textbf{F} (\Phi \vee \Psi)$
3. $\textbf{E}\textbf{G} (\Phi \wedge \Psi)$
4. $\textbf{E} (\Phi \textbf{U} \Psi)$
5. $\textbf{A}\textbf{X} \Phi$
6. $\textbf{A}\textbf{F} \Phi$
7. $\textbf{A}\textbf{G} \Phi$
8. $\textbf{A} (\Phi \textbf{U} \Psi)$