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

Translate the following formula to an equivalent µ-calculus formula.


According to the cheatsheet provided, I get the following answer:

EF(νx.b ∧ ♦x)
µx.(νy.♦∧ (νx.(b ∧ ♦x)) ∨ ♦x)

The solution provided is:

µy.(νx.♦x ∧ (νx.(∧ ♦x)) ∨ ♦y)

Are both of these equal and correct?

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

1 Answer

+1 vote
Best answer

If you treat the inner formula as "phi := (vx.b ∧ ♦x)" then your solution reduces to:

µx.(vy.♦y ∧ phi ∨ ♦x)

while the sample solution is reduced to:

µy.(vx.♦x ∧ phi ∨ ♦y)

which are both equivalent because the only difference is that the variables x and y are switched. The important part is that the variable x in the formula phi does not depend on the variables outside of phi because the variable is rebound in phi, so instead you could also use:

"phi := (vz.b ∧ ♦z)"

instead without changing the meaning.

by (3.4k points)
selected by
Imprint | Privacy Policy