Symbolic Computation of Predecessor States (exercise sheet 5 question 2)

Question

Consider the following symbolic representation of a FSM: A=(2Vin,2Vout,φI,2Vstate,φR)A=(2Vin,2Vout,φI,2Vstate,φR), where Vin={a}Vin={a}, Vout={o}Vout={o}, Vstate={p,q}Vstate={p,q}, φI=p∨qφI=p∨q, φR=φR=!((next(q)->p)<->(o&q->a))&next(p)

a) Compute the existential predecessors of !(a|a) for the corresponding Kripke structure of the FSM.

b) Compute the universal predecessors of !(a|a) for the corresponding Kripke structure of the FSM.

for this question as far as I understood, we need to first create the Kripke out of FSM. But what are the next steps?

Here I have the Kripke (if I calculated it correctly). What should I do next?

Answer 1

Computing the Kripke structure is already a good start!

The next step would be simplifying the formula to ¬a.

After that, you take the formulas for existential and universal predecessors, and plug in the formula ¬a, and the transition relation. Then you simplify the formula.

Comments

how can I get the transition relation?

---

and also what should I do with this kripke structure that I created?

---

in page 6 of the solution file we have:
Let the transition relation R be described by ψ R = (p` ↔ q) ∨ a.
Let the set Q be described by φ Q = ¬p

in our case (exercise sheet 5 question 2) Q = !a. But what is R and how can I get it from the kripke structure that I created?