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

1.1k questions

1.3k answers

1.7k comments

556 users

0 votes

How is the formula derived for both the questions for A SU b? Can someone explain this?

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

1 Answer

0 votes
We simply consider the semantics of [a SU b] which means that a&!b holds until finally b holds. Hence, we use the initial state to observe a&!b and if that should no longer hold, we have to make sure that b holds to finally satisfy [a SU b]. In that case, we switch to the other state so that we can express that this state must be finally reached. So, the construction of the automaton just implements the semantics of the SU operator.

You can derive this also from the recursion law of the SU operator which is [a SU b] <-> b | a & X[a SU b]. Since we want [a SU b] to hold initially, we have to demand that b | a & X[a SU b] must hold initially. This is equivalent to b | a & !b & X[a SU b]. Hence, if b holds, we are done, and otherwise, a & !b must hold, and we have to repeat that in the next step.
by (170k points)
edited by

Related questions

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