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

1.6k comments

543 users

0 votes

there must be error in box (x) output? Also explain how implication is computed here.

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

1 Answer

0 votes

Where exactly do you see an error here?

And the implication is done like one would except, so if you have two state sets A and B and you want to compute States(A -> B) then the result is:

B U (S \ A)   with S being the complete state set S := {s0, ..., s7}

So state si is part of States(A -> B) if either si is part of set B or si is not part of set A. Or you can put it like that:

If a state si is part of set A then it must be also part of set B. If this condition holds true, then si is also element of States(A -> B) otherwise it isn't.

by (3.4k points)
Thanks for the response.

How could universal predecessors of x be all states in step 0?
This is because you calculate the greatest fixpoint via a "nu" operator instead of a "mu" operator (which calculates the least fixpoint). Thus you need to start with the whole state set.
I think you mis-understood my question. I know that x will be initialised with all the states due to nu operator.

My question is how States([]x) = {s0;...;s7}?

How universal predecessor of x could be all the states, Please elaborate that part.
The reason for that is simply that x contains all states, thus all transitions do of course point to some state in {s0,...,s7} i.e. there is no state that has a transition that does not point into that set (as there are no other states outside this set). Also see page 56 in chapter 4 in that regard: pre_{universal}(S) = S
Imprint | Privacy Policy
...