Global Model Checking, Alternation Depth

Question

I have confusion related to the topic of alternation free and alternation depth.
How are S1 = nu x. ([]x & mu y. (b | b | [] y)) not alternation free since least fixpoint is nested in a greatest fixpoint.
Also, is S2 = nu x. (<:>x & nu y. ((a|x) & []y)) alternation free?  If yes, how? and if no, then why not?

Answer 1

S1 = nu x. ([]x & mu y. (b | b | [] y)) is alternation free since least fixpoint mu y. (b | b | [] y) nested in the greatest fixpoint does not depend on the fixpoint variable of the outer fixpoint. Hence, you can first compute the state of the inner fixpoint with one fixpoint iteration, and with these states, you can compute the fixpoint of the outer fixpoint also with a single fixpoint iteration.

S2 = nu x. (<:>x & nu y. ((a|x) & []y)) is also alternation free since the two nested fixpoints are of the same kind, so that there is no alternation. Alternation means that least fixpoints are nested in greatest fixpoints or vice versa.

Comments

Understood professor. Thank you for the detailed response.