Infinite streams and finite observations in the semantics of uniform concurrency (Q1091800)

Two ways of assigning meaning to a language with uniform concurrency are presented and compared. The language has uninterpreted elementary actions from which statements are composed using sequential, alternative and parallel composition (with communication), and recursion. The first semantics uses infinite streams, the second one uses finite observations. It is shown that the two models are isomorphic, which induces an equivalence result between the two semantics. Furthermore, a definition of the hiding operation which is inspired by the infinite streams approach is presented, and its continuity is proved within the framework of finite observations. It has also been proven possible to show continuity of the hiding operator within the framework of infinite streams in an independent way; this line has been pursued in [\textit{J.-J. Ch. Meyer} and \textit{E.-R. Olderog}, Hiding in stream semantics of uniform concurrency, Rep. IR-125, Free Univ., Amsterdam (1987)]. Related to this work is the paper [\textit{J. W. de Bakker} and \textit{J.-J. Ch. Meyer}, Acta Inf. 24, 491-511 (1987; Zbl 0607.68014)], in which it is proved that stream semantics for a language without hiding operator can be dealt with both in a metric and in an order-theoretic setting. In [Meyer/Olderog, loc. cit.], however, it is shown that stream semantics for a language with hiding operator can only be given an adequate base in an order-theoretic way.