Exam 2020.02.19

Question

Could you please clarify, why this has been done here? 

A∃ ({p, q}, ¬q ∧ p, Φ1 ∧ Φ2, FG¬q ∨ FGp) 

A∃ ({q, p}, ¬q ∧ p, Φ1 ∧ Φ2, A∃ ({r}, ¬r, r0 ↔ (r ⇒ p | q), FG(¬r ∨ p)))

Can we do the operation like the below instead of the above one?

A∃ ({p, q}, ¬q ∧ p, Φ1 ∧ Φ2, FG[¬q ∨ p]) 

Answer 1

FGφ ∨ FGψ is not equivalent to FG(φ ∨ ψ), but we can reduce the disjunction using a new state variable as shown on slide 51 of the related chapter. 

Comments

FGϕ ∨ FGψ = A∃ ({q}, ¬q, q′ ↔ (q ⇒ ψ| ¬ϕ), FG[¬q ∨ ψ]) . Thanks for clarifying , Professor.