Invited Talk: Damian Niwinski
The expressive power of fixed-point alternation
Alternation of least and greatest fixed point operators has been
recognized as a source of an expressive power of the Mu-calculus,
as well as of its computational difficulty. The strictness of the
alternation hierarchy for Kozen's modal Mu-calculus was established
in 1996 by J.C.Bradfield and (independently) G.Lenzi, only 10 years
after the author of the talk came with the first example of a strict
alternation hierarchy, in the context of powerset tree algebra.
Roughly speaking, the role of diagonalization in the quantifier based
hierarchies is taken here by the so-called parity condition (which
owes its elegant formulation to Emerson and Jutla). This condition
also underlines a tight correspondence between the alternation
hierarchies in various Mu-calculi and the index hierarchies of various
types of automata.
All these hierarchies can be compared to the classical complexity criteria
in the set-theoretical topology, in particular to the Borel definability
and Wadge reducibility. Topological complexity can be seen behind
several strictness results, in particular of the index hierarchy of
the alternating automata, corresponding to Kozen's Mu-calculus
(as first noted by A.Arnold).
Still, the structure of alternation hierarchies is not fully
understood yet. In particular, a decision procedure to determine the
exact level of a formula (or, an automaton) within the hierarchy
is known only in a special case of deterministic automata, although
the techniques used there (in particular, forbidden patterns) may
appear promising for the general case (results of I.Walukiewicz and
author).