摘要:互模拟是并发系统分析和验证的一个重要概念.主要扩展了一种由Du和Deng提出的准局部算法，使其更加适用于一般的标记迁移系统.用Java实现扩展后的准局部算法与Fernandez和Mounier提出的局部算法.以VLTS为实验数据基准进行大量的实验，发现在大多数情况下，前者的性能比后者更好.同时，修改了算法使其能够验证模拟关系.最后，用Java实现对标记迁移系统进行转换，使算法同时可以验证弱互模拟关系.
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.
PDF全文下载地址:
http://jos.org.cn/jos/article/pdf/5461
删除或更新信息，请邮件至freekaoyan#163.com(#换成@)
互模拟准局部验证算法的扩展与实现
本站小编 Free考研考试/2022-01-02
相关话题/实验 系统 数据 算法 局部
领限时大额优惠券,享本站正版考研考试资料!
优惠券领取后72小时内有效，10万种最新考研考试考证类电子打印资料任你选。涵盖全国500余所院校考研专业课、200多种职业资格考试、1100多种经典教材，产品类型包含电子书、题库、全套资料以及视频，无论您是考研复习、考证刷题，还是考前冲刺等，不同类型的产品可满足您学习上的不同需求。 ...考试优惠券 本站小编 Free壹佰分学习网 2022-09-19自动分析递归数据结构的归纳性质
摘要:提出了一种对递归数据结构的归纳性质进行自动化分析的框架.工作分为3个主要部分.首先，它将递归数据结构的归纳性质分为两个主要类别，并提出对应的处理模式，从而帮助简化对于程序中的递归数据结构上的相关性质的分析.其次，提出了一种称为分割与拼接的技术来发现和描述递归数据结构是如何被程序修改的：递归数据 ...中科院软件研究所 本站小编 Free考研考试 2022-01-02异构多智能体系统模型检查
摘要:模型检查作为一种自动化系统验证方法，已被应用于多智能体系统的验证.由此延伸出的规约描述语言——交替时态逻辑（ATL），也被给予了高度关注.根据智能体是否可以看到全局信息，分为不完全信息和完全信息；根据智能体是否可以记录历史信息，分为无记忆能力和无限记忆能力，提出了4种经典的策略类型.这些策略类 ...中科院软件研究所 本站小编 Free考研考试 2022-01-02向量加法系统验证问题研究综述
摘要:Petri网是形式化验证领域最重要的模型之一，具有重要的理论和应用价值.从验证算法分析的角度，Petri网可以被等价地抽象为向量加法系统.在对向量加法模型的研究中，人们又发展了一些重要的扩展模型.对近些年来国内外****在向量加法系统验证领域取得的成果进行了系统总结.首先给出了向量加法系统及几 ...中科院软件研究所 本站小编 Free考研考试 2022-01-02一种嵌套中断系统的建模和分析方法
摘要:在嵌入式系统和各类操作系统中，中断机制是确保实时响应各类异步事件的重要方法.通常在处理一个中断事件的过程中，往往会有更紧迫的中断事件请求响应，因而发生中断嵌套.建模并验证嵌套中断系统是具有挑战性的工作.提出一种建模和验证嵌套中断系统的方法.首先，提出基于投影时序逻辑（projectiontem ...中科院软件研究所 本站小编 Free考研考试 2022-01-02基于类型理论的领域数据建模和验证及案例
摘要:数据作为软件系统的主要处理对象，其规范性有助于软件系统的设计开发和软件系统之间的数据交换.面向行业数据规范及其验证，提出了一种基于类型理论的领域数据建模语言（DDML）和领域建模方法（DDMM）.DDML语言通过定义类型和项的语法和语义，描述领域数据类型和对象的结构，通过定义类型规则及其类型检 ...中科院软件研究所 本站小编 Free考研考试 2022-01-02机器人关节通信总线系统的建模与验证
摘要:高速串行现场总线（controllerareanetwork，简称CAN）被广泛部署到机器人通信系统中.而服务机器人任务具有并发性和高实时性的特点，因此，如何根据总线协议规范和应用需求精化设计模型，保证系统设计的正确性和实时性要求，避免设计阶段的漏洞十分必要.针对传统方法的局限性，提出使用形式 ...中科院软件研究所 本站小编 Free考研考试 2022-01-02MapReduce与Spark用于大数据分析之比较
摘要:评述了MapReduce与Spark两种大数据计算算法和架构，从背景、原理以及应用场景进行分析和比较，并对两种算法各自优点以及相应的限制做出了总结.当处理非迭代问题时，MapReduce凭借其自身的任务调度策略和shuffle机制，在中间数据传输数量以及文件数目方面的性能要优于Spark；而在 ...中科院软件研究所 本站小编 Free考研考试 2022-01-02医学影像计算机辅助检测与诊断系统综述
摘要:计算机辅助检测/诊断（computer-aideddetection/diagnosis，简称CAD）能够提高诊断的准确性，减少假阳性的产生，为医生提供有效的诊断决策支持.旨在分析计算机辅助诊断工具的最新发展.以CAD研究较多的四大致命性癌症的发病医学部位为主线，按照不同的成像技术和病类，对目 ...中科院软件研究所 本站小编 Free考研考试 2022-01-02数据外补偿的深度网络超分辨率重建
摘要:单张图像超分辨率重建受到多对一映射的困扰.对于给定的低分辨率图像块，存在若干高分辨率图像块与之对应.基于学习的方法受此影响，学习到的逆映射规则只能预测这些高分辨率图像块的均值，从而产生视觉上模糊的超分辨率重建结果.为了弥补歧义性造成的高频细节损失，提出了一种基于深度网络、利用在线检索的数据进行 ...中科院软件研究所 本站小编 Free考研考试 2022-01-02多媒体大数据处理与分析专题前言
摘要:Abstract:PDF全文下载地址:http://jos.org.cn/jos/article/pdf/5417 ...中科院软件研究所 本站小编 Free考研考试 2022-01-02
