LTL Equivalence - answer not accepted

Question

S1=[b SB [a WB c]]

S2=[b WB [a WB c]]

My solution is:

2 ; G (!b & !a &c) ; c & X (!c & a) & G (!b & !a)

I checked it with the tool and both formulas are valid but my solution is not accepted in the exercise system.

Answer 1

Case 2 means that !S1&S2 will be implied, but we have S1->S2, i.e., [b SB [a WB c]] -> [b WB [a WB c]] is valid. Hence, you should better go for case 1.

For case 1,  G (!b & !a &c) is good.

Your second formula is however equivalent to false: G(!b&!a) contradicts to X a.

Comments

Case 2 was the case to go.

I came up with the simple solution:  2 ; G (!b & !a &c) ; G (!b & a &c)

---

Yes, you are right. Case 2 means !S1&S2 which can be satisfied since S2->S1 is not valid. Above, I wrote that S1->S2 is valid (which is true), but that means that we should go for case 2 as you did.