Yde VenemaLogic and automata: a coalgebraic perspectiveInstitute for Logic, Language and Computation, Universiteit van Amsterdam, Plantage Muidergracht 24, 1018TV Amsterdam, The Netherlands yde@science.uva.nl

A long and respectable tradition in theoretical computer science, going back to the work of Büchi and Rabin, links the research fields of automata theory and logic. This link becomes particularly strong for automata operating on (potentially) infinite objects like streams, trees or transition systems. An interesting phenomenon in this area is that most (but not all) key results hold for word and tree automata alike, and that many can even be formulated and proved for automata that operate on yet other objects such as trees of unbounded branching degree, or labelled transition systems. The aim of the talk is to show that these results can be formulated and proved at the more general abstraction level of coalgebra.

Universal Coalgebra is an emerging mathematical theory of state-based evolving systems. Words, trees and transition systems are all examples of coalgebras of a certain type, which is formally given as a functor on the category (with sets as objects and functions as arrows). We introduce the concept of an -automata, a device that operates on coalgebras of type . The criterion under which such an automaton accepts or rejects a pointed coalgebra is formulated in terms of an infinite two-player graph game. Extending Moss' coalgebraic logic with fixpoint operators, we also introduce a language of coalgebraic fixed point logic for coalgebras, and we provide a game semantics for this language.

Finally we show that some of the central results in automata theory can be generalized to the abstraction level of coalgebras and thus lay out the foundations of a universal theory of automata. As examples of such results, we will see that the class of recognizable languages of coalgebras is closed under taking unions, intersections, and projections. We also prove that if a coalgebra automaton accepts some coalgebra it accepts a finite one of bounded size. Many of these results are based on an explicit construction which transforms a given alternating -automaton into an equivalent nondeterministic one, of bounded size.