Here you can ask questions and find or give answers to organizational, academic and other questions about studying computer science.

868 questions

986 answers


438 users

0 votes

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]

in # Study-Organisation (Master) by (1.1k points)

1 Answer

+1 vote
Best answer

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. 

by (139k points)
selected by
FGϕ ∨ FGψ = A∃ ({q}, ¬q, q′ ↔ (q ⇒ ψ| ¬ϕ), FG[¬q ∨ ψ]) . Thanks for clarifying , Professor.
Imprint | Privacy Policy