A Truly Concurrent Semantics for a Simple Parallel Programming Language

Abstract. This paper represents the beginning of a study aimed at devising semantic models for true concurrency that provide clear distinctions between concurrency, parallelism and choice. We present a simple programming language which includes (weakly) sequential composition, asynchronous and synchronous parallel composition, a restriction operator, and that supports recursion. We develop an operational and a denotational semantics for this language, and we obtain a congruence theorem relating the behavior of a process as described by the transition system to the meaning of the process in the denotational model. This implies that the denotational model is adequate with respect to the operational model. Our denotational model is based on the resource traces of Gastin and Teodesiu, and since a single resource trace represents all possible executions of a concurrent process, we are able to model each term of our concurrent language by a single trace. Therefore we obtain a deterministic s...

• Type: Conference
• Year: 1999
• Where: CSL
• Authors: Paul Gastin, Michael W. Mislove
• Keywords: Automated Reasoning, CSL 1999, Denotational Model, Denotational Semantics, Synchronous Parallel Composition