|Abstract + References|
|PDF (820 K)|
|Save as Citation Alert|
Behavioural differential equations: a coinductive calculus of streams, automata, and power series*1
J. J. M. M. Rutten,
CWI, P.O. Box 94079, 1090 GB, Amsterdam, The Netherlands
Received 25 October 2000; revised 11 November 2002; accepted 14 November 2002; Communicated by D. Sannella Available online 19 December 2002.
We present a theory of streams (infinite sequences), automata and languages, and formal power series, in terms of the notions of homomorphism and bisimulation, which are the cornerstones of the theory of (universal) coalgebra. This coalgebraic perspective leads to a unified theory, in which the observation that each of the aforementioned sets carries a so-called final automaton structure, plays a central role. Finality forms the basis for both definitions and proofs by coinduction, the coalgebraic counterpart of induction. Coinductive definitions take the shape of what we have called behavioural differential equations, after Brzozowski's notion of input derivative. A calculus is developed for coinductive reasoning about all of the aforementioned structures, closely resembling calculus from classical analysis.
Author Keywords: Coalgebra; Automaton; Homomorphism; Bisimulation; Finality; Coinduction; Stream; Formal language; Formal power series; Differential equation; Input derivative
Mathematical subject codes: 68Q10; 68Q55; 68Q85
*1 This paper is a revised version of Technical Report SEN-R0023, CWI, Amsterdam, 2000.
Volume 308, Issues 1-3 , 3 November 2003 , Pages 1-53
Send feedback to ScienceDirect