Automata for Coalgebras: An Approach Using Predicate Liftings

Universal Coalgebra provides the notion of a coalgebra as the natural mathematical generalization of state-based evolving systems such as (infinite) words, trees, and transition systems. We lift the theory y automata to a coalgebraic level of abstraction by introducing, for a set Λ of predicate liftings associated with a set functor T , the notion of a Λ-automata operating on coalgebras of type T . In a familiar way these automata correspond to extensions of coalgebraic modal logics with least and greatest fixpoint operators. Our main technical contribution is a general bounded model property result: We provide a construction that transforms an arbitrary Λ-automaton A with nonempty language into a small pointed coalgebra (S, s) of type T that is recognized by A, and of size exponential in that of A. S is obtained in a uniform manner, on the basis of the winning strategy in our satisfiability game associated with A. On the basis of our proof we obtain a general upper bound for the...

• Type: Conference
• Year: 2010
• Where: ICALP
• Authors: Gaëlle Fontaine, Raul Andres Leal, Yde Venema
• Keywords: Coalgebraic Modal Logics, ICALP 2010, Natural Mathematical Generalization, Programming Languages, State-based Evolving Systems