主页期刊介绍编委会编辑部服务介绍道德声明在线审稿编委办公编辑办公English
2018-2019年专刊出版计划 微信服务介绍 最新一期:2018年第12期
     
在线出版
各期目录
纸质出版
分辑系列
论文检索
论文排行
综述文章
专刊文章
美文分享
各期封面
E-mail Alerts
RSS
旧版入口
中国科学院软件研究所
  
投稿指南 问题解答 下载区 收费标准 在线投稿
张文博,龙环.向量加法系统验证问题研究综述.软件学报,2018,29(6):1566-1581
向量加法系统验证问题研究综述
State-of-the-Art Survey on Verification of Vector Addition Systems
投稿时间:2017-07-01  修订日期:2017-09-01
DOI:10.13328/j.cnki.jos.005465
中文关键词:  Petri网  向量加法系统  可达性  形式化验证  算法复杂性
英文关键词:Petri nets  vector addition systems  reachability  formal verification  complexity
基金项目:国家自然科学基金(61472239,61772336,61572318)
作者单位E-mail
张文博 上海交通大学 软件学院, 上海 200240  
龙环 上海交通大学 计算机科学与工程系, 上海 200240 longhuan@sjtu.edu.cn 
摘要点击次数: 798
全文下载次数: 476
中文摘要:
      Petri网是形式化验证领域最重要的模型之一,具有重要的理论和应用价值.从验证算法分析的角度,Petri网可以被等价地抽象为向量加法系统.在对向量加法模型的研究中,人们又发展了一些重要的扩展模型.对近些年来国内外学者在向量加法系统验证领域取得的成果进行了系统总结.首先给出了向量加法系统及几个关键验证问题的形式化定义,并重点总结了一般向量加法系统模型上可达性问题的最新研究进展和关键技术;接着总结了当限定模型的维度为固定值时相关研究进展,重点给出了2维情况的核心定理;随后介绍了几个重要扩展模型,并总结了这些模型上验证问题研究的最新进展.在每一部分,都对未来研究方向及可能面临的挑战进行了展望.
英文摘要:
      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.
HTML  下载PDF全文  查看/发表评论  下载PDF阅读器
 

京公网安备 11040202500064号

主办单位:中国科学院软件研究所 中国计算机学会
编辑部电话:+86-10-62562563 E-mail: jos@iscas.ac.cn
Copyright 中国科学院软件研究所《软件学报》版权所有 All Rights Reserved
本刊全文数据库版权所有,未经许可,不得转载,本刊保留追究法律责任的权利