Observational equivalences for concurrency models

Certain node-labelled trees, called NMS's, are introduced as a framework for dealing with various observational equivalences for concurrent systems. An NMS consists of the finite and infinite computations (ordered by prefix) of a transition system. The label of a node is the observation performed on the corresponding computation. A notion of NMS observational eqnivalence is introduced as the maximal bisimulation. Depending on the labels we can capture different equivalences. Milner's CCS is used as a test case for our approach. Both an interleaving and a partial ordering observation for CCS computations are defined, thus inducing two equivalences on CCS agents. In the former case the induced equivalence coincides with Milner's observational equivalence, while in the latter case it is finer exact1y in that it distinguishes interleaving of sequential nondeterministic processes from their concurrent execution.