LTL question exercise 8 1c

Question

Q :  S3=[(G a) WU [c WU b]]

I came up with two counterexamples and I have checked with tool and both are Not Valid, but exercise is not accepting these answers.

1.  G(!a&!b&!c) -> [(G a) WU [c WU b]]

2. G !c & F b & !a -> [(G a) WU [c WU b]] 

Could you please guide me what am I doing wrong here ?

Answer 1

I don't see why you emphasize that your implication is not valid. Shouldn't it be valid in order to satisfy the third requirement of your task?

Comments

For the point "I don't see why you emphasize that your implication is not valid. Shouldn't it be valid in order to satisfy the third requirement of your task?"

I may have interpreted the statement wrongly in question i.e "That means find two different LTL formulas for ω-word sets that are non-empty, non-equal and both don't satisfy S3".
I thought I have to find two formulas for which S3 would be invalid.

Could you please explain this ?

---

So if you want to find a formula phi that does not satisfy some property (S3 in this example) you want to ensure that its negation does always hold, i.e. is valid. Thus, for a correct solution, our teaching tool should give you a "VALID" response when querying:
"phi -> !S3"
however querying "phi -> S3" and expecting a "NOT VALID" is not sufficient, as it it only states that there are cases where when having phi, S3 does not hold, while there may also still be cases where "phi -> S3" does in fact hold, which is not what you want to express as for those cases, your formula phi would actually satisfy the property S3. So again as a conclusion, if:
"phi -> !S3"
returns "VALID" as a result in our teaching tool, then you found a correct formula for the given requirements (at least if its not empty and also not equal to the other formula you need to find).

---

Thank you for this detailed explanation.
I understood the point.

I have 1 small query :
When solving LTL Equivalence question i.e "Q2 where we need to find two formulas that both satisfy S1 and not S2 or both satisfy S2 and not S1", so in this when validating the answer in tool we have to do below in order to know that our answer is correct :
For case 1 :
phi1 -> S1 (returns VALID)
phi1 -> !S2 (returns VALID)

phi2 -> S1 (returns VALID)
phi2 -> !S2 (returns VALID)

The above scenario means that my answer is correct and exercise should accept it as correct answer.

Is this correct ?

---

Provided that the formulas are entered correctly, yes.

I think the following should also do the job:
(phi1 | phi2 ) -> (S1 & !S2) valid

---

Thank you for the answer :)