Refinement Theorem for St-Bisimulation Semantics

摘要

ST-configurations to represent all the states of concurrent systems areintroduced. ST-bisimulation equivalence is proved to be preserved under refinement of actions. This implies that it is possible to abstract from the causal structure of concurrent systems without assuming action atomicity.