Abstract
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.
| Original language | English |
|---|---|
| Pages (from-to) | 1097-1105 |
| Number of pages | 9 |
| Journal | Journal of Computer Science and Technology |
| Volume | 28 |
| Issue number | 6 |
| DOIs | |
| State | Published - Nov 2013 |
Keywords
- convergence mechanism
- correctness of software
- probabilistic process algebra
- ε-bisimulation