Journal of Software:2017.28(4):898-906

(西安电子科技大学 计算理论与技术研究所, 陕西 西安 710071;综合业务网理论及关键技术国家重点实验室(西安电子科技大学), 陕西 西安 710071)
NuTL2PFG: Checking Satisfiability of νTL Formulas
LIU Yao,DUAN Zhen-Hua,TIAN Cong
(Institute of Computing Theory and Technology, Xidian University, Xi'an 710071, China;State Key Laboratory of Integrated Service Networks(Xidian University), Xi'an 710071, China)
Chart / table
Similar Articles
Article :Browse 1945   Download 1133
Received:December 25, 2015    Revised:February 24, 2016
> 中文摘要: 线性μ演算(linear time μ-calculus,简称νTL)语法简单,表达能力强,可用于验证并发程序的多种性质.然而,不动点操作符的嵌套使其判定问题难以有效解决.针对这一问题,开发了工具NuTL2PFG,用以判定νTL公式的可满足性.利用νTL公式的当前-未来范式(present future form,简称PF式),该工具能够为一个给定公式构造其当前-未来范式图(present future form graph,简称PFG),用以描述满足该公式的模型.通过在所得PFG中寻找一条ν-路径,即,不涉及最小不动点公式的无穷展开的路径,该工具便可判断出给定公式的可满足性.实验结果表明,NuTL2PFG的执行效率优于已有工具.
Abstract:Linear time μ-calculus (νTL) is a formalism which has a strong expressive power with a succinct syntax. It is useful for specifying and verifying various properties of concurrent programs. However, the nesting of fix point operators makes its decision problem difficult to solve. To tackle the issue, a tool called NuTL2PFG for checking the satisfiability of νTL formulas is developed in this paper. Based on present future form (PF form) of νTL formulas, the tool is able to construct the present future form graph (PFG) for a given formula to specify the models that satisfy the formula. Further, the tool checks the satisfiability of a given formula by searching for a ν-path in its PFG free of infinite unfoldings of least fixpoints. Experimental results show that NuTL2PFG is more efficient than the existing tools.
文章编号:     中图分类号:    文献标志码:
基金项目:国家自然科学基金(61322202,61133001,61420106004,91418201) 国家自然科学基金(61322202,61133001,61420106004,91418201)
Foundation items:National Natural Science Foundation of China (61322202, 61133001, 61420106004, 91418201)
Reference text:


LIU Yao,DUAN Zhen-Hua,TIAN Cong.NuTL2PFG: Checking Satisfiability of νTL Formulas.Journal of Software,2017,28(4):898-906