【摘要】：本文首先定義了具有模糊時態(tài)的廣義可能性線性時序邏輯GPoFLTL(Generalized Possibilistic Fuzzy Linear Tempora Logic)的語構(gòu)以及基于路徑和基于語言的兩種語義解釋,證明了GPoFLTL在模糊時態(tài)方面對GPo LTL(Generalized Possibilistic Linear Tempora Logic)進(jìn)行了擴(kuò)張,并通過實例說明了GPoFLTL比GPo LTL具有更強(qiáng)的表達(dá)能力;其次在廣義可能性測度下通過模糊矩陣運算討論了"不久","幾乎總是"等幾類模糊時態(tài)性質(zhì)的模型檢測問題;最后研究了模糊時態(tài)性質(zhì)的必要性閾值模型檢測問題,給出了基于自動機(jī)的GPoFLTL的閾值模型檢測算法及算法的復(fù)雜度.
[Abstract]:In this paper, we first define the construction of generalized possibilistic linear temporal logic (GPoFLTL (Generalized Possibilistic Fuzzy Linear Tempora Logic) with fuzzy tenses and two semantic interpretations based on path and language. It is proved that GPoFLTL extends GPo LTL (Generalized Possibilistic Linear Tempora Logic) in fuzzy tenses. The examples show that GPoFLTL has stronger expressive ability than GPo LTL, and then some fuzzy temporal properties such as "soon" and "almost always" are discussed by fuzzy matrix operation under generalized possibility measure. Finally, the necessity threshold model detection problem of fuzzy temporal properties is studied, and the algorithm of threshold model detection based on automata for GPoFLTL and the complexity of the algorithm are given.
【作者單位】： 陜西師范大學(xué)數(shù)學(xué)與信息科學(xué)學(xué)院;商丘師范學(xué)院數(shù)學(xué)與統(tǒng)計學(xué)院;
【基金】：國家自然科學(xué)基金(No.11271237,No.11671244,No.11401363,No.11501345) 高等學(xué)校博士學(xué)科點專項科研基金項目(No.20130202110001)
【分類號】：TP301

【相似文獻(xiàn)】

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

2 黃鎮(zhèn)謹(jǐn);基于模型檢測的時空性能分析若干問題研究[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 田聰;命題投影時序邏輯的判定性、復(fù)雜性、表達(dá)性及模型檢測[D];西安電子科技大學(xué);2010年

7 逄濤;命題投影時序邏輯符號模型檢測及其應(yīng)用研究[D];西安電子科技大學(xué);2014年

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

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

10 劉萬偉;擴(kuò)展時序邏輯的推理及符號化模型檢驗技術(shù)[D];國防科學(xué)技術(shù)大學(xué);2009年

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

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

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

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

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

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

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

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

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

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

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

，

本文編號：2290898