A Denotational Model for Mobile Many-to-Many Data-flow Networks

We present a fully abstract, denotational model for mobile, timed, nondeterministic data-flow networks whose components communicate in a many-to-many 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 guarded and generic. A stream processing function is strongly guarded if it is contractive with respect to the standard metric on streams. This property guarantees the existence of unique fix-points. The genericity property can be thought of as an invariant, or alternatively, a privacy requirement, that is satisfied by any mobile system. It guarantees that a function never accesses, depends on or forwards a port whose name it does not already know. 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 mobile telephone network.     «

We present a fully abstract, denotational model for mobile, timed, nondeterministic data-flow networks whose components communicate in a many-to-many 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 guarded and generic. A stream processing function is strongly guarded if it is contractive with respect to the standard metric on streams. This property guarantees the existe...     »