An extensional fixed-point semantics for nondeterministic data flow (Q1183593)

The first part of the paper is devoted to the deterministic case: basic domains, deterministic processes, operators used to model networks and a behaviour equivalence relation over deterministic processes are defined. The behaviour equivalence is shown to be preserved under the network construction. In section 6 a translation from the nondeterministic level to the deterministic one is defined and the associativity of a nondeterministic network construction is proved. Further it is shown that the modelling is extensional: if nondeterministic processes \(P_ 1,P_ 2\) exhibit the same nondeterministic input-output behaviours in all nondeterministic contexts, then \(P_ 1=P_ 2\). An alternative metric space framework is presented as well and the paper concludes with the comparison of the work with that of \textit{D. Park} [Math. Cent. Tracts 159, 133-161 (1983; Zbl 0527.68012)].