Articles in Journals

A classical result by Rabin states that if a set of trees and its complement are both Büchi definable in the monadic second order logic, then these sets are weakly definable. In the language of μ-calculi, this theorem asserts the equality between the complexity classes Σ₂ /\ Π₂ and Comp(Σ₁,Π₁) of the alternation-depth hierarchy of the μ-calculus of tree languages. It becomes natural to ask whether at higher levels of the hierarchy the ambiguous classes Σ_{n + 1} /\ Π_{n + 1} and the composition classes Comp(Σ_n,Π_n) are equal, and for which μ-calculi. A first result of this paper is that the alternation-depth hierarchy of the games μ-calculus - whose canonical interpretation is the class of all complete lattices - enjoys this property. Explicitly, every parity game which is equivalent both to a game in Σ_{n + 1} and to a game in Π_{n + 1} is also equivalent to a game obtained by composing games in Σ_n and Π_n. A second result is that the alternation-depth hierarchy of the μ-calculus of tree languages does not enjoy the property. Taking into account that any Büchi definable set is recognized by a nondeterministic Büchi automaton, we generalize Rabin's result in terms of the following separation theorem: if two disjoint languages are recognized by nondeterministic Π_{n+ 1} automata, then there exists a third language recognized by an alternating automata in Comp(Σ_n,Π_n) containing one and disjoint with the other. Finally, we lift the results obtained for the μ-calculus of tree languages to the propositional modal μ-calculus: ambiguous classes do not coincide with composition classes, but a separation theorem is established for disjunctive formulas.

We propose a method to axiomatize by equations the least prefixed point of an order preserving function. We discuss its domain of application and show that the Boolean μ-calculus has a complete equational axiomatization. The method relies on the existence of a closed structure and its relationship to the equational axiomatization of Action Logic is made explicit. The implication operation of a closed structure is not monotonic in one of its variables; we show that the existence of such a term that does not preserve the order is an essential condition for defining by equations the least prefixed point. We stress the interplay between closed structures and fixed point operators by showing that the theory of Boolean modal μ-algebras is not a conservative extension of the theory of modal μ-algebras. The latter is shown to lack the finite model property.

For an arbitrary category, we consider the least class of functors containing the projections and closed under finite products, finite coproducts, parameterized initial algebras and parameterized final coalgebras, i.e. the class of functors that are definable by μ-terms. We call the category μ-bicomplete if every μ-term defines a functor. We provide concrete examples of such categories and explicitly characterize this class of functors for the category of sets and functions. This goal is achieved through parity games: we associate to each game an algebraic expression and turn the game into a term of a categorical theory. We show that μ-terms and parity games are equivalent, meaning that they define the same property of being μ-bicomplete. Finally, the interpretation of a parity game in the category of sets is shown to be the set of deterministic winning strategies for a chosen player.

A μ-lattice is a lattice with the property that every unary polynomial has both a least and a greatest fix-point. In this paper we define the quasivariety of μ-lattices and, for a given partially ordered set P, we construct a μ-lattice J_P whose elements are equivalence classes of games in a preordered class J(P). We prove that the μ-lattice J_P is free over the ordered set P and that the order relation of J_P is decidable if the order relation of P is decidable. By means of this characterization of free μ-lattices we infer that the class of complete lattices generates the quasivariety of μ-lattices.

The alternation hierarchy problem asks whether every μ-term φ, that is, a term built up also using a least fixed point constructor as well as a greatest fixed point constructor, is equivalent to a μ-term where the number of nested fixed points of a different type is bounded by a constant independent of φ. In this paper we give a proof that the alternation hierarchy for the theory of μ-lattices is strict, meaning that such a constant does not exist if μ-terms are built up from the basic lattice operations and are interpreted as expected. The proof relies on the explicit characterization of free μ-lattices by means of games and strategies.