Fixpoint alternation: arithmetic, transition systems, and the binary tree
J. C. Bradfield · RAIRO - Theoretical Informatics and Applications · 1999
We provide an elementary proof of the fixpoint alternation hierarchy in arithmetic, which in turn allows us to simplify the proof of the modal mu-calculus alternation hierarchy. We further show that the alternation hierarchy on the binary tree is strict, resolving a problem of Niwiński.