本文關(guān)鍵詞： 線性μ演算 當(dāng)前-未來范式 當(dāng)前-未來范式圖 可滿足性　出處：《軟件學(xué)報》2017年04期 　論文類型：期刊論文

【摘要】：線性μ演算(linear timeμ-calculus,簡稱νTL)語法簡單,表達(dá)能力強,可用于驗證并發(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)于已有工具.
[Abstract]:Linear time 渭 -calculus is simple and expressive, and can be used to verify the properties of concurrent programs. Because of the nesting of fixed point operators, it is difficult to solve the problem of judging the fixed point operators effectively. In order to solve this problem, a tool NuTL2PFG is developed. In order to determine the satisfiability of future TL formula, the present-future normal form (PF) is used to determine the satisfiability of the formula. The tool can construct its present-future normal form graph (PFG) for a given formula. In this paper, we use the model to describe the formula. By looking for a PFG path, we can find an infinitely expanded path that does not involve the minimum fixed point formula. The experimental results show that the performance efficiency of NuTL2PFG is better than that of existing tools.
【作者單位】： 西安電子科技大學(xué)計算理論與技術(shù)研究所;綜合業(yè)務(wù)網(wǎng)理論及關(guān)鍵技術(shù)國家重點實驗室(西安電子科技大學(xué));
【基金】：國家自然科學(xué)基金(61322202,61133001,61420106004,91418201)~~
【分類號】：TP311.1
【正文快照】： 線性μ演算(linear timeμ-calculus,簡稱νTL)[1]是模態(tài)μ演算[2]的時序版本,它與線性時序邏輯(linear temporallogic,簡稱LTL)[3]最大的不同在于最小和最大不動點操作符的引入.νTL不僅語法簡潔,而且具有完全正則的表達(dá)能力[4,5],可用于表達(dá)和驗證并發(fā)程序的多種正則性質(zhì),這

【相似文獻(xiàn)】

相關(guān)期刊論文 前10條

1 王守信;張莉;王帥;申菊芳;劉禹;;一種目標(biāo)可滿足性定性、定量表示與推理方法[J];軟件學(xué)報;2011年04期

2 張忠林;唐璞山;;一個基于可滿足性算法的時序深度計算方法[J];計算機工程;2006年02期

3 李光輝,李曉維;基于增量可滿足性的等價性檢驗方法[J];計算機學(xué)報;2004年10期

4 施伯樂,李科;連接依賴子類可滿足性的多項式測試[J];計算機學(xué)報;1985年05期

5 孫雪姣;劉驚雷;;基于表決策略的CP-Nets可滿足性序列的聚合[J];模式識別與人工智能;2013年09期

6 鄧澍軍;吳為民;邊計年;;RTL驗證中的混合可滿足性求解[J];計算機輔助設(shè)計與圖形學(xué)學(xué)報;2007年03期

7 孫雪姣;劉驚雷;;CP-nets的可滿足性及一致性研究[J];計算機研究與發(fā)展;2012年04期

8 鄧雨春,楊士元,邢建輝;基于布爾可滿足性的組合電路ATPG算法[J];計算機工程與應(yīng)用;2003年07期

9 鄭飛君,嚴(yán)曉浪,葛海通,楊軍,盧永江;使用輸出分組和電路可滿足性的等價性驗證算法[J];計算機輔助設(shè)計與圖形學(xué)學(xué)報;2005年11期

10 吳洋;唐璞山;;基于布爾可滿足性的電路設(shè)計錯誤診斷算法[J];計算機輔助設(shè)計與圖形學(xué)學(xué)報;2006年09期

相關(guān)會議論文 前3條

1 鄧澍軍;吳為民;邊計年;;RTL驗證中的混合可滿足性求解[A];第四屆中國測試學(xué)術(shù)會議論文集[C];2006年

2 馬海濤;郝忠孝;;一種檢驗Active XML文檔樹模式查詢可滿足性算法[A];第二十五屆中國數(shù)據(jù)庫學(xué)術(shù)會議論文集（二）[C];2008年

3 吳為民;;基于二元CSP的RTL數(shù)據(jù)通路可滿足性求解方法[A];第五屆中國測試學(xué)術(shù)會議論文集[C];2008年

相關(guān)博士學(xué)位論文 前2條

1 范全潤;基于分治的布爾可滿足性判定[D];西安電子科技大學(xué);2015年

2 唐玉蘭;偽布爾可滿足性算法及其在FPGA布線中的研究應(yīng)用[D];江南大學(xué);2010年

相關(guān)碩士學(xué)位論文 前5條

1 王鶴;面向GPU的可滿足性求解技術(shù)研究[D];國防科學(xué)技術(shù)大學(xué);2010年

2 李學(xué)彬;開源軟件依賴可滿足性識別方法研究與實現(xiàn)[D];東北大學(xué);2008年

3 趙偉楠;對可滿足性（SAT）問題求全解的算法研究及實現(xiàn)[D];北京交通大學(xué);2009年

4 王先建;基于偽布爾可滿足性的CMOL單元配置研究[D];寧波大學(xué);2013年

5 郭琦;一個證明QBF不可滿足性的新算法的設(shè)計與實現(xiàn)[D];東北師范大學(xué);2015年

，

本文編號：1463757