In this paper, we describe a \emph{symbolic} synthesis method which given an algebraic expression that specifies a bitstream function $f$, constructs a (minimal) Mealy machine that realises $f$. The synthesis algorithm can be seen as an analogue of Brzozowski's construction of a finite deterministic automaton from a regular expression. It is based on a coinductive characterisation of the operators of 2-adic arithmetic in terms of stream differential equations.

, , , ,
Scientific Annals of Computer Science
Computer Security

Hansen, H., & Rutten, J. (2010). Symbolic synthesis of Mealy machines from arithmetic bitstream functions. Scientific Annals of Computer Science, XX, 97–130.