Am 7. September 2009 habe ich meinen Vortrag ueber das Komplementierungslemma fuer Koalgebraautomaten im Rahmen der CALCO Konferenz 2009 in Udine gehalten. Das Papier kann heruntergeladen werden, genauso wie die Folien. Ich wuerde mich ueber Kritik, Vorschlaege, und Fragen freuen : email(at)christiankissig.de !

Titel Complementation of Coalgebra Automata

Zusammenfasung In our paper we show that the class of languages of coalgebras is closed under taking complements (the complementation lemma for coalgebra automata). Therefor we take the perspective, that states in coalgebra automata are formulas of a coalgebraic logic extended by fixed point operators.

Our paper divides into three parts, each with results of independent interest. First, we define the semantical dual of Moss' cover modality in the positive fragment of Moss' coalgebraic logic. We call this the one-step complementation lemma of coalgebraic logic. It allows us to push negation inwards, over nabla. We obtain that Moss' coalgebraic logic is essentially negation-free.

The one-step complementation lemma extends inductively to all formulas, and coinductively to coalgebra automata. We had to verify that the latter indeed yields a complementary automaton. Therefor we developed a coinductive proof method for parity graph games, based on Johann van Benthem's notion of power of players. Acceptance games of coalgebra automata are parity graph games, where some positions can be distinguished as basic. Each play in the acceptance game can then be divided into rounds, each delimited by terminal or basic positions. The player's powers then give rise to a normalisation of the player's interaction in each round. On the normalised interaction pattern we can define a (bi)simulation relation, similar to the one known from modal logic. Using game (bi)simulation, we can compare games, uniformly for all transition types of automata.

In the third we put the one-step complementation lemma and the game bisimulation together and obtain the complementation lemma for coalgebra automata. However, the one-step complementation introduces a non-determinism after each transition step, so that we introduce two new types of coalgebra automata, trans-alternating and semi-transalternating automata. They turned out to be effectively translatable with alternating automata.