Preprint: Behavioural differential equations: a coinductive calculus of streams, automata, and power series
The following technical report is now available at ftp.cwi.nl as pub/CWIreports/SEN/SEN-R0023.ps.Z (also via my home page: http://www.cwi.nl/~janr): J.J.M.M. Rutten Behavioural differential equations: a coinductive calculus of streams, automata, and power series Technical Report SEN-R0023, CWI, Amsterdam, 2000. Abstract: Streams, (automata and) languages, and formal power series are viewed coalgebraically. In summary, this amounts to supplying these sets with a deterministic automaton structure, which has the universal property of being final. Finality then 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 afore mentioned structures, closely resembling (and at times generalising aspects of) calculus from classical analysis. (This report combines and extends earlier papers on automata and languages (CONCUR '98) and formal power series (ICALP '99).)
participants (1)
-
Jan Rutten