Lifting Adjunctions to Coalgebras to (Re)Discover Automata ...

Reference

Henning Kerstan, Barbara König, and Bram Westerbaan. Lifting adjunctions to coalgebras to (Re)Discover automata constructions. In Marcello M. Bonsangue, editor, Coalgebraic Methods in Computer Science, volume 8446 of Lecture Notes in Computer Science, pages 168–188. Springer Berlin Heidelberg, 2014.

Abstract

It is a well-known fact that a nondeterministic automaton can be transformed into an equivalent deterministic automaton via the powerset construction. From a categorical perspective this construction is the right adjoint to the inclusion functor from the category of deterministic automata to the category of nondeterministic automata. This is in fact an adjunction between two categories of coalgebras: deterministic automata are coalgebras over Set and nondeterministic automata are coalgebras over Rel. We will argue that this adjunction between coalgebras originates from a canonical adjunction between Set and Rel. In this paper we describe how, in a quite generic setting, an adjunction can be lifted to coalgebras, and we compare some sufficient conditions. Then we illustrate this technique in length: we recover several constructions on automata as liftings of basic adjunctions including determinization of nondeterministic and join automata, codeterminization, and the dualization of linear weighted automata. Finally, we show how to use the lifted adjunction to check behavioral equivalence.

Keywords:

adjunction, coalgebra, lifting

Suggested BibTeX entry:

@inproceedings{KKW14,
    author = {Henning Kerstan and Barbara K{\"o}nig and Bram Westerbaan},
    booktitle = {Coalgebraic Methods in Computer Science},
    editor = {Marcello M. Bonsangue},
    pages = {168--188},
    publisher = {Springer Berlin Heidelberg},
    series = {Lecture Notes in Computer Science},
    title = {Lifting Adjunctions to Coalgebras to ({R}e){D}iscover Automata Constructions},
    volume = {8446},
    year = {2014}
}



See dx.doi.org ...
© University of Duisburg-Essen, Theoretical Computer Science group