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
Hi, in local model checking the rules for nu and mu are the same. I'm wondering how this works, I don't want a formal proof, a bit intuition is enough.

Also i have another question suppose we have a formula phi.

Is mu.phi always a subset of nu.phi? Im guessing it is, could that be the reason the rules are the same?
in * TF "Emb. Sys. and Rob." by (870 points)

1 Answer

+1 vote
Best answer
We can treat mu and nu formulas the same way in the rules (at first) since we only use the property that these formulas define fixpoints, and at that point is does not matter which particular fix point, since we just unroll the fixpoint. That means if we have x=f(x), we replace x by f(x) that's all. However, note that if a repetition is found, then the treatment of mu and nu is different. At that point we do care about least and greatest fixpoints.

And, yes mu x. phi is always a subset of nu x.phi, since the set of fixpoints form a lattice also.
by (166k points)
selected by
Imprint | Privacy Policy