3
$\begingroup$

I'm reading the Model Chekcing book of E. M. Clarke and in the chapter about µ-calculus there is an example formula $$ f = \mu Z. ((q \mathrel{\mathrm{AND}} Y) \mathrel{\mathrm{OR}} \langle a \rangle Z) $$ As the author has mentioned, here $Y$ is a free variable, and we need an association list to pair $Y$ with the corresponding states. But why do we need it? Can it be replaced by an atomic proposition?

$\endgroup$
1
$\begingroup$

If you define the $\mu$-calculus to not allow free variables, you would have the problem that the components of a well-formed formula are not again well-formed formulas.

Consider a well-formed formula "$\mu Z . \varphi$", such that $Z$ occurs freely in $\varphi$ and $\varphi$ has no other free variables. If you were to exclude formulas with free variables from your definition, $\varphi$ would not be a well-formed formula.

This would make structural induction on formulas more complicated. For example the semantics of formulas (the set of states in which the formula holds) is usually defined inductively: You define the semantics of "$\mu Z . \varphi$" in terms of the semantics of $\varphi$. If your definition says $\varphi$ is not a well-formed formula, you would have to extended the induction to also cover these non-well-formed cases. If you have to consider these cases every time you do structural induction, you haven't really gained anything from excluding them in your definition.

| cite | improve this answer | |
$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.