Step semantics and action refinement in event structures
Weidong Tang 1, 2, 3, Jinzhao Wu 1, 2, 3, Meiling Liu 1, 4
COMPUTER MODELLING & NEW TECHNOLOGIES 2014 18(5) 94-101
1School of Information Science and Engineering, Guangxi University for Nationalities, Nanning 530006, China
2Chengdu Institute of Computer Applications, Chinese Academy of Sciences, Chengdu 610041, 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. However, 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, step equivalences, which include step trace equivalence and step bisimulation equivalence are not preserved under action refinement [17]. 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 step equivalences are able to preserve under action refinement.