BIB-VERSION:: CS-TR-v2.0
          ID:: SBCS//stark/dfcalc.dvi
       ENTRY:: July 2, 1994
ORGANIZATION:: State University of New York at Stony Brook, Computer Science
       TITLE:: An Calculus of Dataflow Networks
        TYPE:: Preprint
      AUTHOR:: Stark, Eugene W.
     CONTACT:: Eugene W. Stark, Department of Computer Science,
                   SUNY at Stony Brook, Stony Brook, NY 11794-4400
                   Tel: 516-632-8444 <stark@cs.sunysb.edu>
	DATE:: February, 1992
   RETRIEVAL:: HTTP from BSD7.CS.SUNYSB.EDU with the URL
		   http://bsd7.cs.sunysb.edu/~stark/REPORTS/dfcalc.ps.gz
       NOTES:: A version of this paper appeared as:
		E. W. Stark,
		"A Calculus of Dataflow Networks"
		Proceedings of the Seventh Annual Symposium
			on Logic in Computer Science
		IEEE Computer Society Press
		June, 1992
		pp. 125-136

ABSTRACT::

Dataflow networks are a paradigm for concurrent computation in which a
collection of concurrently and asynchronously executing processes communicate
by sending data values over FIFO communication channels.  In this paper,
we define a CCS-style calculus of dataflow networks with a standard structural
operational semantics.  A version of weak bisimulation equivalence,
called "buffer bisimilarity," is defined for this calculus, and its equational
theory is investigated.  The main result is a completeness theorem for proving
equations valid under buffer bisimilarity.  The axioms have a familiar,
category-theoretic flavor, in which a dataflow process with m input ports
and n output ports is represented by an arrow from m to n in a category
whose objects are the finite ordinals.