Istituto di Scienza e Tecnologie dell'Informazione     
Degano P., De Nicola R., Montanari U. Observational equivalences for concurrency models. In: 3rd Working Conference on the Formal Description of Programming Concepts (Ebberup, Denmark, 25 - 28 August 1986). Proceedings, pp. 105 - 132. Martin Wirsing (ed.). North-Holland, 1986.
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.

Icona documento 1) Download Document PDF

Icona documento Open access Icona documento Restricted Icona documento Private


Per ulteriori informazioni, contattare: Librarian http://puma.isti.cnr.it

Valid HTML 4.0 Transitional