Infinite Streams and Finite Observations in the Semantics of Uniform Concurrency (Preliminary Version)

摘要

Two ways of assigning meaning to a programming 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 between the divergence and readiness semantics of Olderog and Hoare. It is shown that the two models are isomorphic and that this isomorphism induces an equivalence result between the two semantics.