Talk "Coalgebras and Generalized Regular Expressions"

by Stefan Milius

Sat, 16 March 2013 at 09:45 am in Rome, Italy

Joint work with: Marcello Bonsangue and Alexandra Silva

Abstract: Calculi of (generalized) regular expression that allow to reason about the equivalence up to behavioral equivalence of states of coalgebras have recently been investigated by Silva et al. In this talk I present a setting in which one can extend an expression calculus for behavioral equivalence to one for a new and coarser coalgebraic language equivalence; the latter equivalence arises from a generalized powerset construction that determinizes coalgebras. It is shown that soundness and completeness are established by proving that expressions modulo axioms of a calculus form the rational fixpoint of the functor describing the type of the systems one wants to reason about. The main result is that the rational fixpoint of the functor $FT$, where $T$ is a monad describing the branching of the systems (e.g.~non-determinism, weights, probability etc.), has as a quotient the rational fixpoint of the ``determinised'' type functor $\bar F$, a lifting of $F$ to the category of $T$-algebras. As an application, I consider weighted automata, and I present a new sound and complete expression calculus for weighted language equivalence. As a special case, we obtain non-deterministic automata, where we recover Rabinovich's sound and complete calculus for language equivalence.