Sheet 8 Question 2

Question

I have a question according to Sheet 8, Question 2 (b) - find 2 LTL counter-examples. 

For (b) it's:  S = [c WB [b WB a]]. The same example in exercise explanation, I understand how it works, but before it, I tried to solve by myself and I had the next intuition:

S = c WB [b WB a] = c WB [b SB a | G (!a)] = c SB [b SB a | G (!a)] | G(![b SB a | G (!a)]) - by definition of WB. Let's re-write it with abbreviation \psi = b SB a | G (!a):

S* = [c SB \psi] | [G (!\psi)]. I see here two formulas that correspond to !S:

1) G (!c) & G(\psi) - that breaks SB by definition (a SB b = !b U (a & !b)) and G (!\psi) as a consequence. One can re-write it as: G (!c & \psi)

2) \psi U c - breaks S* in the same way as 1).

I tried to submit the next solution: G(!c & ((b SB a) | G(!a))); [(b SB a) | G(!a)] U c and unfortunately parsing error arised. Could you please explain where I'm wrong?

Answer 1

The syntax of the binary temporal operators always requires square brackets (see https://es.cs.uni-kl.de/tools/teaching/QuartzRef.pdf).

Hence, using the correct syntax your thoughts are as follows with psi := [b SB a] | G !a 

    S = [c WB [b WB a]] 
      = [c WB [b SB a] | G !a] 
      = [c SB [b SB a] | G !a] | G!([b SB a] | G !a)
      = [c SB psi] | G!psi 

Now you claim that the following is valid (which is true):

    (G(!c&psi)) -> !([c SB psi] | G!psi)

which leads to your first formula G(!c&([b SB a] | G !a)).

Second, you use [c SB psi] = [!psi SU c & !psi] (which is right) and you claim that the following holds:

    [psi SU c] -> !([c SB psi] | G!psi)

which is not correct (I don't see why you think so). However, you may argue that

    !([c SB psi] | G!psi)
    = ![c SB psi] & !G!psi
    = [(!c) WU psi] & F psi
    = [(!c) SU psi]

and hence, you could use [(!c) WU psi] to prove

    [(!c) SU psi] -> !([c SB psi] | G!psi)

I guess that was what you wanted. 

However, also that will not be accepted by our clever tool, since even the following holds:

    [(!c) SU psi] <-> !([c SB psi] | G!psi)

Note that the implication must be a strict one (that was the main reason why the requirements were stated in terms of sets where we have a strict inclusion operator).  Hence, be careful with just doing equivalence transformations of the formulas.

Answer 2

That strongly depends on your implicit brackets.

If you claim  [b WB a] = [b SB a | G (!a)] and mean by it  [b WB a] = [b SB a] | G (!a), then you are right. If you mean  [b WB a] = [b SB (a | G (!a))], then you aren't right. A path satisfying b at some point but never a would satisfy the original formula  [b WB a] but not [b SB (a | G (!a))] as G(¬b) and hence also (a | G(¬b)) would be satisfied in the first step.

1. Assuming, your [¬b U (a & ¬b)] is [¬b SU (a & ¬b)].
2. Counterexample: c in the first step, never \psi. Then both [\psi SU c] and [\psi WU c] are satisfied but also [c SB \psi, G ¬\psi, and [c WB \psi] are satisfied.

Answer 3

Maybe here is a strategy that you had in mind: We unroll the temporal logic operator and create a DNF of the rest, then we negate that and pick the one or the other conjunct. That can give us quickly a couple of counterexamples.

For example, the given formula [c WB [b WB a]] will be converted as follows (note that [phi WB psi] = !psi & (phi | X[phi WB psi]):

    ![c WB [b WB a]]
    = !(![b WB a] & (c | X[c WB [b WB a]]))
    = !(!(!a & (b | X[b WB a])) & (c | X[c WB [b WB a]]))
    = !a&b | !a&X[b WB a] | !c&!X[c WB [b WB a]]

The final step requires some propositional logic simplifications, you may use whatever propositional logic tool to check that. Thus, we now have the following counterexamples:

1. (!a&b) -> ![c WB [b WB a]]
2. (!a&X[b WB a]) -> ![c WB [b WB a]]    
3. (!c&!X[c WB [b WB a]]) -> ![c WB [b WB a]]

Comments

Thank you! The best strategy for this task.