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

912 questions

1k answers

1.4k comments

441 users

0 votes

Is this also correct.

In this [a SU b] holds in an infinite loop so globally. whereas Ga does not hold. 

So S1 is satisfied and S2 is not.

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

1 Answer

0 votes
 
Best answer

Yes, that is true which you can check with the LTL prover:

(a&!b) & 
G( ((a&!b)->X(!a&b)) & 
   ((!a&b)->X(a&!b)) 
 ) 
-> !((G a) & (F b)) & (G[a SU b])
by (142k points)
selected by

Related questions

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