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

557 users

0 votes
Hi, im very sorry if this was already mentioned somewhere or discussed in the lecture, but I have not found anything yet . How do we know from the symbolic description whether we have states s_i s_j with L(s_i)=L(s_j)? Do we assume them to be distinct with a new variable x which we just use for this purpose?

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

1 Answer

+1 vote
 
Best answer
If we consider a symbolic description of a Kripke structure (I guess that is what you mean), then we have the variables V, the initial states I, and the transition relation R given. The states are by definition the subsets of V, i.e., we have 2^|V| many states and these subsets are viewed as variable assignments to find the transitions with R.

So, there is no label function in this case, because we define L(s) = s and that in turn means that there is no reason to have your doubt.

The other way around: if we have a Kripke structure with two states s1 and s2 with the same label L(s1)=L(s2), then we cannot generate a symbolic description just with the variables known by the structure. In that case, we have to add further variables to distinguish between such states. And such additional variables may have to be ignored for simulation computations etc. That is one reason why these different sets of variables may come from.
by (170k points)
selected by
Thank you, I understand now.
Imprint | Privacy Policy
...