νTL公式的可滿足性檢查
大?。?/span>1.18 MB 人氣： 2017-12-30 需要積分：3
標(biāo)簽：
線性μ演算(linear time μ-calculus,簡稱νTL)語法簡單,表達能力強,可用于驗證并發(fā)程序的多種性質(zhì).然而,不動點操作符的嵌套使其判定問題難以有效解決.針對這一問題,開發(fā)了工具 NuTL2PFG,用以判定νTL 公式的可滿足性.利用νTL 公式的當(dāng)前-未來范式(present future form,簡稱 PF 式),該工具能夠為一個給定公式構(gòu)造其當(dāng)前-未來范式圖(present future form graph,簡稱 PFG),用以描述滿足該公式的模型.通過在所得 PFG 中尋找一條ν-路徑,即,不涉及最小不動點公式的無窮展開的路徑,該工具便可判斷出給定公式的可滿足性.實驗結(jié)果表明,NuTL2PFG 的執(zhí)行效率優(yōu)于已有工具。
?
?
非常好我支持^.^
(0) 0%
不好我反對
(0) 0%