Automata and Fixed Point Logics for Coalgebras

There is a long tradition in theoretical computer science connecting logic and automata theory. As a paradigmatic example we mention the link between the modal mu-calculus and parity automata on graphs. Much of this work has a strong coalgebraic flavour, but to our knowledge this perspective has never been made explicit or exploited. In the talk we will generalize existing connections between automata and logic to a more general, coalgebraic level. For any arbitrary set-based functor F meeting some mild constraints, we define the notion of an F-automaton. Such a device will operate on pointed F-coalgebras, i.e., F-coalgebras with a selected actual state, and either accept or reject such a structure. The criterion for rejection and acceptance are given in terms of an infinite two-player parity game. We also introduce a rather natural language of coalgebraic fixed point logic for F-coalgebras, and we provide a game semantics for this language. Finally, we provide a procedure transforming a coalgebraic fixpoint formula p into a an automaton A_p that is equivalent to p in the sense that A_p accepts precisely those pointed F-coalgebras in which p holds. This then establishes the link between logic and automata on a coalgebraic level.  

hosted by