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

870 questions

988 answers

1.4k comments

439 users

+1 vote

I have a problem regarding the following exercise:

I'm trying to find 2 formulas which satisfy S1 but not S2.

Therefore, the formulas must imply ![b WB a] and !c.

I tried G(a & !b & !c) and G(!b & !c) & X(a).

In both formulas, [b WB a] is false since when a is true, b wasn't true before. Also, c is always false. Therefore those formulas should satisfy S1 but not S2. However, the online tool does not accept this as a correct solution. Where am I wrong?

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

1 Answer

+2 votes
 
Best answer

I checked your two formulas and the second one is not correct. We can prove that

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

is valid, but (G(!b & !c) & X(a)) -> [[b WB a] WB c] & ![[b WB a] SB c] is not valid. 

To find your formulas, I suggest to first disprove [[b WB a] WB c] -> [[b WB a] SB c] so that the tool gives you a counterexample that satisfies [[b WB a] WB c] & ![[b WB a] SB c]. When I do that, I obtain a single path that is described by your first formula G(a & !b & !c). 
To find the second formula, try a proof for !(G(a & !b & !c)) & [[b WB a] WB c] -> [[b WB a] SB c]. Since that is not valid, a counterexample will satisfy !(G(a & !b & !c)) & [[b WB a] WB c] & ![[b WB a] SB c] and will give you a second formula. 
by (139k points)
selected by
Ok I think I understand why formula 2 is not valid. S2 might be true for G(!b & !c) & X(a).

We evaluate [b WB a] not just at the start, but for each "step" of the automata. And once a occured (since it just has to occur at least in the next state due to X(a)) [b WB a] might evaluate to true if a never appears again. And then [[b WB a] SB c] would be true.

Related questions

+2 votes
1 answer
+2 votes
1 answer
0 votes
1 answer
asked Aug 26, 2021 in * TF "Emb. Sys. and Rob." by KB (280 points)
Imprint | Privacy Policy
...