LTL Equivalence (Before relation)

Question

I have a problem regarding the following exercise:

I'm trying to find 2 formulas which satisfy S1 but not S2.

Therefore, the formulas must imply ![b WB a] and !c.

I tried G(a & !b & !c) and G(!b & !c) & X(a).

In both formulas, [b WB a] is false since when a is true, b wasn't true before. Also, c is always false. Therefore those formulas should satisfy S1 but not S2. However, the online tool does not accept this as a correct solution. Where am I wrong?

Answer 1

I checked your two formulas and the second one is not correct. We can prove that

(G(a & !b & !c)) -> [[b WB a] WB c] & ![[b WB a] SB c]

is valid, but (G(!b & !c) & X(a)) -> [[b WB a] WB c] & ![[b WB a] SB c] is not valid. 

To find your formulas, I suggest to first disprove [[b WB a] WB c] -> [[b WB a] SB c] so that the tool gives you a counterexample that satisfies [[b WB a] WB c] & ![[b WB a] SB c]. When I do that, I obtain a single path that is described by your first formula G(a & !b & !c). 

To find the second formula, try a proof for !(G(a & !b & !c)) & [[b WB a] WB c] -> [[b WB a] SB c]. Since that is not valid, a counterexample will satisfy !(G(a & !b & !c)) & [[b WB a] WB c] & ![[b WB a] SB c] and will give you a second formula. 

Comments

Ok I think I understand why formula 2 is not valid. S2 might be true for G(!b & !c) & X(a).

We evaluate [b WB a] not just at the start, but for each "step" of the automata. And once a occured (since it just has to occur at least in the next state due to X(a)) [b WB a] might evaluate to true if a never appears again. And then [[b WB a] SB c] would be true.