BISIMULATION SEMANTICS FOR CONCURRENCY WITH ATOMICITY AND ACTION REFINEMENT

Article type: Research Article

Authors: de Bakker, J.W. | de Vink, E.P.

Affiliations: CWI, Postbus 4079, NL-1009 AB Amsterdam & Vrij Universiteit | Department of Mathematics and Computer Science, Vrije Universiteit, De Boelelaan 1081a, NL-1081 HV Amsterdam

Abstract: A comparative semantic study is made of two notions in concurrency, viz. atomicity and action refinement. Parallel composition is modeled by interleaving, and refinement is taken in the version where actions are refined by atomized statements. The bisimulation domain used in the semantic definitions is obtained as solution of a system of domain equations over complete metric spaces. Both operational and denotational models are developed, and their equivalence is established using higher-order techniques and Banach’s fixed point theorem. The operational semantics for refinement is based on transition rules rather than on some form of syntactic substitution.

DOI: 10.3233/FI-1994-201231

Journal: Fundamenta Informaticae, vol. 20, no. 1,2,3, pp. 3-34, 1994