Articles in Conference Proceedings

We define the class of algebraic models of μ-calculi and study whether every such model can be embedded into a model which is a complete lattice. We show that this is false in the general case and focus then on free modal μ-algebras, i.e. Lindenbaum algebras of the propositional modal μ-calculus. We prove the following fact: the MacNeille-Dedekind completion of a free modal μ-algebra is a complete modal algebra, hence a modal μ-algebra (i.e. an algebraic model of the propositional modal μ-calculus). The canonical embedding of the free modal μ-algebra into its Dedekind-MacNeille completion preserves the interpretation of all the terms in the class Comp(Σ₁,Π₁) of the alternation-depth hierarchy. The proof uses algebraic techniques only and does not directly rely on previous work on the completeness of the modal μ-calculus.

We introduce a new method (derived from model theoretic general combination procedures in automated deduction) for proving fusion decidability in modal systems. We apply it to show fusion decidability in case not only the boolean connectives, but also a universal modality and nominals are shared symbols.

We prove that every finitary polynomial endofunctor of a category C has a final coalgebra, provided that C is locally Cartesian closed, it has finite coproducts and is an extensive category, it has a natural number object.

Every parity game is a combinatorial representation of a closed Boolean μ-term. When interpreted in a distributive lattice every Boolean μ-term is equivalent to a fixed-point free term. The alternation-depth hierarchy is therefore trivial in this case. This is not the case for non distributive lattices, as the second author has shown that the alternation-depth hierarchy is infinite. In this paper we show that the alternation-depth hierarchy of the games μ-calculus, with its interpretation in the class of all complete lattices, has a nice characterization of ambiguous classes: 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.

We investigate the reasons for which the existence of certain right adjoints implies the existence of some final coalgebras, and vice-versa. In particular we prove and discuss the following theorem which has been partially available in the literature: let F G be a pair of adjoint functors, and suppose that an initial algebra F(X) of the functor H(Y) = X + F(Y) exists; then a right adjoint G(X) to F(X) exists if and only if a final coalgebra HG(X) of the functor K(Y) = X × G(Y) exists. Motivated by the problem of understanding the structures that arise from initial algebras, we show the following: if F is a left adjoint with a certain commutativity property, then an initial algebra of H(Y) = X + F(Y) generates a subcategory of functors with inductive types where the functorial composition is constrained to be a Cartesian product.

We survey on the ongoing research that relates the combinatorics of parity games to the algebra of categories with finite products, finite coproducts, initial algebras and final coalgebras of definable functors, i.e. μ-bicomplete categories. We argue that parity games with a given starting position play the role of terms for the theory of μ-bicomplete categories. We show that the interpretation of a parity game in the category of sets and functions is the set of deterministic winning strategies for one player in the game. We discuss bounded memory communication strategies between two parity games and their computational significance. We describe how an attempt to formalize them within the algebra of μ-bicomplete categories leads to develop a calculus of proofs that are allowed to contain cycles.

We present a calculus of ``circular proofs'': the graph underlying a proof is not a finite tree but instead it is allowed to contain a certain amount of cycles. The main challenge in developing a theory for the calculus is to define the semantics of proofs, since the usual method by induction on the structure is not available. We solve this problem by associating to each proof a system of equations - defining relations among undetermined arrows of an arbitrary category with finite products and coproducts as well as constructible initial algebras and final coalgebras - and by proving that this system admits always a unique solution.

We show how to axiomatize by equations the least prefixed point of an order preserving function and discuss the domain of application of the proposed method. Thus, we generalize the well known equational axiomatization of Propositional Dynamic Logic to a complete equational axiomatization of the Boolean Modal μ-Calculus. We show on the other hand that the existence of a term which does not preserve the order is an essential condition for the least prefixed point to be definable by equations.