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


543 users

0 votes

Why we can not combine same variables states as one state in quotient structure. As far as I know even 4 or more states can also be combined as one state, so by looking at this why s0,s2,s3,s5 are not combined into one state?  is quotient structure unique?

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

1 Answer

0 votes
Simple answer: We cannot combine states that are not bisimilar. If states just have the same label, it does not mean that they are bisimilar, the states must additionally satisfy the further requirements on their successor states.

Why is that so? We want to minimize state transition systems, but do not want to chance their satisfaction of properties like mu-calculus formulas. One can prove (see page 191 of VRS-05-MuCalculus) that two states satisfy the same mu-calculus formulas (without past modalities) if and only if these states are bisimilar.

For instance, the states {s2} and {s0,s5} are not bisimilar and can therefore be distinguished by mu-calculus formulas. For instance, <>a holds on {s2}, but not on {s0,s5} since s2 has a successor state where a holds, but {s0,s5} does not have such a state. States {s2} and {s3} can be distinguished by <>(b&d). Hence, you cannot combine these states if you want to preserve the validity of the same set of mu-calculus formulas.

The minimal quotient structure unique because of the above mentioned theorem that expresses the bisimilar states as those that satisfy the same mu-calculus formulas (without past modalities).
by (166k points)
Imprint | Privacy Policy