Compositional relational semantics for indeterminate dataflow networks

Given suitable categories T, C and functor F: T → C, if X,Y are objects of T, then we define an (X,Y)-relation in C to be a triple (formula presented), where R is an object of C and r: R → FX and (formula presented) are morphisms of C. We define an algebra of relations in C, including operations of “relabeling,” “sequential composition,” “parallel composition,” and “feedback,” which correspond intuitively to ways in which processes can be composed into networks. Each of these operations is defined in terms of composition and limits in C, and we observe that any operations defined in this way are preserved under the mapping from relations in C to relations in C′ induced by a continuous functor G: C → C′. To apply the theory, we defined a category Auto of concurrent automata, and we give an operational semantics of dataflow-like networks of processes with indeterminate behaviors, in which a network is modeled as a relation in Auto. We then define a category EvDom of “event domains,” a (non-full) subcategory of the category of Scott domains and continuous maps, and we obtain a coreflection between Auto and EvDom. It follows, by the limit-preserving properties of coreflectors, that the denotational semantics in which dataflow networks are represented by relations in EvDom, is “compositional” in the sense that the mapping from operational to denotational semantics preserves the operations on relations. Our results are in contrast to examples of Brock and Ackerman, which imply that no compositional semantics is possible in terms of set-theoretic relations.