LTL Equivalence (Globally & Eventually relation)

Question

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?

Comments

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.

Answer 1

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.

Comments

Thank you. I simply added "&c" in the second formula, therefore the Implication still holds but the formulas are no longer equivalent.