# [Tool not accepting the answer] VRS Sheet 8 Q2 LTL Equivalence

----------------------------------------------------------------------------------------------------------------------------------

Q:-

S1=S1=[b WB [a WB c]]

S2=S2=[b SB [a WB c]]

Assumed that the alphabets is the set of variables that appear in the formulas

-------

When I check my LTL formulas in "LTL (Linear Temporal Logic) Tools", it gives me VALID answer but my answer is not being accepting by the exercise tool.

My answer: "1 ; G (!a & !b & c) ; G (a & !c) & G !b"

And my search queries in "LTL (Linear Temporal Logic) Tools" are:

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

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

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

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

Thank you.

reshown

Did you really try the above queries with the LTL tool? When I try it, then G (a & !c) & G !b -> [b WB [a WB c]] turns out not to be valid. A counterexample is of course a single path where always s&!b&!c holds so that G (a & !c) & G !b is satisfied on that path at the initial point of time. [a WB c] also holds at the initial point of time, since a holds there, but c does not. Therefore, [b WB [a WB c]] must be false, since it requires that [a WB c] must be false at the initial point of time.
by (117k points)
selected by