24. Interleaving semantics and action refinement with atomic choice

I. Czaja (GMD), R.J. van Glabbeek (Stanford) & U. Goltz (GMD)

November 1991

We investigate how to restrict the concept of action refinement such that established interleaving equivalences for concurrent systems are preserved under these restricted refinements. We show that interleaving bisimulation is preserved under refinement if we do not allow to refine action occurrences deciding choices and action occurrences involved in autoconcurrency. On the other hand, interleaving trace equivalence is still not preserved under these restricted refinements.
KEYWORDS: Concurrency, event structures, semantic equivalences, interleaving vs. partial orders, bisimulation, action refinement, atomicity.