A Denotational Model for Mobile Point-to-Point Data-flow Networks with Channel Sharing

We present a fully abstract, denotational model for mobile, timed, nondeterministic data-flow networks whose components communicate in a point-to-point fashion. In this model components and networks of components are represented by sets of stream processing functions. Each stream processing function is required to be strongly pulse-driven and privacy preserving. A function is strongly pulse-driven if it is contractive with respect to the metric on streams. This property guarantees the existence of unique fix-points. The privacy preservation property can be thought of as an invariant specific to mobile point-to-point systems. Firstly, it guarantees that a function never accesses, depends on or forwards a port whose name it does not already know. Secondly, it guarantees that at the same point in time no port is known to more than two components, namely the sender and the receiver. Our model allows the description of a wide variety of networks; in particular, the description of unbounded nondeterministic networks. We demonstrate some features of our model by specifying a communication central.     «

We present a fully abstract, denotational model for mobile, timed, nondeterministic data-flow networks whose components communicate in a point-to-point fashion. In this model components and networks of components are represented by sets of stream processing functions. Each stream processing function is required to be strongly pulse-driven and privacy preserving. A function is strongly pulse-driven if it is contractive with respect to the metric on streams. This property guarantees the existence...     »