DERIVING COMPOSITIONAL MODELS FOR CONCURRENCY BASED ON DEBAKKER-ZUCKER METRIC DOMAIN FROM STRUCTURED OPERATIONAL SEMANTICS

This paper investigates the compositionality of operational models for concurrency induced by labeled transition systems (LTS's). These mode ls are defined on the basis of a metric domain first introduced by de Bakker and Zucker; the domain is a complete metric space consisting of tree-like structures called processes. Transition system specificatio ns (TSS's) define LTS's; the set of states of such a LTS A is the set of terms generated by a signature-SIGMA. For the syntactical operators F contained in SIGMA, semantic operations (on processes) associated w ith F are derived from the TSS S by which A is defined, provided that S satisfies certain syntactical restrictions. By means of these operat ions, the compositionality of the operational model induced by A is es tablished. A similar result was obtained by Rutten from TTS's which de fine finitely branching LTS's. The main contribution of this paper is generalization of Rutten's result to be applicable to TSS's which are based on applicative languages including recursion, parameterized stat ements, and value passing, and which define infinitely branching LTS's . A version of typed lambda-calculus incorporating mu-notation is empl oyed as a formalism for treating recursion, parameterized statements, and value-passing. Infinitely branching LTS's are needed to treat prog ramming languages including value passing such as CCS.