Sheet 8 Exercise 1

Question

Hello,

my Exercise 1 of the current sheet is (almost) the same as the one from this week's solution PDF (https://es.cs.uni-kl.de/teaching/vrs/exercises/08-Solutions.pdf Page 10)

The only difference is - as you can see in the screenshot - that Case 1 and Case 2 are different. 
Do I need to do something differently from the solution in the solution pdf, because of the different Case 1 and Case 2, or does this make no difference? When I enter 
[c WU [a WU b]] ->  [c WU [a SU b]] in the teaching tool, I also get the same answer (always a) as the solution pdf.

If this is the correct answer, what exactly do I have to enter in the text field from the online exercise tool? Do I need to enter either a solution for 1 or a solution for 2? Or both at the same time?

This solution was wrong:
1 ; G (a) ; G (!b)
These  solutions were not accepted:

• 1 ; G (a) ; G (!b) ; G (!c)
• 1 ; G (a) ; G (!b) ; G (!c)
  2 ;
• 1 ; G (a) ; F (!b)
• 1 ; G (a & !b & !c)

I am not exactly sure how the solution needs to be entered. Especially since S2 has no counterexample (just like in the solution PDF). 

Answer 1

For given LTL formulas S1 and S2, you have to find two satisfiable formulas phi1 and phi2 which are not equivalent that one of the following holds:

    (1) phi1->S1&!S2 and phi2->S1&!S2
    (2) phi1->!S1&S2 and phi2->!S1&S2

To indicate which of the above cases you mean, you have to enter either one of the following two lines with the right formulas phi1 and phi2:

    1; phi1 ; phi2
    2; phi1 ; phi2

So, you have to give two nontrivial counterexamples to either S1->S2 or to S2->S1.

Now consider your particular task: Your formulas are S1 := [c WU [a WU b]] and S2 := [c WU [a SU b]].

Checking S2->S1, i.e., [c WU [a SU b]] -> [c WU [a WU b]] by the LTL prover shows that this implication is valid. Hence, !S1&S2 is unsatisfiable and we can therefore not use case 2. 

So, we have to find formulas phi1 and phi2 that satisfy phi1->S1&!S2 and phi2->S1&!S2. Checking S1->S2, i.e., [c WU [a WU b]] -> [c WU [a SU b]] with the tool shows us that this implication is not valid. 

You tried as an answer 1 ; G(a) ; G(!b) which was wrong. Why is that so? Well, check whether the following formulas are valid:

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

But none of them are valid! You have to find other formulas that will meet the requirements. If you look at the counterexample that is generated by the LTL prover, you can see that it is a path where (G(a&!b&!c)) holds. 

Hence, (G(a&!b&!c)) is such a candidate formula, while the two you tried do not meet the requirements. It is up to you to find a second one.