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

1.6k comments

546 users

0 votes
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?
in * TF "Emb. Sys. and Rob." by (250 points)

1 Answer

0 votes
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.
by (166k points)
Understood professor. Thank you for the detailed response.

Related questions

0 votes
1 answer
0 votes
1 answer
0 votes
1 answer
Imprint | Privacy Policy
...