VRS Sheet 8 Q2 LTL Equivalence

Question

I solved this as per my understanding but the tool rejected the answer. Any hint would be appreciated. The same goes with question (c).

a) S1=[b WU [c WU a]]

S2=[b WU [c SU a]]

Answer: [b WU [c WU a]] -> [b WU [c SU a]]

=> G (!b & !a &c) // 1st

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

=> 1; G (!b & !a &c) ; (!a&!b&c) & X(!a&b&c) & G (!b & !a &c)

Answer 1

Please repeat the question of the exercise sheet so that also students of later semesters can understand what we are discussing here. The question is that for a given LTL formulas S1 and S2, we should construct two LTL formulas φ1 and φ2 that satisfy the following requirements:

1. φ1 and φ2 are not equivalent
2. φ1 and φ2 are both satisfiable
3. either φ1->S1&!S2 and φ2->S1&!S2 or φ1->!S1&S2 and φ2->!S1&S2are valid

For the given formulas S1=[b WU [c WU a]] and S2=[b WU [c SU a]], you believe that [b WU [c WU a]] -> [b WU [c SU a]] would be valid, but that is not true. A counterexample is a single path where always !a&!b&c holds which obviously satisfies S1 but not S2. Note that [c WU a] holds here at every point of time, so that [b WU [c WU a]] is true at time 0, but [c SU a] is always false, and since b is also always false, S2 is false at initial time.

The formulas you suggest as a solution are φ1=G(!b&!a&c) and φ2=(!a&!b&c) & X(!a&b&c) & G(!b&!a&c). Formula φ1 holds exactly on the counterexample that I discussed above, so that the following is indeed valid:

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

Also φ2->S1&!S2, i.e., the following formula is valid

(!a&!b&c) & X(!a&b&c) & G(!b&!a&c) -> [b WU [c WU a]] & ![b WU [c SU a]]

However, the above is valid since φ2 is not satisfiable: If G(!b&!a&c) holds at initial time, then also X(!b&!a&c) must hold which contradicts X(!a&b&c). 

I guess you mean (!a&!b&c) & X((!a&b&c) & G(!b&!a&c)) as formula φ2, right?

Comments

Hello, I am putting following answer in the tool as it is but I am getting parsing error:

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

According to my calculations, for case 2, no formulas exist. Why the tool is not processing my answer?

---

I think you should either enter a solution with case 1 or with case 2, but not both. So, simply try
1 ; G (!a&!b&c) ; (!a&!b&c) & X ((!a&b&c) & G (!b&!a&c))

---

It has been marked as incorrect. I do not know where I am going wrong. I have also verified it through the tool.

---

I have also tried this one as well.
1 ; G (!a&!b&c) ; (!a&!b&c) & X (!a&b&c) & G (!b&!a&c)

---

Well, the formula (!a&!b&c) & X ((!a&b&c) & G (!b&!a&c)) is also not satisfiable. Note that in the next point of time, we should have !a&b&c and also !b&!a&c. I guess what you really mean is (!a&!b&c) & X ((!a&b&c) & X G (!b&!a&c)), right?

---

Ys exactly, I solved that. Thanks for guiding.

For part C in which S1=G a <-> X b  and S2=  G a <-> F b

I have computed these but once again tool is raising parcing error,
1 ; G (a&!b&!c) ; G (a&!b&c)
2 ; G (!a&b&!c) ; G (a&!b&!c)

If I enter only one row then system flags incorrect answer. Any leads in this regard

---

Well, again either case 1 or case 2 should apply, not both. Checking your formulas, they are not equivalent and they are both satisfiable. With φ1=G(a&!b&!c) and φ2=G(a&!b&c), we neither have (G(a&!b&!c))->(G a <-> X b)&!(G a <-> F b) nor do we have (G(a&!b&!c))->!(G a <-> X b)&(G a <-> F b). Note that G(a&!b&!c) implies that G a is true, thus the formulas become (G(a&!b&!c))->(X b)&!(F b) and (G(a&!b&!c))->!(X b)&(F b). However, since G!b holds, both X b and F b are false, so that we get (G(a&!b&!c))->false and (G(a&!b&!c))->false. Hence, we these formulas, neither case 1 nor case 2 is given.

---

Thanks for the help. I found my mistake. I've updated my questions as per your instructions for other students.