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

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