[DOUBT] Translation of omega automaton to LO2

Question

I have a small doubt about the solution provided in the paper of 2022. During the conversion of FG(p XOR q), wouldn't there be an -> operator instead of &? Can you please tell me if the below equation would be right:

Comments

Why it got changed to implication?  In the formula of LO2 it is & operator I guess

Answer 1

Yes, you are right, that should be an implication, and it has now be fixed. Thank you for point out that mistake!

Comments

Thanks for the verification. Glad it was helpful!