文献类型：会议论文

英文题名：Uniform Random Process Model Revisited

作者：Zhang, Wenbo[1];Long, Huan[1];Xu, Xian[2]

机构：[1]Shanghai Jiao Tong Univ, BASICS, Shanghai, Peoples R China;[2]East China Univ Sci & Technol, Shanghai, Peoples R China

会议论文集：17th Asian Symposium on Programming Languages and Systems (APLAS)

会议日期：DEC 01-04, 2019

会议地点：Bali, INDONESIA

语种：英文

摘要：Recently, a proper bisimulation equivalence relation for random process model has been defined in a model independent approach. Model independence clarifies the difference between nondeterministic and probabilistic actions in concurrency and makes the new equivalence relation to be congruent. In this paper, we focus on the finite state randomized CCS model and deepen the previous work in two aspects. First, we show that the equivalence relation can be decided in polynomial time. Second, we give a sound and complete axiomatization system for this model. The algorithm and axiomatization system also have the merit of model independency as they can be easily generalized to the randomized extension of any finite state concurrent model.