Infinite Streams and Finite Observations in the Semantics of Uniform Concurrency

摘要

Two ways of assigning meaning to a language with uniform concurrency are compared. The language has uninterpreted elementary actions from which statements are composed using sequential composition, nondeterministic choice, parallel composition with communication, and recursion. The first semantics uses infinite streams in the sense which is a refinement of the linear time semantics of De Bakker et al. The second semantics uses the finite observations of Hoare et al., situated in between the divergence and readiness semantics of Olderog & Hoare. It is shown that the two models are isomorphic and that this isomorphism induces an equivalence result between the two semantics. The hiding operation inspired by the infinite streams approach is defined. The continuity of this operation is proved in the framework of finite observations.