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

Question

Would you please explain me the steps that I should do in this question?

I have no idea how to start!

What are Q and R in this question so that I can do the followings:

Answer 1

You can simplify !(a|a) to ¬a. It is the set Q₂ whose predecessors you want to compute.

((q' → p) <-> (o&q → a)) & p'

is the symbolic formula representing your relation R.

Let's simplify this formula a bit:

((¬q'  | p) <-> (¬o|¬q|a)) & p' = ((¬q'  | p) & (¬o|¬q|a) & p') | (¬(¬q'  | p) & ¬(¬o|¬q|a) & p')
=
¬q' & ¬o & p' |
¬q' & ¬q & p' |
¬q' & a & p' |
p & ¬o & p' |
p & ¬q & p' |
p & a & p' |
q'  & ¬p & o & q & ¬a & p'

Next, we plug that in to formula on slide 59 of the chapter on state transition systems, and simplify.

Comments

how do I check my answer using the tool (Symbolic Representation online tool). Could you please explain.

---

https://es.cs.uni-kl.de/tools/teaching/SymbolicStateTrans.html

Enter state variables (here p;q;a), input variables (here o), enter initial state formula (here p|q), enter transition relation (here ((next(q)→p)<->(o&q → a))&next(p)), enter state set (here ¬a), check computation goals (here existential and universal predecessors). Note that we moved input variable a to the state variables so that the tool can compute predecessors of a state set depending on variable a.

In the end, we get the formulas describing the two predecessor-sets. We can then use the propositional logic tools to check whether they are equal to the formulas we computed by hand.

---

i didnt understand this part. how do you come up with ((q' → p) <-> (o&q → a)) & p' to ((¬q'  | p) <-> (¬o|q|a)) & p' = ((¬q'  | p) & (¬o|q|a) & p') | (¬(¬q'  | p) & ¬(¬o|q|a) & p')?.  please explain.

---

Ooops. My bad. I dropped a negation. The first transformation was replacing A→B by ¬A|B (twice), The second one was replacing A<->B by A&B | ¬A&¬B.

---

no problem. i understand the second part but In your starting part in righthand of double implication side, you are taking (¬o|¬q|a)) & p' but in question it's (o&q → a)) & p'. is this a mistake as well or there's some rules to simplify it.

---

o&q → a = (o&q) → a = ¬(o&q) | a = (¬o | ¬q) | a = ¬o | ¬q | a

---

ok now it's clear. Thanks.