# Symbolic Computation of Predecessors

In this question for computing the universal predecessors, I do not understand how in highlight 1: (p' XOR q') was omitted (it is not present in the next step)

and in highlight 2: p' was omitted.

+1 vote

Doubt 1: (p' xor q') is equivalent to !(p'<->q'), so when we multiply out, we get

(((p<->q) | (p' xor q')) & ((p<->q')|(p' xor q))&(p'<->q'))
<->
(
(p<->q) & ((p<->q')|(p' xor q))&(p'<->q')
|(p' xor q') & ((p<->q')|(p' xor q)) & (p'<->q')
)
<->
(p<->q) & ((p<->q')|(p' xor q))&(p'<->q')

Note that (p' xor q') & (...) & (p'<->q') is just false.

Doubt 2:

exists q'. (p<->q) & ((p<->q')|(p' xor q)) & (p'<->q')
<-> (p<->q) & ((p<->0)|(p' xor q)) & (p'<->0)
| (p<->q) & ((p<->1)|(p' xor q)) & (p'<->1)
<-> (p<->q) & (!p|(p' xor q)) & !p'
| (p<->q) & ( p|(p' xor q)) &  p'
<-> (p<->q) & (!p|(0 xor q)) & !p'
| (p<->q) & ( p|(1 xor q)) &  p'
<-> (p<->q) & (!p| q) & !p'
| (p<->q) & ( p|!q) &  p'

p' was omitted because of φ ∧ x ⇔ φ[x<-1] ∧ x and φ ∧ ¬x ⇔ φ[x<-0] ∧ x (see page 69 on the Chapter on transition systems where the symbolic computation of predecessors and successors is explained with this trick.

by (166k points)
selected by