Exam 16.02.2022, Problem 8g) Natural Language to LTL

Question

Hello,

I have a question regarding the solution for Problem 8(g) of the exam from Feb. 2022 (2022.02.16.vrs.solutions.pdf):

Shouldn't the underlined part be  X( (a -> Ga) & (!a -> G(!a)) )  instead?
The underlined formula in the solution is equivalent to  X( (a -> Ga) & (!a -> !Ga) ), but if I understood it correctly, the latter subformula is not what we want, since we want to express that if a is false at that point in time, it should also always be false in the future (i.e. G(!a)).

Thanks in advance :)

Answer 1

Yes, I agree with you. We can even write more explicitly the following formula:

    G((!a & X a -> X G a) & (a & X !a -> X G !a))

The above is equivalent to your suggestion.