Sheet 8 Exercise 1 c)

Question

Hello,

I have trouble with the c) subpoint of the first question in exercise sheet 8. 

I am given the following two formulas:

S1=S1=X b & G c
S2=S2=G b & F c

The way I reason about it is that I need to find two formulas that are valid for either 

1.  !(X b & G c) & G b & F c  or
2. X b & G c & !(G b & F c).

 I managed to come up with the following two formulas: 

• G (b & [c SB b]) ; G (b & [c WB b])

that satisfy 1. (according to the tool). Now if I enter this as an answer in the sheet, I get the following error: "Please check whether your LTL formula fulfill the requirements". What exactly are the requirements? Are we not allowed to use S/WB, S/WU... in our solutions?

Thank you!

Answer 1

There are a couple of requirements given in the exercise. For given formulas S1 and S2, you have to find formulas phi1 and phi2 such that 

1. phi1 <-> phi2 is not valid
2. phi1 <-> false is not valid
3. phi2 <-> false is not valid
4. (phi1 -> S1&!S2 and phi2 -> S1&!S2 are both valid) or (phi1 -> !S1&S2 and phi2 -> !S1&S2 are both valid)

Now, check these requirements for your formulas 

    S1 := X b & G c
    S2 := G b & F c
    phi1 := G (b & [c SB b]) 
    phi2 := G (b & [c WB b])

These formulas satisfy all requirement 4, but none of 1-3 since you can prove that

(G (b & [c SB b]) ) <-> (G (b & [c WB b]))

is valid. That is, you just found one example instead of two. Syntactically they are different, but they are equivalent. Moreover, both formulas are no candidates since you can also prove that

!(G (b & [c SB b]) )

is valid, and therefore your formulas phi1 and phi2 are both false. You can see that also by unrolling the SB operator: 

[c SB b] <-> !b & (c | X[c SB b])

and therefore

 (b & [c SB b]) <-> b & !b & (c | X[c SB b])

which is obviously false. Therefore, none of your formulas phi1 and phi2 are candidates for a solution.