2
$\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$

Your Answer

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

Browse other questions tagged or ask your own question.