| 互模拟准局部验证算法的扩展与实现 |
| |
| 引用本文： | 郑晓琳,邓玉欣,付辰,雷国庆.互模拟准局部验证算法的扩展与实现[J].软件学报,2018,29(6):1517-1526. |
| |
| 作者姓名： | 郑晓琳 邓玉欣 付辰 雷国庆 |
| |
| 作者单位： | 上海市高可信计算重点实验室(华东师范大学), 上海 200062,上海市高可信计算重点实验室(华东师范大学), 上海 200062,计算机科学国家重点实验室(中国科学院软件研究所), 北京 100080,上海市高可信计算重点实验室(华东师范大学), 上海 200062 |
| |
| 基金项目： | 国家自然科学基金（61672229，61261130589）；上海市自然科学基金（16ZR1409100）资助。 |
| |
| 摘 要： | 互模拟是并发系统的分析和验证的一个重要概念。本文主要扩展了一种由Du和Deng提出的准局部算法，使其更加适用于一般的标记迁移系统。我们用Java实现扩展后的准局部算法与Fernandez和Mounier提出的局部算法。我们以VLTS为实验数据基准，进行大量的实验，发现在大多数情况下，前者的性能比后者更好。同时，我们修改了算法使其能够验证模拟关系。最后，我们用Java实现对标记迁移系统进行转换，使算法同时可以验证弱互模拟关系。
|
| 关 键 词： | 互模拟 算法 标记迁移系统 扩展 |
| 收稿时间： | 2017/6/28 0:00:00 |
| 修稿时间： | 2017/9/1 0:00:00 |
Extension and Implementation of the Quasi-Local Algorithm for Checking Bisimilarity |
| |
| ZHENG Xiao-Lin,DENG Yu-Xin,FU Chen and LEI Guo-Qing.Extension and Implementation of the Quasi-Local Algorithm for Checking Bisimilarity[J].Journal of Software,2018,29(6):1517-1526. |
| |
| Authors: | ZHENG Xiao-Lin DENG Yu-Xin FU Chen and LEI Guo-Qing |
| |
| Affiliation: | Shanghai Key Laboratory of Trustworthy Computing, East China Normal University, Shanghai 200062, China,Shanghai Key Laboratory of Trustworthy Computing, East China Normal University, Shanghai 200062, China,State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences, Beijing 100080, China and Shanghai Key Laboratory of Trustworthy Computing, East China Normal University, Shanghai 200062, China |
| |
| Abstract: | Bisimilarity plays an important role in the analysis and verification of concurrent systems. In this paper, we propose an optimization of the quasi-local algorithm of Du and Deng, so that it is applicable for general labeled transition systems. We implement both the optimized algorithm and the local algorithm of Fernandez and Mounier in Java, and find that the former outperforms the latter in most cases, based on our experiment using the VLTS benchmark suite. We have also modified the algorithms to check similarity, for which similar phenomenon has been observed. Finally, we implement a procedure for transforming labeled transition systems, which allows us to check weak bisimilarity. |
| |
| Keywords: | Bisimulation algorithm labeled transition system optimization weak bisimulation |
|
| 点击此处可从《软件学报》浏览原始摘要信息 |
|
点击此处可从《软件学报》下载全文 |
|
