TY - JOUR
T1 - The infinite evolution mechanism of ε-Bisimilarity
AU - Ma, Yan Fang
AU - Zhang, Min
PY - 2013/11
Y1 - 2013/11
N2 - In this paper, we focus on the convergence mechanism of ε-bisimulation under probabilistic processes to discuss the dynamic correctness of the software. Firstly, ε-limit bisimulation is defined for reflecting the dynamic relation between software specification and implementation. Some special ε-limit bisimulations are showed. Secondly, ε-bisimulation limit is proposed, which states the specification is the limit of implementation under ε-bisimulation. The uniqueness of ε-bisimulation limit and consistence with ε-bisimulation are presented. Finally, the substitutivity laws of ε-bisimulation limit with various combinators are proved.
AB - In this paper, we focus on the convergence mechanism of ε-bisimulation under probabilistic processes to discuss the dynamic correctness of the software. Firstly, ε-limit bisimulation is defined for reflecting the dynamic relation between software specification and implementation. Some special ε-limit bisimulations are showed. Secondly, ε-bisimulation limit is proposed, which states the specification is the limit of implementation under ε-bisimulation. The uniqueness of ε-bisimulation limit and consistence with ε-bisimulation are presented. Finally, the substitutivity laws of ε-bisimulation limit with various combinators are proved.
KW - convergence mechanism
KW - correctness of software
KW - probabilistic process algebra
KW - ε-bisimulation
UR - https://www.scopus.com/pages/publications/84890381330
U2 - 10.1007/s11390-013-1400-y
DO - 10.1007/s11390-013-1400-y
M3 - 文章
AN - SCOPUS:84890381330
SN - 1000-9000
VL - 28
SP - 1097
EP - 1105
JO - Journal of Computer Science and Technology
JF - Journal of Computer Science and Technology
IS - 6
ER -