LTL Equivalence

Question

Can someone please explain, how to approach these questions without using the online tool? I understood the other variants of such questions with WU, SU, WB, SB, but where other Temporal operators come I don't understand how to find the formula to satisfy one and not others.

The given LTL formulas S1 and S2 are not equivalent.
Please construct two LTL formulas φ1φ1 and φ2φ2 that satisfy the following requirements:

• Lφ1≠Lφ2
• Lφi≠{}
• Case 1: Lφ1⊊LS1∧¬S2Lφ1⊊LS1∧¬S2 and Lφ2⊊LS1∧¬S2Lφ2⊊LS1∧¬S2
  or
  Case 2: Lφ1⊊L¬S1∧S2Lφ1⊊L¬S1∧S2 and Lφ2⊊L¬S1∧S2Lφ2⊊L¬S1∧S2

where LφiLφi represents a set of ωω-words that satisfy φiφi.

S1=S1=X c -> F a
S2=S2=F c -> X a

2) Why this solution  (!c & G b & G (!a) )is correct for [c WU [b WU a]]?

3) I am able to make one formula but not second one, is there any trick to generate second formula?

Answer 1

Well, this kind of question asks for your intuitive understanding of temporal logic formulas. You should first read and understand the formulas to then point out their differences.

In your example, you can first understand that S2 implies S1, which means that

    ((F c) -> (X a)) -> ((X c) -> (F a))

is valid. Why is that so? By propositional logic, (a->(b->c)) is equivalent to (a&b)->c, thus, the formula is equivalent to

    (X c) & ((F c) -> (X a)) -> (F a)

which is valid: if (X c) holds, then also (F c) holds, and by modus ponens, it then follows also that (X a) must hold, and that in turn implies (F a).

Hence, S2 implies S1 and we must therefore search for counterexamples for S1->S2, since there are no counterexamples for S2->S1. A counterexample for S1->S2 is an example for S1&!S2, thus an example for

    ((X c) -> (F a)) & (F c) & !(X a)

Hence, find an example where once c holds, a does not hold at the next point of time, and if c should hold at the next point of time, then a should hold at some point of time.

For example, you could use any path that satisfies

    c & (X !a) & (X !c)

since

    (c & (X !a) & (X !c)) -> ((X c) -> (F a)) & (F c) & !(X a)

But you can also make X c true which must then also make a true at least once, but not at the next point of time. For example, you can choose any path that satisfies

    (a & !c) & X(!a&c)

Question 2): If G(!a&b) holds, then we have always have [b WU a] and therefore also  [c WU [b WU a]] but it is not needed to demand that !c holds initially.

Question 3) There is no special trick, you just have to additionally make sure that your first formula is not equivalent to the second one.

Answer 2

1. Here, just go through the options of statisfying implications. You can either not satisfy the left side or both sides. Also consider that satisfying X y also satisfies F y. So if we satisfy S2, we have two options. We can not satisfy F c but then we also may not satisfy X c, so both S1 and S2 would be satisfied. Or we can try to satisfy both F c and X c but try to differ X a vs F a. That doesn't help to satisfy only S2, as satisfying X a already satisfies F a. Hence, we try to satisfy S1 but not S2. If we want to not satisfy S2, we need to satisfy F c and not X a. For satisfying S1, we can either not satisfy X c (so we satisfy c at any point except for the next one) or we can satisfy X c (which already satisfies F c as well), and satisfy F c (at any point but not the next one).
2. ¬c doesn't satisfy the left side of the outer until. So the outer until can only be satisfied by satisfying the right side in the first step. Also the right side of the outer until is an until. In particular, it is a weak until. This means it can be satisfied without satisfying the right side. Hence, G(¬a) is allowed if and only if the left side is satisfied forever, which is ensured by G b.
3. Which example are you talking about? For the first one, you already have two options. You need to not satisfy the second formula for sure. But the first one can be satisfied both by not satisfying the left side or both sides of the implications. Also, the F-quantifiers can be satisfied at any point (provided that the conditions of the X-quantifiers are respected). For example, the formula F a ∧ ¬ X a can be satisfied by all paths that satisfy a ∧ ¬ X a, or X X a ∧ ¬ X a, or a ∧ X G¬a, or a ∧ X (¬a ∧ G a) … and infinitely many other formulas.