Kleene’s Theorem gives a fundamental correspondence between
regular expressions and deterministic finite automata (DFA’s): each
regular expression denotes a language that can be recognized by a DFA
and, vice-versa, the language accepted by a DFA can be specified by a
regular expression. Languages denoted by regular expressions are called
regular. Two regular expressions are called (language) equivalent if they
denote the same regular language. Kozen in 1991 provided regular
expressions with sound and complete algebraic laws that permit formal
reasoning about equivalences between expressions.

Coalgebras provide a general framework for the study of dynamical systems
such as DFA’s. In this presentation we show the application of the above
program to coalgebras over a large class of functors
$F:{\bf Set} \rightarrow {\bf Set}$. We incrementally introduce a set
of expressions for finite deterministic, non-deterministic and
quantitative coalgebras and proved an analogue of Kleene’s Theorem:
each expression denotes the behavior of a finite coalgebra and,
conversely, the behavior of a finite coalgebra can be specified by an
expression. We also provide a sound and complete axiomatization for
these coalgebraic calculi, with the property that two expressions are
provably equivalent if and only if they are bisimilar.

Example of coalgebraic calculi we consider include labeled transition
systems, weighted automata and probabilistic systems.