LTL Equivalence and its notation

Question

S1 = G a <-> X b
S2 = G a <-> F b

To satisfy S2 while not satisfying S1, I got these automata(A1 and A2):

I have used the notations here to represent these automata:

A1: (a&b) & X(Ga & !b)

A2: (a&b) & X(!a & !b) & XXGa

I have also verified that the following is VALID in the tool:

(((a&b) & X(Ga & !b)) | ((a&b) & X(!a & !b) & XXGa )) -> (G a <-> F b & !(G a <-> X b))

However, the solutions are rejected.

So, the questions are: Are the automata incorrect? or the notation? or how the tool is used?

Answer 1

First of all, make sure that you don't have syntax problems (you have some!). In the formulas you listed, you probably mean something else than you have written down. 

For instance, note that the parser of the tool splits the input string into tokens where blanks and other symbols like brackes and boolean operators separate the tokens. Hence, Ga is read as a single variable instead of "G a" which means "always a". For the same reason, you must not write "XXGa" and should write "X X G a" instead. 

Second, make sure that the precedences are as you want. The formula (G a <-> F b & !(G a <-> X b)) is an equivalence with left hand side "G a" and right hand side "F b & !(G a <-> X b)". You probably want (G a <-> F b) & !(G a <-> X b) instead.

Even after the synatx fixes, I can confirm that the following is valid, i.e., A1 is an example that satisfies S1 but not S2:

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

However, A2 is not fine: 

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

has a counterexample:

                a : 1 0 1 1 ...
                b : 1 0 0 0 ...
              G a : 0 0 1 1 ...
              X b : 0 0 0 0 ...
              F b : 1 0 0 0 ...
      G a <-> X b : 1 1 0 0 ...
      G a <-> F b : 0 1 0 0 ...
   !(G a <-> X b) : 0 0 1 1 ...

So, both G a <-> F b and !(G a <-> X b) are false in this case.

Comments

Thank you professor, I initially got the message "Both formulas are not correct." and was confused. Now, I know the first formula was parsed improperly due to not using space.
 
Since A2 is correct, could you please help me understand how to obtain the other possible automata that satisfies only S2 but not S1?

---

Well, you could state that !A1 & S2 -> S1 so that a counterexample will satisfy its negation, i.e., !A1 & S2 & !S1. From the counterexample, you can easily read another formula (automaton/trace).