扩展命题区间时序逻辑公式可满足性判定算法

留言板

尊敬的读者、作者、审稿人, 关于本刊的投稿、审稿、编辑和出版的任何问题, 您可以本页添加留言。我们将尽快给您答复。谢谢您的支持!

姓名
邮箱
手机号码
标题
留言内容
验证码

扩展命题区间时序逻辑公式可满足性判定算法

朱维军, 邓淼磊, 周清雷, 张海宾

文章导航 > 电子科技大学学报 > 2011 > 40(5): 753-758

朱维军, 邓淼磊, 周清雷, 张海宾. 扩展命题区间时序逻辑公式可满足性判定算法[J]. 电子科技大学学报, 2011, 40(5): 753-758. doi: 10.3969/j.issn.1001-0548.2011.05.023

引用本文:

朱维军, 邓淼磊, 周清雷, 张海宾. 扩展命题区间时序逻辑公式可满足性判定算法[J]. 电子科技大学学报, 2011, 40(5): 753-758. doi: 10.3969/j.issn.1001-0548.2011.05.023

ZHU Wei-jun, DENG Miao-lei, ZHOU Qing-lei, ZHANG Hai-bin. Decision Procedure for Extended Propositional Interval Temporal Logic[J]. Journal of University of Electronic Science and Technology of China, 2011, 40(5): 753-758. doi: 10.3969/j.issn.1001-0548.2011.05.023

Citation:

ZHU Wei-jun, DENG Miao-lei, ZHOU Qing-lei, ZHANG Hai-bin. Decision Procedure for Extended Propositional Interval Temporal Logic[J]. Journal of University of Electronic Science and Technology of China, 2011, 40(5): 753-758. doi: 10.3969/j.issn.1001-0548.2011.05.023

扩展命题区间时序逻辑公式可满足性判定算法

doi: 10.3969/j.issn.1001-0548.2011.05.023

1.
郑州大学信息工程学院郑州 450001;
2.
西安电子科技大学计算机学院西安 710071;
3.
河南工业大学信息科学与工程学院郑州 450001

基金项目:

国家863高技术研究发展计划(2007AA010408);国家自然科学基金(61003079);教育部博士点基金(20100203120012);陕西省工业攻关计划(2009K01-36);中央高校基本科研业务费(JY10000903014)。

作者简介:
朱维军(1976-)，男，博士，主要从事高可信软件与计算机形式化方法方面的研究

中图分类号: TP301

Decision Procedure for Extended Propositional Interval Temporal Logic

1.
School of Information Engineering,Zhengzhou University Zhengzhou 450001;
2.
School of Computer Science,Xidian University Xi'an 71007;
3.
College of Information Science and Technology,Henan University of Technology Zhengzhou 450001

摘要: 针对扩展命题区间时序逻辑由于缺少验证算法因而不能用于模型检测问题，提出该逻辑的可满足性判定算法。首先，正则形子算法把带星算子或不带星算子的扩展命题区间时序逻辑公式翻译为其正则形公式；然后，正则图子算法根据正则形公式构造公式的正则图模型；最后，判定子算法在正则图上判定公式的可满足性。如果在正则图上直接加上接受条件，即可得到公式的自动机模型。新算法的提出为带有星算子的扩展命题区间时序逻辑的模型检测解决了核心方法问题。仿真结果表明，与相关方法相比，基于扩展命题区间时序逻辑的新方法在描述与验证循环结构性质方面具有比较优势。
- 扩展命题区间时序逻辑 /
- 模型检测 /
- 正则图 /
- 可满足性判定
Abstract: Compared with propositional interval temporal logic (PITL), extended propositional interval temporal logic (EPITL) is equipped with infinite models and the chop-star operator additionally. However, there is no algorithm available for model checking EPITL. To this end, we propose an algorithm for EPITL satisfiability checking. The first step is to translate EPITL formulae with or without chop-star operators into their normal forms (NFs). The second step is to construct normal form graphs (NFGs) from the NF formulae. The last step is to check the satisfiability of the EPITL formulae by using the NFGs. Accordingly, we can translate the NFGs into buchi automata. So, the EPITL model checking problem is solved. As shown in the simulation results, our approach is superior to the existing ones based on other logics in terms of specification and verification of some properties of loop structures.
- extended propositional interval temporal logic /
- model checking /
- normal form graph /
- satisifiablity checking

