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

NuTL2PFG: Checking Satisfiability of νTL Formulas

线性μ演算(linear timeμ-calculus,简称νTL)语法简单,表达能力强,可用于验证并发程序的多种性质.然而,不动点操作符的嵌套使其判定问题难以有效解决.针对这一问题,开发了工具NuTL2PFG,用以判定νTL公式的可满足性.利用νTL公式的当前-未来范式(present future form,简称PF式),该工具能够为一个给定公式构造其当前-未来范式图(present future form graph,简称PFG),用以描述满足该公式的模型.通过在所得PFG中寻找一条ν-路径,即,不涉及最小不动点公式的无穷展开的路径,该工具便可判断出给定公式的可满足性.实验结果表明,NuTL2PFG的执行效率优于已有工具.

Linear time u-calculus （vTL） 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 vTL formulas is developed in this paper.Based on present future form （PF form） of vTL 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 v-path in its PFG free of infinite unfoldings of least fixpoints.Experimental results show that NuTL2PFG is more efficient than the existing tools.