删除或更新信息,请邮件至freekaoyan#163.com(#换成@)

向量加法系统验证问题研究综述

本站小编 Free考研考试/2022-01-02

摘要:Petri网是形式化验证领域最重要的模型之一,具有重要的理论和应用价值.从验证算法分析的角度,Petri网可以被等价地抽象为向量加法系统.在对向量加法模型的研究中,人们又发展了一些重要的扩展模型.对近些年来国内外****在向量加法系统验证领域取得的成果进行了系统总结.首先给出了向量加法系统及几个关键验证问题的形式化定义,并重点总结了一般向量加法系统模型上可达性问题的最新研究进展和关键技术;接着总结了当限定模型的维度为固定值时相关研究进展,重点给出了2维情况的核心定理;随后介绍了几个重要扩展模型,并总结了这些模型上验证问题研究的最新进展.在每一部分,都对未来研究方向及可能面临的挑战进行了展望.



Abstract:Petri nets is a fundamental model in the area of formal verification. It is popular in both theoretical study and application. For the analysis of algorithmic properties of Petri nets, they are often equivalently viewed as vector addition systems. This survey gives a comprehensive review of the recent achievements in this area. First, formal definitions of the vector addition systems and their key verification problems are provided with emphasis on the discussion about reachability problem, including the latest results and the main proof techniques. Then the development on the case where the dimension is a constant number rather than a variable is summarized along with some key theorems which are fundamental to the current complexity results. Furthermore, as some important variants of vector addition systems have been proposed in recent years, a brief introduction is given to the motivation and definitions of some of the most representative ones, and the latest results on verification relating to these models. In addition, possible future work are highlighted at the end of each section.



PDF全文下载地址:

http://jos.org.cn/jos/article/pdf/5465
相关话题/系统 介绍 向量 加法 模型

  • 领限时大额优惠券,享本站正版考研考试资料!
    大额优惠券
    优惠券领取后72小时内有效,10万种最新考研考试考证类电子打印资料任你选。涵盖全国500余所院校考研专业课、200多种职业资格考试、1100多种经典教材,产品类型包含电子书、题库、全套资料以及视频,无论您是考研复习、考证刷题,还是考前冲刺等,不同类型的产品可满足您学习上的不同需求。 ...
    本站小编 Free壹佰分学习网 2022-09-19
  • 异构多智能体系统模型检查
    摘要:模型检查作为一种自动化系统验证方法,已被应用于多智能体系统的验证.由此延伸出的规约描述语言——交替时态逻辑(ATL),也被给予了高度关注.根据智能体是否可以看到全局信息,分为不完全信息和完全信息;根据智能体是否可以记录历史信息,分为无记忆能力和无限记忆能力,提出了4种经典的策略类型.这些策略类 ...
    本站小编 Free考研考试 2022-01-02
  • 一种嵌套中断系统的建模和分析方法
    摘要:在嵌入式系统和各类操作系统中,中断机制是确保实时响应各类异步事件的重要方法.通常在处理一个中断事件的过程中,往往会有更紧迫的中断事件请求响应,因而发生中断嵌套.建模并验证嵌套中断系统是具有挑战性的工作.提出一种建模和验证嵌套中断系统的方法.首先,提出基于投影时序逻辑(projectiontem ...
    本站小编 Free考研考试 2022-01-02
  • 机器人关节通信总线系统的建模与验证
    摘要:高速串行现场总线(controllerareanetwork,简称CAN)被广泛部署到机器人通信系统中.而服务机器人任务具有并发性和高实时性的特点,因此,如何根据总线协议规范和应用需求精化设计模型,保证系统设计的正确性和实时性要求,避免设计阶段的漏洞十分必要.针对传统方法的局限性,提出使用形式 ...
    本站小编 Free考研考试 2022-01-02
  • 基于条件概率模型的缺陷定位方法
    摘要:缺陷定位是软件调试的重要阶段,依赖程序频谱信息实现软件缺陷定位,是当前比较行之有效的方法.基于频谱缺陷定位方法应用的前提是,程序频谱和执行结果之间存在的潜在关联.通过经验性分析两者之间的内在关联,借助于统计学的条件概率思想,构建了用以量化分析两者关系强弱的P模型,并基于此提出了基于条件概率的缺 ...
    本站小编 Free考研考试 2022-01-02
  • 医学影像计算机辅助检测与诊断系统综述
    摘要:计算机辅助检测/诊断(computer-aideddetection/diagnosis,简称CAD)能够提高诊断的准确性,减少假阳性的产生,为医生提供有效的诊断决策支持.旨在分析计算机辅助诊断工具的最新发展.以CAD研究较多的四大致命性癌症的发病医学部位为主线,按照不同的成像技术和病类,对目 ...
    本站小编 Free考研考试 2022-01-02
  • 基于同态加密系统的图像鲁棒可逆水印算法
    摘要:同态加密技术可用于保护数据隐私并允许对密文数据进行算术操作,在云计算安全上有着很好的应用前景.针对云计算中的隐私保护和数据安全等问题,提出了一种基于同态加密系统的图像鲁棒可逆水印算法,主要思想为:(1)对原始图像进行分块和利用Paillier加密系统进行加密得到密文图像;(2)在加密域中,通过 ...
    本站小编 Free考研考试 2022-01-02
  • 基于创意序列学习的艺术风格学习与绘制系统
    摘要:在众多传统艺术绘画形式中,笔触是被现代计算机绘画工具(GIMP、Photoshop和Painter)普遍采用的形式之一.创新性地提出了服务于非真实感渲染AI辅助艺术创作系统(A4).系统能够实现自动生成特定艺术家风格的笔触效果.该系统在强化学习框架下,主要进行以下研究工作:(1)提出基于PGP ...
    本站小编 Free考研考试 2022-01-02
  • 分布式图处理系统技术综述
    摘要:图作为一种基本的数据类型,是对现实世界中对象及其关联关系的一种抽象.现实中,许多科学问题都可以被模型化为图的问题,因此,对图数据进行分析非常重要.图数据分析在语义Web分析、社交网络、生物基因分析以及信息检索等领域有着广泛的应用.随着移动互联、物联网等信息技术的发展,图数据的规模处于持续增长的 ...
    本站小编 Free考研考试 2022-01-02
  • 基于边采样的网络表示学习模型
    摘要:近年来,以微博、微信、Facebook为代表的社交网络不断发展,网络表示学习引起了学术界和工业界的广泛关注.传统的网络表示学习模型利用图矩阵表示的谱特性,由于其效率低下、效果不佳,难以应用到真实网络中.近几年,基于神经网络的表示学习方法因算法效率高、较好地保存了网络结构信息,逐渐成为网络表示学 ...
    本站小编 Free考研考试 2022-01-02
  • 基于向量引用Platform-Oblivious内存连接优化技术
    摘要:以MapD为代表的图分析数据库系统通过GPU、Phi等新型众核处理器来支持高性能分析处理,在面向复杂数据模式时,连接操作仍然是重要的性能瓶颈.近年来,异构处理器逐渐成为高性能计算的主流平台,内存连接性能的研究从多核CPU平台扩展到新兴的众核处理器,但众多的研究成果并未系统地揭示连接算法性能、连 ...
    本站小编 Free考研考试 2022-01-02