INTERLEAVING SEMANTICS AND ACTION REFINEMENT IN EVENT STRUCTURES
Weidong Tang1, 2, 3, Jinzhao Wu2, 3, Meiling Liu2, 4
1Chengdu Institute of Computer Applications, Chinese Academy of Sciences, Chengdu 610041, China
2School of Information Science and Engineering, Guangxi University for Nationalities, Nanning 530006, China
3Guangxi Key Laboratory of Hybrid Computation and IC Design Analysis, Nanning 530006, China
4Science Computing and Intelligent Information Processing of GuangXi higher education key laboratory，Nanning 530023, China
An event structure acts as a denotational semantic model of concurrent systems. Action refinement is an essential operation in the design of concurrent systems. But there exists an important problem about preserving equivalence under action refinement. If two processes are equivalent with each other, we hope that they still can preserve equivalence after action refinement. In linear time equivalence and branching time equivalence spectrum, interleaving equivalences, which include interleaving trace equivalence and interleaving bisimulation equivalence are not preserved under action refinement. In this paper, we define a class of concurrent processes with specific properties and put forward the concept of clustered action transition, which ensures that interleaving equivalences are able to preserve under action refinement.