Extension and Implementation of the Quasi-Local Algorithm for Checking Bisimilarity
Author:
Affiliation:

Clc Number:

Fund Project:

National Natural Science Foundation of China (61672229, 61261130589); Natural Science Foundation of Shanghai, China (16ZR1409100)

  • Article
  • |
  • Figures
  • |
  • Metrics
  • |
  • Reference
  • |
  • Related
  • |
  • Cited by
  • |
  • Materials
  • |
  • Comments
    Abstract:

    Bisimilarity plays an important role in the analysis and verification of concurrent systems. In this paper, an optimization of the quasi-local algorithm of Du and Deng is proposed to make it applicable for general labeled transition systems. Both the optimized algorithm and the local algorithm of Fernandez and Mounier are implemented in Java, and experiment using the VLTS benchmark suite shows the former outperforms the latter in most cases. The algorithms are also modified to check similarity. Finally, a procedure for transforming labeled transition systems is implemented to facilitate checking weak bisimilarity.

    Reference
    Related
    Cited by
Get Citation

郑晓琳,邓玉欣,付辰,雷国庆.互模拟准局部验证算法的扩展与实现.软件学报,2018,29(6):1517-1526

Copy
Share
Article Metrics
  • Abstract:
  • PDF:
  • HTML:
  • Cited by:
History
  • Received:June 28,2017
  • Revised:September 01,2017
  • Adopted:November 06,2017
  • Online: December 28,2017
  • Published:
You are the firstVisitors
Copyright: Institute of Software, Chinese Academy of Sciences Beijing ICP No. 05046678-4
Address:4# South Fourth Street, Zhong Guan Cun, Beijing 100190,Postal Code:100190
Phone:010-62562563 Fax:010-62562533 Email:jos@iscas.ac.cn
Technical Support:Beijing Qinyun Technology Development Co., Ltd.

Beijing Public Network Security No. 11040202500063