Split and ST Bisimulation Semantics

In this paper the notion of action atomicity is relaxed by permitting actions to be observed in the middle of their evolution. Non-atomic semantic equivalences, based on the notion of bisimulation, are studied over stable event structures, Split n bisimulation equivalence (denoted ∼ n considers each event as composed of n phases. ST bisimulation equivalence (denoted ∼ ST ) is a slight refinement of ∼ 2 where each ending phase is unambiguously associated to a beginning phase, We prove that, by increasing n , we get finer and finer equivalences (i.e., ∼ n + 1 ⊆ ∼ n ) and, moreover, that ∼ n + 1 coincides with ∼ ST over those event structures whose autoconcurrency is at most n . The main consequence of these results is that, for image finite event structures, ∼ ST is the intersection of all the ∼ n .