Are the two LTL properties $GF(\psi_1 \land F\psi_2 )$ and $GF(\psi_2 \land F\psi_1 )$ equivalent?

cs.stackexchange https://cs.stackexchange.com/questions/106998

문제

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?

올바른 솔루션이 없습니다

라이센스 : CC-BY-SA ~와 함께 속성
제휴하지 않습니다 cs.stackexchange
scroll top