VRS - CTL Counterexample verification through LTL Tool

Question

Problem 7a

Provided above is the counterexample that I came up with and given below is the LTL for this counterexample structure
 

((!a & b) & X(!a & !b) & X(G a))
which seems to satisfy S₁ and not S₂

S_¹ = b & X (!b & G F a)

S2 = b & X (!b & G  a)

Given below is the input that I gave to the LTL teaching tool. 

((!a & b) & X(!a & !b) & X(G a)) -> (b & X (!b & G F a)) & !(b & X (!b & G a))

It returns valid for this combination, however it returns valid for all the other combinations given below:

((!a & b) & X(!a & !b) & X(G a)) -> !(b & X (!b & G F a)) & (b & X (!b & G a))

((!a & b) & X(!a & !b) & X(G a)) -> !(b & X (!b & G F a)) & !(b & X (!b & G a))

((!a & b) & X(!a & !b) & X(G a)) -> (b & X (!b & G F a)) & (b & X (!b & G a))

Is the counterexample structure and the corresponding LTL correct? If so, why does the teaching tool return "VALID" for all the rest of the combinations?

Answer 1

First of all your example is totally correct (assuming that the state with "b" is your initial state which you probably forgot to draw here) but your LTL formula representing the Kripke structure is wrong as you need to have :

((!a & b) & X(!a & !b) & XX(G a)) instead of ((!a & b) & X(!a & !b) & X(G a))

As "G a" only starts after two steps starting from the initial state. For that same reason all your combinations return "VALID" as ((!a & b) & X(!a & !b) & X(G a)) = 0 because "G a" and "!a" can never hold at the same time obviously. With that all combinations are effectively describing "0 -> S_i" which is of course always valid.

Comments

One thing I want to add: The corrected formula is still not totally defined as it doesn't specify the value of b after the second step. For this exercise this is of course not relevant as neither S1 nor S2 care about the later values of b. However to be totally correct, the LTL must be actually:
((!a & b) & X(!a & !b) & XX((G a) & (G !b)))