*Abstract:*

This work examines propositional fixed point temporal and modal logics called mu-calculi and their relationship to automata on infinite strings and trees. We use correspondences between formulae and automata to explore definability in mu-calculi and their fragments, to provide normal forms for formulae, and to prove completeness of axiomatisations. The study of such methods for describing infinitary languages is of fundamental importance to the areas of computer science dealing with non-terminating computations, in particular to the specification and verification of concurrent and reactive systems.

To emphasise the close relationship between formulae of mu-calculi and alternating automata, we introduce a new first recurrence acceptance condition for automata, checking intuitively whether the first infinitely often occurring state in a run is accepting. Alternating first recurrence automata can be identified with mu-calculus formulae, and ordinary, non-alternating first recurrence automata with formulae in a particular normal form, the strongly aconjunctive form. Automata with more traditional Büchi and Rabin acceptance conditions can be easily unwound to first recurrence automata, i.e. to mu-calculus formulae.

In the other direction, we describe a powerset operation for
automata that corresponds to fixpoints, allowing us to translate
formulae inductively to ordinary Büchi and Rabin-automata.
These translations give easy proofs of the facts that
Rabin-automata, the full mu-calculus, its strongly aconjunctive
fragment and the monadic second-order calculus of *n*
successors SnS are all equiexpressive, that Büchi-automata,
the fixpoint alternation class *Pi*_2 and the strongly
aconjunctive fragment of *Pi*_2 are similarly related, and
that the weak SnS and the fixpoint-alternation-free fragment of
mu-calculus also coincide. As corollaries we obtain Rabin's
complementation lemma and the powerful decidability result of
SnS.

We then describe a direct tableau decision method for modal and linear-time mu-calculi, based on the notion of definition trees. The tableaux can be interpreted as first recurrence automata, so the construction can also be viewed as a transformation to the strongly aconjunctive normal form.

Finally, we present solutions to two open axiomatisation
problems, for the linear-time mu-calculus and its extension with
path quantifiers. Both completeness proofs are based on
transforming formulae to normal forms inspired by automata. In
extending the completeness result of the linear-time mu-calculus to
the version with path quantifiers, the essential problem is
capturing the limit closure property of paths in an axiomatisation.
To this purpose, we introduce a new *\exists\nu*-induction
inference rule.

This report is available in the following formats:

- PDF file
- Gzipped PDF file
- PostScript file
- Gzipped PostScript file
- PostScript file with Type 1 fonts
- Gzipped PostScript file with Type 1 fonts
- LaTeX DVI file
- Gzipped LaTeX DVI file