LTL Equivalence

Question

By considering below:

I have submitted following answer, it displayed 

"Please check whether your LTL formula fulfill the requirements" 

but I already tried to fulfill the requirements. Which part I have done wrongly? 

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

Thanks in advance.

Answer 1

Case 2 (which you have chosen) means that you have to find formulas that imply !S1&S2, which is possible since S2->S1 is not valid. So, you have to find formulas that imply that !S1&S2 holds. Case 1 cannot be chosen, since S1->S2 is valid.

The second formula that you have, i.e., (!a&!b&!c) & G(X(!a&!b&c)) seems to be okay, but the first formula you have is false (I mean it is equivalent to false and therefore not allowed as a solution).

Comments

Thanks for clarification. I have checked as below in teaching tools:

[phi1] => G((!a&!b&c)& X(!a&b&c)) -> [[b SB a] WB c]& ![[b WB a] WB c] is valid.

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

In this case, [phi1] is OK and I must find another to replace with [phi2] for CASE1 right?

Thanks.

---

No, phi1 is the trouble maker. It is equivalent to false and that one must therefore be replaced. I think phi2 is fine.

---

I have the same question but not able to understand why phi2 is satisfying s2= [[b WB a] WB c]. Because if next time b and a becomes false and c becomes true then it doesn't satisfy even weak before condition. Could anyone help me on this where i am going wrong?
Thanks in advance.

---

Okay, let's clarify. We have the formulas S1 := [[b SB a] WB c] and S2 := [[b WB a] WB c]. Using the LTL prover, we find out that S1->S2 holds, but S2->S1 does not hold. For the latter, we obtain a counterexample that demonstrates that !S1&S2, i.e., that ![[b SB a] WB c] & [[b WB a] WB c] holds.

The counterexample has initially all variables false, and then a self-loop in a state where !a&!b&c holds. Hence, if [alpha WB c] should hold initially for some formula alpha, it must be the case that alpha must hold initially, since at the next point of time already c holds, and it is therefore too late for alpha. Initially, we have [b WB a] since a and b are always false, but we do not have [b SB a] since the strong before demands that b eventually holds which is however not the case.

Looking at the counterexample, I think a suitable phi1 should be (!a&!b&!c) & X G(!a&!b&c). We can also check that (!a&!b&!c) & X G(!a&!b&c) -> ![[b SB a] WB c] & [[b WB a] WB c] holds.

The formula phi1 that has been used above, i.e., G((!a&!b&c)& X(!a&b&c)) contradicts itself, since it says in particular that b should be false at all points of time, and b should hold at all points of time t>0 which is impossible. Thus, that phi1 is equivalent to false, and that is the reason why you can also prove phi1->S1&!S2 with it (which is equivalent to false->false). The student portal will however not accept that solution since it will check that your formulas phi1 and phi2 are not equivalent to false.

Finally, let's consider your phi2 := (!a&!b&!c) & G X(!a&!b&c) which describes the counterexample discussed above. You say that (!a&!b&!c) & G(X(!a&!b&c))-> [[b SB a] WB c]& ![[b WB a] WB c] is not valid which is true, but we have to check that (!a&!b&!c) & G(X(!a&!b&c))-> ![[b SB a] WB c] & [[b WB a] WB c] which is true. Note that we have to find examples for !S1&S2 since there are no examples for S1&!S2 (since we checked that S1->S2 holds).

Hence, you proved phi1->S1&!S2 with a formula phi1 equivalent to false (which is pointless), and could not prove phi2->S1&!S2 since the latter cannot be proved with a formula different to false. Instead, you should prove phi1->!S1&S2 and phi2->!S1&S2 which will work for your phi2. It does also work for your phi1, but just because it is false and that is not allowed.

Still confused?

---

Thank you so much for explaining it elaborately. If I understood it properly, it means that phi1->!s1&s2 where phi1 = (!a&!b&!c) & X G(!a&!b&c) holds because [b WB a] is true when all the variable are false initially but [b SB c] is not true since it demands that b should atleast hold. And, then at next time state there is self loop for c, which means c holds eventually and thus making [[b SB a] WB c] false because initially [b SB a] was false and it's too late for it to become true?.

---

Almost. In general [x SB y] holds on a path if x holds before y holds. Thus, there must be a prefix (maybe of length 0) where x=y=0 holds, and then there must be a point of time where x=1 and y=0 holds. In addition to that, [x WB y] also holds if both x=y=0 holds all the time.

Thus in the model where a=b=c=0 holds for t=0 and then a=b=0 holds always, we have [b WB a] holds at t=0 (but also for any time t), but [b SB a] does not hold at t=0 and neither does it hold at any other point of time (since b never becomes true).

Hence, we can replace [b WB a] by 1 and [b SB a] by 1, and can now consider the formulas [1 WB c] and [0 WB c]. Since c=0 initially, [1 WB c] holds (it is actually equivalent to !c), and [0 WB c] is false (it is equivalent to G!c).