| 摘要: |
| 线性μ演算（linear time μ-calculus，简称νTL）语法简单，表达能力强，可用于验证并发程序的多种性质.然而，不动点操作符的嵌套使其判定问题难以有效解决.针对这一问题，开发了工具NuTL2PFG，用以判定νTL公式的可满足性.利用νTL公式的当前-未来范式（present future form，简称PF式），该工具能够为一个给定公式构造其当前-未来范式图（present future form graph，简称PFG），用以描述满足该公式的模型.通过在所得PFG中寻找一条ν-路径，即，不涉及最小不动点公式的无穷展开的路径，该工具便可判断出给定公式的可满足性.实验结果表明，NuTL2PFG的执行效率优于已有工具. |
| 关键词: 线性μ演算 当前-未来范式 当前-未来范式图 可满足性 |
| DOI：10.13328/j.cnki.jos.005057 |
| 分类号: |
| 基金项目:国家自然科学基金（61322202，61133001，61420106004，91418201） |
|
| NuTL2PFG: Checking Satisfiability of νTL Formulas |
|
LIU Yao1,2, DUAN Zhen-Hua1,2, TIAN Cong1,2
|
|
1.Institute of Computing Theory and Technology, Xidian University, Xi'an 710071, China;2.State Key Laboratory of Integrated Service Networks(Xidian University), Xi'an 710071, China
|
| 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. |
| Key words: linear time μ-calculus present future form present future form graph satisfiability |
