微信服务号

微信订阅号

2025-4-13- 5
Home > Archive>Volume 29, Issue 6, 2018 >1517-1526. DOI:10.13328/j.cnki.jos.005461
PDF HTML XML Export Cite reminder
Extension and Implementation of the Quasi-Local Algorithm for Checking Bisimilarity
Author:
Affiliation:

Fund Project:

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

  • Article
    • | |
  • Metrics
    • |
  • Reference [19]
    • |
  • Related
    • | | |
  • 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
    [1] Park D. Concurrency and automata on infinite sequences. In:Proc. of the GI-Conf. on Theoretical Computer Science. 1981. 167-183.[doi:10.1007/BFb0017309]
    [2] Milner R. Communication and Concurrency. Prentice-Hall, Inc., 1989.
    [3] Sangiorgi D. Introduction to Bisimulation and Coinduction. Cambridge University Press, 2011.
    [4] Dovier A, Piazza C, Policriti A. An efficient algorithm for computing bisimulation equivalence. Theoretical Computer Science, 2002,311(1-3):221-256.[doi:10.1016/S0304-3975(03)00361-X]
    [5] Fisler K, Vardi MY. Bisimulation minimization and symbolic model checking. Formal Methods in System Design, 2002,21(1):39-78.[doi:10.1023/A:1016091902809]
    [6] Fernandez JC, Mounier L. Verifying bisimulations on the fly. In:Proc. of the 3rd Int'l Conf. on Formal Description Techniques for Distributed Systems and Communication Protocols. North-Holland Publishing Co., 1990. 95-110.
    [7] Du WJ, Deng YX. A quasi-local algorithm for checking bisimilarity. In:Proc. of the IEEE Int'l Conf. on Computer Science and Automation Engineering. 2011. 1-5.[doi:10.1109/CSAE.2011.5952411]
    [8] The VLTS benchmark suite. http://cadp.inria.fr/resources/vlts/
    [9] Valmari A. Simple bisimilarity minimization in O(mlogn) time. Applications and Theory of Petri Nets, 2010,105(3):319-339.[doi:10.3233/FI-2010-369]
    [10] Garavel H, Lang F, Mateescu R, Serwe W. CADP 2011:A toolbox for the construction and analysis of distributed processes. Software Tools for Technology Transfer, 2013,15(2):89-107.[doi:10.1007/s10009-012-0244-z]
    [11] Groote JF, Wijs A. An O(mlogn) algorithm for stuttering equivalence and branching bisimulation. In:Proc. of the 22nd Int'l Conf. on Tools and Algorithms for the Construction and Analysis of Systems. LNCS 9636, Springer-Verlag, 2016. 607-624.[doi:10.1007/978-3-662-49674-9_40]
    [12] Wijs A. GPU accelerated strong and branching bisimilarity checking. In:Proc. of the 21st Int'l Conf. on Tools and Algorithms for the Construction and Analysis of Systems. LNCS 9035, Springer-Verlag, 2015. 368-383.[doi:10.1007/978-3-662-46681-0_29]
    [13] Dalsgaard AE, Enevoldsen S, Larsen KG, Srba J. Distributed computation of fixed points on dependency graphs. In:Proc. of the 2nd Int'l Symp. on Dependable Software Engineering:Theories, Tools, and Applications. LNCS 9984, Springer-Verlag, 2016. 197-212.[doi:10.1007/978-3-319-47677-3_13]
    [14] Kundu S, Lerner S, Gupta R. Validating high-level synthesis. In:Proc. of the 20th Int'l Conf. on Computer Aided Verification. LNCS 5123, Springer-Verlag, 2008. 459-472.[doi:10.1007/978-3-540-70545-1_44]
    [15] Hao KC, Ray S, Xie F. Equivalence checking for function pipelining in behavioral synthesis. In:Proc. of the DATE 2014. European Design and Automation Association, 2014. 1-6.[doi:10.7873/DATE.2014.163]
    [16] http://www.doc.ic.ac.uk/~jnm/LTSdocumention/AB_example.html
    [17] Wikipedia. https://en.wikipedia.org/wiki/Alternating_bit_protocol
    [18] Peralta JC, Gautier T, Besnard L, Guernic PL. LTS for Translation Validation of (multi-clocked) SIGNAL Specifications. IEEE, 2010.[doi:10.1109/MEMCOD.2010.5558632]
    [19] Fiacre. http://projects.laas.fr/fiacre/
    Related
    Cited by
    Comments
    Comments
    分享到微博
    Submit
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
Links:Institute of Software, CASChina Computer FederationCASNSFC
You are the first2034797Visitors
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