- Automata for Coalgebras: an approach using predicate liftings
- Lecture Notes in Computer Science
- Pages (from-to)
- Document type
- Interfacultary Research Institutes
- Institute for Logic, Language and Computation (ILLC)
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 of parity automata to this 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 \mathbbAA with nonempty language into a small pointed coalgebra (\mathbbS,s)(Ss) of type T that is recognized by \mathbbAA, and of size exponential in that of \mathbbAA. \mathbbSS is obtained in a uniform manner, on the basis of the winning strategy in our satisfiability game associated with \mathbbAA. On the basis of our proof we obtain a general upper bound for the complexity of the non-emptiness problem, under some mild conditions on Λ and T. Finally, relating our automata-theoretic approach to the tableaux-based one of Cîrstea et alii, we indicate how to obtain their results, based on the existence of a complete tableau calculus, in our framework.
- go to publisher's site
- Proceedings title: Automata, languages and programming: 37th International Colloquium, ICALP 2010, Bordeaux, France, July
6-10, 2010: proceedings. - Pt. 2
Place of publication: Berlin
Editors: S. Abramsky, C. Gavoille, C. Kirchner, F. Meyer auf der Heide, P.G. Spirakis
If you believe that digital publication of certain material infringes any of your rights or (privacy) interests, please let the Library know, stating your reasons. In case of a legitimate complaint, the Library will make the material inaccessible and/or remove it from the website. Please Ask the Library, or send a letter to: Library of the University of Amsterdam, Secretariat, Singel 425, 1012 WP Amsterdam, The Netherlands. You will be contacted as soon as possible.