Global Model Checking: "Alternation-free"

Question

I don't know what exactly is meant by alternation-free. First, I thought it was related to the alternation depth, meaning if there is a change between mu and nu, then there is an alternation and it is therefore not "alternation-free".

So, for "mu y. ([] y & mu x. (b | y | <:> x))" I would have said it is alternation-free, as there are only mu and no nu. So there is no alternation present. But the accepted answer says otherwise.

Is alternation-free only related to the variables? So, since there is a y inside the mu x. part, it counts as an alternation?

Comments

Is the problem persistent?

Answer 1

You are right with your thoughts. Alternation-free means that there are no fix point formulas of different kind (means mu and nu) that depend on each other. The formula that you mention should be alternation-free, I am wondering that your answer is not accepted. Please tell your tutor about that, you should get your points, and maybe we have to fix something in the online corrections.

To clarify further mu y. ([] y & nu x. (b | y | <:> x)) would have an alternation, but mu y. ([] y & y | nu x. (b | <:> x)) would also be alternation free (since the inner fix point does not depend on the outer one).

Comments

Uff. When generating the tasks, we are generating three mu-calculus formulas per Kripke Structure. That's done by a recursive function called generateSpec that is given a Restriction object. That has a parameter AlternationFreeOp. For the result, we set AlternationFreeOp = restriction.AlternationFreeOp. That means that we rely on the function generateMuSpecNoConstant to implement that Restriction.

---

@KS Thank you for providing code that computes the AlternationDepth. I read it. Seems to do the right thing. I fed some examples to it. Seems correct.

I added this code to the generate-function. Now, after the formula is generated (with respect to a given restriction), the alternationfreeness isn't deduced from the restriction anymore but determined by checking AlternationDepth to be equal to zero.

I regenerated all standard solutions based on that change.

---

Great, I just hope that the code I wrote in a hurry is correct. But I think so, even though I have not verified it...