Transition systems, metric spaces and ready sets in the semantics of uniform concurrency

摘要

Transition systems as proposed by Hennessy and Plotkin are defined for a series of three languages featuring concurrency. The first has shuffle and local nondeterminacy, the second synchronization merge and local nondeterminacy, and the third synchronization merge and global nondeterminacy. The languages are all uniform in the sense that the elementary actions are uninterpreted. Throughout, infinite behaviour is taken into account and modelled with infinitary languages in the sense of Nivat. A comparison with denotational semantics is provided. For the first two languages, a linear time model suffices; for the third language a branching time model with processes in the sense of de Bakker and Zucker is described. In the comparison an important role is played by an intermediate semantics in the style of Hoare and Olderog's specification oriented semantics. A variant on the notion of ready set is employed here. Precise statements are given relating the various semantics terms of a number of abstraction operators.