Report CS--R9031, pages 1-42 pp.. Amsterdam, The Netherlands: Centre for Mathematics and Computer Science, Department of Software Technology, July 1990.
Abstract: The aim of the paper is to propose a new model based on the posets with non-actions to describe the concurrent nondeterministic processes and to investigate their properties. The algebra SAFP2 of structured finite processes with three main operations for specifying sequentiality, concurrency and nondeterminism is introduced. Denotational semantics based on posets with non-actions is constructed for processes of SAFP2. Full abstractness of denotational semantics w.r.t. observational equivalence and proposed operational Petri net semantics is established.
Keywords: concurrent nondeterministic process (based on) posets (with) non-action(s); denotational semantics; observational equivalence; operational net semantics; occurrence net.