Is $GF(\psi_1 \land F\psi_2 )$ equivalent to the property $GF(\psi_2 \land F\psi_1 )$?


In the first property each state must eventually see $\psi_1$ and $\psi_2$, in the second property as well each state must eventually see $\psi_1$ and $\psi_2$, as such the two properties must be equivalent. Is this correct?


1 Answer 1


You are right, but you should prove it. Here's a proof sketch:

Proof setup:

Suppose that $GF(\psi_1 \land F\psi_2)$ is true and assume towards a contradiction that $\neg GF(F\psi_1 \land \psi_2)$.


Then there exists a state $s_1$ in which $\neg F(F\psi_1 \land \psi_2)$, which means that every state $s_2 > s_1$ has $\neg(F\psi_1 \land \psi_2)$, which means that for every state $s_2$, either $\neg F\psi_1$ or $\neg \psi_2$.


But since $GF(\psi_1 \land F\psi_2)$, there exists a state $s_3 > s_2$ such that $s_3 \vDash \psi_1$ and a state $s_3 > s_2'$ such that $s_3' \vDash \psi_2$, which is a contradiction.

The other direction is identical.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.