Last week Thursday, February 19th, I delivered my talk in the internal seminar at Leicester. I had planned to give a technical outline of the proof of the Complementation Lemma for Coalgebra Automata from my paper with Yde Venema, including the various results in Coalgebraic Logic, Game Theory and Automata Theory that contributed to the paper, but then managed only the two third of it. As there have been requests for further details I am planning for an extended seminar on the proof at Leicester in the next month.

Title: Complementation of Coalgebra Automata

Abstract: Coalgebra automata, introduced by Venema, generalise the well-known automata operating on infinite words, such as streams, trees, graphs, or transition systems. The coalgebraic perspective lays foundation for a unified theory of automata operating on infinite models.

We prove a complementation lemma for coalgebra automata. In particular, we provide an algorithm that transforms a given coalgebra automaton into an automaton of similar type accepting precisely those pointed coalgebras rejected by the original automaton. Our construction works for arbitrary Set functors which preserve weak pullbacks and restrict to finite sets.

Our proof is coalgebraic in nature in that we introduce and use the coinductive notion of game bisimilarity between certain kinds of parity graph games.