本文選題：可能性理論 + 計(jì)算樹邏輯�。� 參考：《電子學(xué)報(bào)》2017年11期

【摘要】：本文首先分別給出了"約束可達(dá)","總是可達(dá)"這兩個公式在廣義可能性計(jì)算樹邏輯(GPo CTL)中的另外兩種等價(jià)形式;其次討論了基于廣義可能性測度的計(jì)算樹邏輯的模型檢測問題,將GPo CTL的模型檢測問題規(guī)約為經(jīng)典的CTL模型檢測問題,利用截集的方法,給出了計(jì)算GPo CTL的模型檢測問題的算法及其復(fù)雜度,并通過實(shí)例分析說明了這種算法的可行性;最后,研究了具有公平性假設(shè)的GPo CTL模型檢測問題的計(jì)算復(fù)雜度,得到了與上面相似的結(jié)論.
[Abstract]:In this paper, we first give two other equivalent forms of "constraint reachability" and "always reachability" in generalized possibility computing tree logic (GPOCTL), and then discuss the model checking problem of computing tree logic based on generalized possibility measure. The model detection problem of GPO CTL is defined as a classical CTL model detection problem. The algorithm and complexity of the model detection problem for calculating the GPO CTL are given by using the method of truncation. The feasibility of the algorithm is illustrated by an example. In this paper, the computational complexity of the GPO CTL model detection problem with fairness hypothesis is studied, and a similar conclusion is obtained.
【作者單位】： 陜西師范大學(xué)數(shù)學(xué)與信息科學(xué)學(xué)院;商丘師范學(xué)院數(shù)學(xué)與統(tǒng)計(jì)學(xué)院;
【基金】：國家自然科學(xué)基金(No.11271237,No.11671244,No.11401363,No.11501345) 高等學(xué)校博士學(xué)科點(diǎn)專項(xiàng)科研基金(No.20130202110001)
【分類號】：TP301.6

【相似文獻(xiàn)】

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

1 林惠民,張文輝;模型檢測:理論、方法與應(yīng)用[J];電子學(xué)報(bào);2002年S1期

2 戎玫;張廣泉;;模型檢測新技術(shù)研究[J];計(jì)算機(jī)科學(xué);2003年05期

3 肖健宇;張德運(yùn);鄭衛(wèi)斌;;過程提取用于改善程序模型檢測的可伸縮性[J];西安交通大學(xué)學(xué)報(bào);2006年06期

4 袁志斌;徐正權(quán);王能超;;軟件模型檢測中的抽象[J];計(jì)算機(jī)科學(xué);2006年07期

5 劉吉鋒;孫吉貴;;基于抽象-驗(yàn)證-細(xì)化范例的軟件模型檢測[J];計(jì)算機(jī)科學(xué);2006年12期

6 化志章;吳傳孫;揭安全;薛錦云;;軟件模型檢測新技術(shù)研究[J];微計(jì)算機(jī)信息;2007年36期

7 王飛明;胡元闖;董榮勝;;模型檢測研究進(jìn)展[J];廣西科學(xué)院學(xué)報(bào);2008年04期

8 鄺宏斌;羅貴明;;并行軟件模型檢測[J];計(jì)算機(jī)工程;2008年19期

9 何愷鐸;顧明;宋曉宇;李力;李江;;面向源代碼的軟件模型檢測及其實(shí)現(xiàn)[J];計(jì)算機(jī)科學(xué);2009年01期

10 顧濱兵;;一種軟件模型檢測方法及其原型系統(tǒng)[J];微計(jì)算機(jī)應(yīng)用;2010年11期

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

1 高靜;曹子寧;;基于空間邏輯和計(jì)算樹邏輯的模型檢測[A];2009年中國高校通信類院系學(xué)術(shù)研討會論文集[C];2009年

2 許梅;曹子寧;;基于謂詞μ演算和空間邏輯的模型檢測算法研究[A];2009年中國高校通信類院系學(xué)術(shù)研討會論文集[C];2009年

3 何青;駱翔宇;蘇開樂;;對弈必勝策略的符號化模型檢測[A];2006年全國理論計(jì)算機(jī)科學(xué)學(xué)術(shù)年會論文集[C];2006年

4 王飛明;胡元闖;董榮勝;;模型檢測中狀態(tài)爆炸及其優(yōu)化策略研究[A];廣西計(jì)算機(jī)學(xué)會2008年年會論文集[C];2008年

5 陳道喜;張廣泉;陳冬火;;NSPK協(xié)議的Spin模型檢測[A];2008年全國開放式分布與并行計(jì)算機(jī)學(xué)術(shù)會議論文集(下冊)[C];2008年

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

1 奚琪;基于模型檢測的二進(jìn)制代碼惡意行為識別技術(shù)研究[D];解放軍信息工程大學(xué);2014年

2 黃鎮(zhèn)謹(jǐn);基于模型檢測的時(shí)空性能分析若干問題研究[D];合肥工業(yè)大學(xué);2016年

3 江華;界程演算模型檢測[D];貴州大學(xué);2008年

4 劉劍;傳值進(jìn)程與移動進(jìn)程的模型檢測方法[D];中國科學(xué)院研究生院（軟件研究所）;2005年

5 趙璐;On-the-Fly和動態(tài)的軟件模型檢測方法研究[D];哈爾濱工程大學(xué);2014年

6 田聰;命題投影時(shí)序邏輯的判定性、復(fù)雜性、表達(dá)性及模型檢測[D];西安電子科技大學(xué);2010年

7 黃宏濤;基于懶惰切片的模型檢測技術(shù)研究[D];哈爾濱工程大學(xué);2012年

8 劉金卓;基于符號化模型檢測的軟件演化過程模型驗(yàn)證[D];云南大學(xué);2013年

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

1 張興興;基于廣義可能性測度的互模擬及CTL不動點(diǎn)語義[D];陜西師范大學(xué);2015年

2 王彬;基于多值模型檢測的SaaS應(yīng)用測試及其自動化研究[D];陜西師范大學(xué);2015年

3 王凱;基于模型檢測多反例對軟件進(jìn)行調(diào)試[D];電子科技大學(xué);2015年

4 張恒;多值模型檢測器的研究與實(shí)現(xiàn)[D];陜西師范大學(xué);2015年

5 王舒鵬;基于外存的大規(guī)模模型檢測新方法的研究[D];電子科技大學(xué);2015年

6 劉曉芳;PPTL符號模型檢測方法及工具研究[D];西安電子科技大學(xué);2014年

7 王云云;基于分組壓縮算法的并行程序模型檢測[D];中國科學(xué)技術(shù)大學(xué);2016年

8 段廷銀;基于云計(jì)算平臺的時(shí)態(tài)邏輯模型檢測算法研究與實(shí)現(xiàn)[D];鄭州大學(xué);2016年

9 張巖;基于模型檢測的Twig模式最小化技術(shù)[D];北京工業(yè)大學(xué);2016年

10 張松年;基于模型檢測的漏洞挖掘方法研究[D];西安電子科技大學(xué);2015年

，

本文編號：2018607