Denotational Models Based on Synchronously Communicating Processes (Semantics, Programming Languages).

We initially establish a fundamental connection between the semantic theories of concurrency and communication in the works of de Bakker and Milner. We define a natural metric over Milner's rigid synchronization trees and show the resultant quotient space to be complete. For a finite alphabet, we show that our metric space is isometric to the solution to a domain equation investigated by de Bakker. For a countably infinite alphabet, the isometry between our space and an appropriate one constructed in the de Bakker style is demonstrated. We extend the results above to synchronization trees. An observation equivalence relation and a metric over a natural subclass of synchronization trees are defined and completeness is established. We define and establish continuity for a broad collection of process operations, although hiding, a nondeterministic operation used to support notions of parallel composition, fails to be well defined. We focus next on the hiding problem, giving it a completely satisfactory treatment within a Scott-Strachey style of denotational semantics. We develop three process models, illustrating a general technique in which we first construct a logic suitable for specifying general behavioral characteristics. We next apply Scott's theory of information systems to obtain a domain, and then interpret these abstract representations over synchronization trees, which provide the underlying semantic models for the logics. The first construction, the failog model, characterizes processes by what they can refuse to do. Our notion of process turns out to be more general than that of the failures model of Hoare, Brookes and Roscoe, a model which readily embeds into ours. Furthermore, unlike the failures model, our treatment of the hiding operation is completely adequate. Our two other models characterize different notions of acceptance behavior. In addition to refusals, acrelog deals with events that may be accepted, or are possible, and failsafe deals with events that must be accepted, or are safe. These models are compared to the acceptance-refusal machine model of Rounds and Brookes, which turns out to have characteristics of both constructions. Finally, we define the full range of process operations for our models, and , in all cases, hiding is treated satisfactorily.PhDComputer scienceUniversity of Michiganhttp://deepblue.lib.umich.edu/bitstream/2027.42/160133/1/8422236.pd