PUMA
Istituto di Scienza e Tecnologie dell'Informazione     
Degano P., De Nicola R., Montanari U. Partial orderings descriptions and observations of nondeterministic concurrent processes. In: Linear Time, Branching Time and Partial Order in Logics and Models for Concurrency (Noordwijkerhout, The Netherlands, May/June 1989). Proceedings, pp. 438 - 466. J.W. De Bakker (ed.). Springer-Verlag, 1989.
 
 
Abstract
(English)
A methodology is introduced for defining concurrent semantics of processes as equivalence c1asses of Labelled Event Structures (LES). The construction of a les providing the operational semantics of systems consists of three main steps. First, systems are decomposed into sets of sequential processes and a set of rewriting rules is introduced which describe both the actions sequential processes may perform and their causal relation. Then, the rewriting rules are used to build an occurrence net. Finally, the required event structure is easily derived from the occurrence net. As a test case, a partial ordering operational semantics is introduced first for a subset of Milner's CCS and then for the whole calculus. The proposed semantics are consistent with the original interleaving semantics of the calculus and are able to capture all and only the parallelism present in its multiset semantics. In order to obtain more abstract semantic definitions, new notions of observational equivalence on Labelled Event Structures are introduced that preserve both concurrency and nondeterminism.
Subject Semantics of programming languages
Communicating processes
Observational equivalence
Concurrency
Nondeterminism
CCS
LES


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