Temporal Logic

Question

I am not able to understand how to get the highlighted step from the 2nd step. I understood 1st and 2nd line but not 3rd line. How can we remove q all together from the automata?

Exam paper:Question 9 last part:  https://es.cs.uni-kl.de/teaching/vrs/exams/2015.10.15.vrs/2015.10.15.vrs.solutions.pdf

Answer 1

Have a look at the automaton that is replaced by FG p:

Only runs are accepted where once the green state is reached. Obviously, we may also demand that FG p should hold, right?

Comments

yes, right. I understood thank you. :D

---

One more doubt I have in the same problem.  p is input variable for second automata and s0, s1 are states and we define acceptance condition on states. So shouldn't we define acceptance condition on q? I am asking very basic question.

---

q is a state variable that defines the two states s0 and s1. Acceptance conditions are defined on states, right. But in symbolic descriptions, we do not work with explicit states like s0 and s1, and rather use formulas on the state variables as replacement of sets of states. So, it is fine to have acceptance conditions on the state variables. Note also that for the first automaton p is a state formula while p is an input for the second one.

---

ok. Got it. Thank you :)