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

868 questions

986 answers

1.4k comments

438 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 (139k points)
selected by

Related questions

0 votes
1 answer
0 votes
1 answer
0 votes
1 answer
0 votes
1 answer
0 votes
1 answer
Imprint | Privacy Policy
...