Operational and Denotational Semantics with Explicit Concurrency

Article type: Research Article

Authors: Broy, Manfred

Affiliations: Institut für Informatik, Technische Universität München, Postfach 20 24 20, D-8 München

Abstract: The semantics of a simple language for describing tightly coupled “synchronous” systems is defined in terms of action structures representing histories of computations with explicit concurrency. An operational semantics is defined by term rewriting rules labelled by action structures. A consistent denotational semantics in terms of action structures is defined based on the concept of observable behaviour and on fixpoint theory. A fully abstract denotational semantics is given. In particular, the issue of interleaving semantics versus semantics including explicit concurrency is discussed.

DOI: 10.3233/FI-1992-163-402

Journal: Fundamenta Informaticae, vol. 16, no. 3-4, pp. 201-229, 1992