Fixpoint alternation: arithmetic, transition systems, and the binary tree
LFCS, Division of Informatics, University of Edinburgh,
Edinburgh EH9 3JZ, U.K., firstname.lastname@example.org.
2 BRICS, Department of Computer Science, Aarhus University, Bygning 540, Ny Munkegade, 8000 Århus C, Denmark.
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.
Mathematics Subject Classification: 68Q60 / 03D55 / 03D70 / 03D80
Key words: Fixpoints / mu-calculus / alternation / modal logic.
© EDP Sciences, 1999