Sciweavers

Share
LICS
2010
IEEE

A Sound and Complete Calculus for Finite Stream Circuits

9 years 1 months ago
A Sound and Complete Calculus for Finite Stream Circuits
Stream circuits are a convenient graphical way to represent streams (or stream functions) computed by finite dimensional linear systems. We present a sound and complete expression calculus that allows us to reason about the semantic equivalence of finite closed stream circuits. For our proof of the soundness and completeness we build on recent ideas of Bonsangue, Rutten and Silva. They have provided a "Kleene theorem" and a sound and complete expression calculus for coalgebras for endofunctors of the category of sets. The key ingredient of the soundness and completeness proof is a syntactic characterization of the final locally finite coalgebra. In the present paper we extend this approach to the category of real vector spaces. We also prove that a final locally finite (dimensional) coalgebra is, equivalently, an initial iterative algebra. This makes the connection to existing work on the semantics of recursive specifications.
Stefan Milius
Added 14 Feb 2011
Updated 14 Feb 2011
Type Journal
Year 2010
Where LICS
Authors Stefan Milius
Comments (0)
books