[1]	苏晓萍, 查英华, 曲鸿博. 一种异质图的Lorentz嵌入模型 . 电子科技大学学报, 2023, 52(1): 146-153. doi: 10.12178/1001-0548.2021284
[2]	胡章芳, 曾念文, 罗元, 肖雨婷, 钟征源. 基于原图-光照不变图视觉词典改进的闭环检测方法 . 电子科技大学学报, 2021, 50(4): 586-591. doi: 10.12178/1001-0548.2020272
[3]	黄青松, 戴丹, 冯旭鹏, 付晓东, 刘骊, 刘利军. 面向微博可信度评估的辩论图模型 . 电子科技大学学报, 2017, 46(2): 392-398. doi: 10.3969/j.issn.1001-0548.2017.02.013
[4]	韩凯宁, 张珍兵, 胡剑浩, 陈杰男. 基于因子图的SCMA和LDPC联合检测和译码 . 电子科技大学学报, 2017, 46(5): 685-691, 794. doi: 10.3969/j.issn.1001-0548.2017.05.008
[5]	杨帆, 杨国武, 郝玉洁. 基于模型检测的半量子密码协议的安全性分析 . 电子科技大学学报, 2017, 46(5): 716-721. doi: 10.3969/j.issn.1001-0548.2017.05.013
[6]	王任, 王秉中, 丁霄. 一种新型宽带方向图可重构天线 . 电子科技大学学报, 2016, 45(3): 371-376. doi: O45;TN82
[7]	王任, 王秉中, 丁霄. 一种新型宽带方向图可重构天线 . 电子科技大学学报, 2016, 45(3): 371-376. doi: 10.3969/j.issn.1001-0548.2016.02.010
[8]	闫超, 张建州, 姜正茂. 基于外区抑制与马尔可夫模型的轮廓检测 . 电子科技大学学报, 2016, 45(1): 135-140. doi: 10.3969/j.issn.1001-0548.2016.01.023
[9]	张涛, 谢红, 黄少滨. 多Agent交互策略模型检测方法 . 电子科技大学学报, 2016, 45(5): 802-807. doi: 10.3969/j.issn.1001-0548.2016.05.016
[10]	郭文生, 杨国武, 李晓瑜, 高敏. 基于满足性判定的布尔网络环求解算法 . 电子科技大学学报, 2015, 44(6): 881-886. doi: 10.3969/j.issn.1001-0548.2015.06.015
[11]	俞东进, 吴为, 殷昱煜, 闫大强, 刘志清. 基于模型检测的服务规则路由正确性验证方法 . 电子科技大学学报, 2014, 43(1): 107-112. doi: 10.3969/j.issn.1001-0548.2014.01.018
[12]	朱维军, 乔芃喆, 周清雷, 张海宾. 基于时间区间时序逻辑的实时系统统一模型检测 . 电子科技大学学报, 2014, 43(5): 712-716. doi: 10.3969/j.issn.1001-0548.2014.05.014
[13]	吴丹, 危胜军. 基于模型检测的策略冲突检测方法 . 电子科技大学学报, 2013, 42(5): 745-748,768. doi: 10.3969/j.issn.1001-0548.2013.05.019
[14]	陈世杰, 连可, 王厚军. 采用多信号流图模型的雷达接收机故障诊断方法 . 电子科技大学学报, 2009, 38(1): 87-91.
[15]	王小兵, 段振华. 面向对象的时序逻辑语言 . 电子科技大学学报, 2009, 38(1): 97-101.
[16]	胡威, 李建华, 陈秀真, 蒋兴浩. 可扩展的网络安全态势评价模型优化设计 . 电子科技大学学报, 2009, 38(1): 113-116.
[17]	宋文, 伊良忠, 牟行军. 15-谜问题的可达性判定 . 电子科技大学学报, 2004, 33(5): 604-607.
[18]	丁志强. 基于对象数据流图的可复用方案 . 电子科技大学学报, 1999, 28(3): 306-310.
[19]	章小兵, 王勇, 陈光. 基于自由二元判决图转换的可测性优化方法 . 电子科技大学学报, 1997, 26(2): 171-174.
[20]	张先迪. 高度不正则图的全着色 . 电子科技大学学报, 1997, 26(6): 650-653.

