Here you can ask questions and find or give answers to organizational, academic and other questions about studying computer science.

1.1k questions

1.2k answers


543 users

0 votes

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

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

Automata A1 and A2I 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?

in * TF "Emb. Sys. and Rob." by (480 points)

1 Answer

+1 vote
Best answer

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.

by (166k points)
selected by
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).

Related questions

0 votes
1 answer
0 votes
1 answer
0 votes
1 answer
0 votes
1 answer
asked Aug 24, 2022 in * TF "Emb. Sys. and Rob." by CS_E (2.9k points)
0 votes
1 answer
Imprint | Privacy Policy