NuTL2PFG:νTL公式的可满足性检查

发布时间：2018-01-25 21:39

  本文关键词： 线性μ演算 当前-未来范式 当前-未来范式图 可满足性　出处：《软件学报》2017年04期 　论文类型：期刊论文

【摘要】：线性μ演算(linear timeμ-calculus,简称νTL)语法简单,表达能力强,可用于验证并发程序的多种性质.然而,不动点操作符的嵌套使其判定问题难以有效解决.针对这一问题,开发了工具NuTL2PFG,用以判定νTL公式的可满足性.利用νTL公式的当前-未来范式(present future form,简称PF式),该工具能够为一个给定公式构造其当前-未来范式图(present future form graph,简称PFG),用以描述满足该公式的模型.通过在所得PFG中寻找一条ν-路径,即,不涉及最小不动点公式的无穷展开的路径,该工具便可判断出给定公式的可满足性.实验结果表明,NuTL2PFG的执行效率优于已有工具.
[Abstract]:Linear time 渭 -calculus is simple and expressive, and can be used to verify the properties of concurrent programs. Because of the nesting of fixed point operators, it is difficult to solve the problem of judging the fixed point operators effectively. In order to solve this problem, a tool NuTL2PFG is developed. In order to determine the satisfiability of future TL formula, the present-future normal form (PF) is used to determine the satisfiability of the formula. The tool can construct its present-future normal form graph (PFG) for a given formula. In this paper, we use the model to describe the formula. By looking for a PFG path, we can find an infinitely expanded path that does not involve the minimum fixed point formula. The experimental results show that the performance efficiency of NuTL2PFG is better than that of existing tools.
【作者单位】： 西安电子科技大学计算理论与技术研究所;综合业务网理论及关键技术国家重点实验室(西安电子科技大学);
【基金】：国家自然科学基金(61322202,61133001,61420106004,91418201)~~
【分类号】：TP311.1
【正文快照】： 线性μ演算(linear timeμ-calculus,简称νTL)[1]是模态μ演算[2]的时序版本,它与线性时序逻辑(linear temporallogic,简称LTL)[3]最大的不同在于最小和最大不动点操作符的引入.νTL不仅语法简洁,而且具有完全正则的表达能力[4,5],可用于表达和验证并发程序的多种正则性质,这

【相似文献】

相关期刊论文 前10条

1 王守信;张莉;王帅;申菊芳;刘禹;;一种目标可满足性定性、定量表示与推理方法[J];软件学报;2011年04期

2 张忠林;唐璞山;;一个基于可满足性算法的时序深度计算方法[J];计算机工程;2006年02期

3 李光辉,李晓维;基于增量可满足性的等价性检验方法[J];计算机学报;2004年10期

4 施伯乐,李科;连接依赖子类可满足性的多项式测试[J];计算机学报;1985年05期

5 孙雪姣;刘惊雷;;基于表决策略的CP-Nets可满足性序列的聚合[J];模式识别与人工智能;2013年09期

6 邓澍军;吴为民;边计年;;RTL验证中的混合可满足性求解[J];计算机辅助设计与图形学学报;2007年03期

7 孙雪姣;刘惊雷;;CP-nets的可满足性及一致性研究[J];计算机研究与发展;2012年04期

8 邓雨春,杨士元,邢建辉;基于布尔可满足性的组合电路ATPG算法[J];计算机工程与应用;2003年07期

9 郑飞君,严晓浪,葛海通,杨军,卢永江;使用输出分组和电路可满足性的等价性验证算法[J];计算机辅助设计与图形学学报;2005年11期

10 吴洋;唐璞山;;基于布尔可满足性的电路设计错误诊断算法[J];计算机辅助设计与图形学学报;2006年09期

相关会议论文 前3条

1 邓澍军;吴为民;边计年;;RTL验证中的混合可满足性求解[A];第四届中国测试学术会议论文集[C];2006年

2 马海涛;郝忠孝;;一种检验Active XML文档树模式查询可满足性算法[A];第二十五届中国数据库学术会议论文集（二）[C];2008年

3 吴为民;;基于二元CSP的RTL数据通路可满足性求解方法[A];第五届中国测试学术会议论文集[C];2008年

相关博士学位论文 前2条

1 范全润;基于分治的布尔可满足性判定[D];西安电子科技大学;2015年

2 唐玉兰;伪布尔可满足性算法及其在FPGA布线中的研究应用[D];江南大学;2010年

相关硕士学位论文 前5条

1 王鹤;面向GPU的可满足性求解技术研究[D];国防科学技术大学;2010年

2 李学彬;开源软件依赖可满足性识别方法研究与实现[D];东北大学;2008年

3 赵伟楠;对可满足性（SAT）问题求全解的算法研究及实现[D];北京交通大学;2009年

4 王先建;基于伪布尔可满足性的CMOL单元配置研究[D];宁波大学;2013年

5 郭琦;一个证明QBF不可满足性的新算法的设计与实现[D];东北师范大学;2015年

，

本文编号：1463757