Are the two LTL properties $GF(\psi_1 \land F\psi_2 )$ and $GF(\psi_2 \land F\psi_1 )$ equivalent?
-
05-11-2019 - |
Question
Is $GF(\psi_1 \land F\psi_2 )$ equivalent to the property $GF(\psi_2 \land F\psi_1 )$?
Attempt:
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?
No correct solution
Licensed under: CC-BY-SA with attribution
Not affiliated with cs.stackexchange