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?


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.