A Proof System for Dataflow Networks with Indeterminate Modules

Abstract

In this paper we discuss a model for dataflow networks containing indeterminate operators and the associated proof system. The model is denotational and associates with each network the set of possible behaviors. The possible behaviors are represented by traces. The novel feature of our proof system is that we give an inductive proof rule for recursively defined networks based on a fixed point construction given by Keller and Panangaden. We show soundness and relative completeness of our proof system.