互模拟准局部验证算法的扩展与实现

作者：郑晓琳; 邓玉欣; 付辰; 雷国庆

来源：软件学报, 2018, (06): 1517-1526.

• 互模拟
• 标记迁移系统
• 扩展 bisimulation
• labeled transition system
• optimization
• weak bisimulation

互模拟是并发系统分析和验证的一个重要概念.主要扩展了一种由Du和Deng提出的准局部算法,使其更加适用于一般的标记迁移系统.用Java实现扩展后的准局部算法与Fernandez和Mounier提出的局部算法.以VLTS为实验数据基准进行大量的实验,发现在大多数情况下,前者的性能比后者更好.同时,修改了算法使其能够验证模拟关系.最后,用Java实现对标记迁移系统进行转换,使算法同时可以验证弱互模拟关系.

• 单位
  华东师范大学; 中国科学院