主页期刊介绍编委会编辑部服务介绍道德声明在线审稿编委办公编辑办公English
2020-2021年专刊出版计划 微信服务介绍 最新一期:2020年第5期
     
在线出版
各期目录
纸质出版
分辑系列
论文检索
论文排行
综述文章
专刊文章
美文分享
各期封面
E-mail Alerts
RSS
旧版入口
中国科学院软件研究所
  
投稿指南 问题解答 下载区 收费标准 在线投稿
谭锦豪,李国强.基本并行进程活性的限界模型检测.软件学报,2020,31(8):0
基本并行进程活性的限界模型检测
Bounded Model Checking Liveness on Basic Parallel Processes
投稿时间:2019-08-27  修订日期:2019-12-30
DOI:10.13328/j.cnki.jos.005959
中文关键词:  基本并行进程  限界模型检测  活性  线性整数算术  SMT求解
英文关键词:basic parallel processes  bounded model checking  liveness  linear integer arithmetic  SMT solving
基金项目:国家自然科学基金(61872232,61732013)
作者单位E-mail
谭锦豪 上海交通大学 软件学院, 上海 200240  
李国强 上海交通大学 软件学院, 上海 200240 li.g@sjtu.edu.cn 
摘要点击次数: 266
全文下载次数: 207
中文摘要:
      基本并行进程是一个用于描述和分析并发程序的模型,是Petri网的一个重要子类.EG逻辑是一种在Hennessy-Milner Logic的基础上增加EG算子的分支时间逻辑,其中的AF算子表示从当前的状态出发性质最终会被满足,因此EG逻辑是能够表达活性的逻辑.然而,基于基本并行进程的EG逻辑的模型检测问题是不可判定的.由此,本文提出了基本并行进程上EG逻辑的限界模型检测方法.首先,给出了基本并行进程上EG逻辑的限界语义,然后采用基于约束的方法,将基本并行进程上EG逻辑的限界模型检测问题转化为线性整数算术公式的可满足性问题,最后利用SMT求解器进行求解.
英文摘要:
      Basic parallel processes (BPPs) are a model for describing and analyzing concurrent programs, which is an importance subclass of Petri nets. The logic EG is a branching time logic obtained by extending Hennessy-Milner Logic with the EG operator, in which the AF operator means that a certain property will be satisfied eventually from the current state. Hence, the logic EG is a logic that can express liveness. However, model checking the logic EG over BPPs is undecidable. In this paper, we propose an algorithm for the problem of bounded model checking EG over BPPs. First, a bounded semantics of EG over BPPs is proposed. Then, according to the constraint-based approach, we give a reduction from the problem of bounded model checking EG over BPPs, to the satisfiability problem of linear integer arithmetic formulas. And finally, the linear integer arithmetic formulas are solved by SMT solvers.
HTML  下载PDF全文  查看/发表评论  下载PDF阅读器
 

京公网安备 11040202500064号

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