# LTL Equivalence (Globally & Eventually relation)

I have a problem with the following exercise:

S1=X b & G c
S2=G b & F c

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

I tried the following 2 formulas:

• !c&G(b)&X(c)
• G(b)&F(c)&!G(c)

The LTL Tool says that

• G(b)&F(c)&!G(c) -> G b & F c & !(X b & G c) is valid
• !c&G(b)&X(c) -> G B & F C & !(X B & G C) is valid as well.

However, the student portal gives me the following error: "Please check whether your LTL formula fulfill the requirements."

Which requirements do my formulars not fulfill?

I have the exact same problem
It would be too simple to allow !S1&S2 as one of the two formulas, but one your formulas is equivalent to that.

Very tricky. For your formulas phi1 and phi2, we can check that they are satisfiable, they are not equivalent and both imply !S1&S2. So, what is wrong here?

Read carefully the exercise problem. The formulas should satisfy

`phi[i] -> !S1&S2 `

but that should be strict, i.e., the formulas should **not** satisfy

`phi[i] <-> !S1&S2`

However, this is the case with your formula phi2.

by (142k points)
selected by
Thank you. I simply added "&c" in the second formula, therefore the Implication still holds but the formulas are no longer equivalent.

+1 vote