WeChat

点击查看大图

计量

文章访问数: 3317
HTML全文浏览量: 114
PDF下载量: 41
被引次数: 0

扩展命题区间时序逻辑公式可满足性判定算法

doi: 10.3969/j.issn.1001-0548.2011.05.023

1. 郑州大学信息工程学院郑州 450001;

2. 西安电子科技大学计算机学院西安 710071;

3. 河南工业大学信息科学与工程学院郑州 450001

基金项目:

国家863高技术研究发展计划(2007AA010408);国家自然科学基金(61003079);教育部博士点基金(20100203120012);陕西省工业攻关计划(2009K01-36);中央高校基本科研业务费(JY10000903014)。

作者简介:
朱维军(1976-)，男，博士，主要从事高可信软件与计算机形式化方法方面的研究

收稿日期: 2010-01-18
修回日期: 2010-07-06
刊出日期: 2011-10-15

中图分类号: TP301

关键词:

摘要: 针对扩展命题区间时序逻辑由于缺少验证算法因而不能用于模型检测问题，提出该逻辑的可满足性判定算法。首先，正则形子算法把带星算子或不带星算子的扩展命题区间时序逻辑公式翻译为其正则形公式；然后，正则图子算法根据正则形公式构造公式的正则图模型；最后，判定子算法在正则图上判定公式的可满足性。如果在正则图上直接加上接受条件，即可得到公式的自动机模型。新算法的提出为带有星算子的扩展命题区间时序逻辑的模型检测解决了核心方法问题。仿真结果表明，与相关方法相比，基于扩展命题区间时序逻辑的新方法在描述与验证循环结构性质方面具有比较优势。

English Abstract

朱维军, 邓淼磊, 周清雷, 张海宾. 扩展命题区间时序逻辑公式可满足性判定算法[J]. 电子科技大学学报, 2011, 40(5): 753-758. doi: 10.3969/j.issn.1001-0548.2011.05.023

引用本文:

朱维军, 邓淼磊, 周清雷, 张海宾. 扩展命题区间时序逻辑公式可满足性判定算法[J]. 电子科技大学学报, 2011, 40(5): 753-758. doi: 10.3969/j.issn.1001-0548.2011.05.023

ZHU Wei-jun, DENG Miao-lei, ZHOU Qing-lei, ZHANG Hai-bin. Decision Procedure for Extended Propositional Interval Temporal Logic[J]. Journal of University of Electronic Science and Technology of China, 2011, 40(5): 753-758. doi: 10.3969/j.issn.1001-0548.2011.05.023

Citation:

ZHU Wei-jun, DENG Miao-lei, ZHOU Qing-lei, ZHANG Hai-bin. Decision Procedure for Extended Propositional Interval Temporal Logic[J]. Journal of University of Electronic Science and Technology of China, 2011, 40(5): 753-758. doi: 10.3969/j.issn.1001-0548.2011.05.023

全文HTML

/

下载: 全尺寸图片幻灯片

分享

用微信扫码二维码

分享至好友和朋友圈

返回

期刊在线

编辑办公

友情链接

电子科技大学

版权所有 © 《电子科技大学学报》编辑部

地址: 成都市建设北路二段四号电子科技大学主楼中350室电话: 028-83202308,83207559 Email: xuebao@uestc.edu.cn

本系统由北京仁和汇智信息技术有限公司开发