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. ``Determinate'' dataflow networks, which are composed of processes with functional input/output behavior, are a well-understood special case, whereas ``indeterminate'' networks, which can contain non-functional processes, still present some puzzles. In particular, the goal of discovering a useful and powerful logic for reasoning about indeterminate networks, has not yet been fully achieved. A step in the direction of such a logic is a formal theory called ``dataflow calculus''. The syntax of the calculus is designed to reflect in a natural way the mathematical structure that has seemed most important in previous semantic studies of dataflow networks. In previous research a soundness and completeness theorem has been proved for a set of equational axioms for dataflow networks, which shows that these axioms characterize an interesting notion of equivalence for dataflow networks. This research project is concerned with continuing the study of dataflow calculus, and its uses, as a concrete foundation on which to build a more powerful logic of dataflow networks, and as a tool for understanding better the relationship between the various abstract semantic models for dataflow networks.
