›› 2013,Vol. 28 ›› Issue (6): 1097-1105.doi: 10.1007/s11390-013-1400-y

• Special Section on Selected Paper from NPC 2011 • 上一篇    下一篇

ε-互模拟的无限演化机制

Yan-Fang Ma1 (马艳芳) and Min Zhang2, * (张敏)   

  • 收稿日期:2012-10-24 修回日期:2013-07-07 出版日期:2013-11-05 发布日期:2013-11-05
  • 作者简介:Yan-Fang Ma received her Ph.D. degree in computer science and technology from Software Engineering Institute in East China Normal University, Shanghai, in 2010. She is an associate professor in the School of Computer Science and Technology, Huaibei Normal University, China. Her research interests include formalization of software, semantics of program, and trustworthiness measure.

The Infinite Evolution Mechanism of ε-Bisimilarity

Yan-Fang Ma1 (马艳芳) and Min Zhang2, * (张敏)   

  1. 1 School of Computer Science and Technology, Huaibei Normal University, Huaibei 235000, China;
    2 Shanghai Key Laboratory of Trustworthy Computing, East China Normal University, Shanghai 200062, China
  • Received:2012-10-24 Revised:2013-07-07 Online:2013-11-05 Published:2013-11-05
  • Supported by:

    This work is supported by the National Natural Science Foundation of China under Grant Nos. 61021004, 61202105, 61300048, the Natural Science Foundation of Anhui Province of China under Grant No. 1308085QF117, the Natural Science Foundation of Universities of Anhui Province of China under Grant No. KJ2011A248, and the Open Fund of Shanghai Key Laboratory of Trustworthy Computing of China.

PDF (PC)

1146

为了形式化描述软件的动态正确性, 本文在概率进程代数基础上, 讨论了ε-互模拟的收敛机制. 首先, 提出ε-极限互模拟, 其描述了软件的规范和实现之间的动态关系, 列举一些ε-极限互模拟的例子. 其次, 建立ε-互模拟极限, 其描述了软件的规范在ε-互模拟下是其实现的极限形式, 证明了ε-互模拟极限的唯一性, 与ε-互模拟的相容性等性质. 最后, 为了说明软件的模块化开发和设计, 证明了ε-互模拟极限在各种进程复合算子下的可替换性.

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.

[1] Baeten J C,WeijlandWP. Process Algebra. New York, USA: Cambridge University Press, 1990.

[2] Hoare C A R. Communicating sequential processes. Communications of the ACM, 1978, 21(8): 666-677.

[3] Hoare C A R. Communicating Sequential Processes. New Jersey, USA: Prentice Hall, 1985.

[4] Milner R. Communication and Concurrency. New Jersey, USA: Prentice-Hall, 1989.

[5] Ying M S, Wirshing M. Approximate bisimilarity. In Proc. the 8th International Conference of Algebraic Methodology and Software Technology, May 2000, pp.309-322.

[6] Ying M S. Bisimulation indexes and their applications. Theoretical Computer Science, 2002, 275(1/2): 1-68.

[7] Ying M S. Topology in Process Calculus: Approximate Correctness and Infinite Evolution of Concurrency Programs. New York: Springer-Verlag, 2001.

[8] Segala R, Lynch N. Probabilistic simulations for probabilistic processes. In Proc. the 5th International Conference on Concurrency Theory, August 1994, pp.481-496.

[9] Deng Y X, van Glabbeek R, Hennessy M, Morgan C. Testing finitary probabilistic processes. In Proc. the 20th International Conference on Concurrency Theory, September 2009, pp.274-288.

[10] Song L, Deng Y X,Cai X J. Towards automatic measurement of probabilistic processes. In Proc. the 7th International Conference on Quality Software, Oct. 2007, pp.50-59.

[11] van Glabbeek R J, Smolka S A, Steffen B. Reactive, generative, and stratified models of probabilistic processes. Infromation and Computation, 1995, 121(1): 59-80.

[12] Larsen K G, Skou A. Bisimulation through probabilistic testing. Information and Computation, 1991, 94(1): 1-28.

[13] Larsen K G, Skou A. Compositional verification of probabilistic processes. In Proc. the 3rd International Conference on Concurrency Theory, August 1992, pp.456-471.

[14] Giacalone A, Jou C C, Smolka S A. Algebraic reasoning for probabilistic concurrent systems. In Proc. IFIP TC2 Working Conference on Programming Concepts and Methods, April 1990, pp.443-458.

[15] Smolka S A, Steffen B. Priority as extremal probability. In Proc. Theories of Concurrency: Unification and Extension, August 1990, pp.456-466.

[16] Milner R. Calculi for synchrony and asynchrony. Theoretical Computer Science, 1983, 25(3): 267-310.

[17] Ying M S. Additive models of probabilistic processes. Theoretical Computer Science, 2002, 275(1/2): 481-519.

[18] Ma Y F, Zhang M, Chen L. The infinite evolution mechanism of ε-bisimulation. In Proc. the 3rd International Conference on Quantitative Logic and Soft Computing, May 2012, pp.252-259.

[19] Engelking R. General Topology. Polish Science, 1977.

[20] Kelly J L. General Topology. Springer-Verlag, 1975.
No related articles found!
Viewed
Full text


Abstract

Cited
  Shared   
  Discussed   
No Suggested Reading articles found!
版权所有 © 《计算机科学技术学报》编辑部
本系统由北京玛格泰克科技发展有限公司设计开发 技术支持：support@magtech.com.cn
总访问量：