Automata and behaviours in categories of processes

An early result of Goguen describes the fundamental adjunction between categories of deterministic automata and their behaviours. Our first step is to redefine (morphisms in) these categories of automata and behaviours so that a restriction in Goguen's approach can be avoided. Subsequently we give a coalgebraic analysis of this behaviour-realization adjunction; it yields a second generalization to other types of (not only deterministic) automata (and their behaviours). We further show that our (redefined) categories of automata and behaviours support elementary process combinators like renaming, restriction, parallel composition, replication and feedback (some of which also occur, for example, in the $pi$-calculus). One of the main contributions is that replication $!P$ is defined for an automaton $P$ such that $!P$ is the terminal coalgebra $!P stackrel{cong{rightarrow P | !P$ of the functor $P | (-)$ ``compose with $P$''. The behaviour functor from automata to their behaviours preserves these process combinators, so that the behaviour of a complex automaton can be understood from the behaviour of its components.