Solutions for CTL Exercise (Nov. 4th)

[Eric Wohlstadter]

Here are the CTL answers, also I include a restatement of the
question, sometimes in different words than used by the original
questions, in case rephrasing the question helps. Where I say
something like "p is true", it is short for "a state where p is true",
and where I say "reach p", it is short for "reach a state where p is
true"

1. p & EF(q)
"p is true in the current state AND it is possible to reach q"

2. EF(p & EX(q))
"It is possible to reach a state where: p is true AND q is true in the
next state"

3. AG([p & EX(p)] -> EX[p & EF(q)])

"IF p is true in some state AND it is possible for p to be true the
next state,
THEN there is a path from the first state, which starts with p true in
the next state AND it is possible to reach q from there"

4. AG([p -> A(pUq)] and [not(p) -> AX(AX(EF(p)))])

"IF p THEN p until q
AND
IF not p THEN it must be possible to reach p after two steps"

5. AG(EF(p) -> [not(q) & not(r)])

"IF it is possible to reach p THEN q and r are both false"

6. AG(p -> A[(not(p) U q) and (not(p) U r)])

"IF p THEN on all following paths, (p is false until q) and (p is
false until r)"

7. EF(p & AG(q))

"It is possible to reach a state where p is true and q is always true
after that"

8. not(AG(AF(p)))

"It is not the case that p occurs infinitely often."

9. E(not(p) U q)

"There exists a path where p is false until q is true"