Bisimulation semantics for concurrency with atomicity and action refinement

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.