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

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=pqφ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?

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.
by (25.6k points)
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?