NuTL2PFG:vTL公式的可满足性检查

• 作者: 刘尧 段振华 田聪
• 来源期刊: 软件学报
• 学科: 工学
• 关键词: 线性μ演算 当前-未来范式 当前-未来范式图 可满足性
• 年，卷（期）: 2017,（4）
• 所属期刊栏目: 系统软件与软件工程
• 页码范围: 898-906
• 页数: 9页
• 分类号: TP301
• 字数: 6502字
• 语种: 中文
• DOI: 10.13328/j.cnki.jos.005057

摘要

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