本文選題：模型檢測　切入點(diǎn)：時態(tài)邏輯　出處：《計算機(jī)工程與設(shè)計》2011年04期 　論文類型：期刊論文

【摘要】：為了能夠有效的描述現(xiàn)實(shí)世界中的相對靜止?fàn)顟B(tài),分析了在哲學(xué)邏輯理論中的線序時態(tài)邏輯定理系統(tǒng)中引入自反性質(zhì)的可行性,在此基礎(chǔ)上建立了具有自反性質(zhì)的線序時態(tài)邏輯系統(tǒng)TA。敘述了TA時態(tài)系統(tǒng)的主要定理以及該系統(tǒng)具有無端稠密線序性質(zhì),并表明了該系統(tǒng)的緊致性、可靠性和完全性。運(yùn)用狀態(tài)重命名方法說明了TA系統(tǒng)與行為時序邏輯TLA系統(tǒng)之間的聯(lián)系,從而將TA的定理系統(tǒng)運(yùn)用到行為時序邏輯的研究中。
[Abstract]:In order to effectively describe the relative static state in the real world, the feasibility of introducing reflexive properties into the linear order temporal logic theorem system of philosophical logic theory is analyzed. On this basis, a linear ordered temporal logic system with reflexive properties is established. The main theorems of the TA temporal system and its dense linear ordering property are described, and the compactness of the system is shown. Reliability and completeness. The relationship between TA system and behavioral temporal logic (TLA) system is explained by the state renaming method, and the TA theorem system is applied to the study of behavioral temporal logic.
【作者單位】： 貴州大學(xué)計算機(jī)軟件與理論研究所;
【分類號】：B819

【共引文獻(xiàn)】

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

1 張玉軍,李忠誠;移動IPv6測試中的層次化協(xié)議描述和測試生成方法[J];電子學(xué)報;2004年S1期

2 高翔,戎舟,馬秀飛,周亮;網(wǎng)絡(luò)儀器與通信協(xié)議一致性測試技術(shù)[J];工業(yè)儀表與自動化裝置;2005年01期

3 潘紅艷,于全;用于通信網(wǎng)絡(luò)協(xié)議開發(fā)的形式化方法[J];計算機(jī)工程;2004年02期

4 張玉軍,田野,鄭紅霞,孫靜波;基于TTCN的IPv6協(xié)議測試[J];計算機(jī)輔助設(shè)計與圖形學(xué)學(xué)報;2005年07期

5 王繼曾,張鍵,王小剛;基于Lotos的面向宏的規(guī)范風(fēng)格[J];計算機(jī)工程與設(shè)計;2005年01期

6 劉丹,于海斌,王宏,呂勇;FF HSE和FF H1協(xié)議網(wǎng)關(guān)的基本原理與實(shí)現(xiàn)[J];信息與控制;2004年06期

7 楊武金;弗協(xié)調(diào)邏輯及其理論特征[J];中共南京市委黨校南京市行政學(xué)院學(xué)報;2004年02期

8 馮艷;論經(jīng)典否定、直覺主義否定和弗協(xié)調(diào)否定[J];自然辯證法研究;2005年02期

9 陳波;從人工智能看當(dāng)代邏輯學(xué)的發(fā)展[J];中山大學(xué)學(xué)報論叢;2000年02期

10 王路;關(guān)于邏輯哲學(xué)的幾點(diǎn)思考[J];中國社會科學(xué);2003年03期

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

1 宋巖;徐皚冬;;ISO11783協(xié)議棧測試[A];2007'儀表，，自動化及先進(jìn)集成技術(shù)大會論文集（二）[C];2007年

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

1 余俊偉;弗協(xié)調(diào)邏輯應(yīng)用于道義邏輯的研究[D];中國社會科學(xué)院研究生院;2001年

2 楊華千;基于混沌與代數(shù)群的分組密碼算法研究[D];重慶大學(xué);2007年

3 張立娜;個體詞的邏輯語義[D];清華大學(xué);2007年

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

1 賈國恒;盧卡西維茨多值邏輯及其與一些邏輯的比較[D];河南大學(xué);2003年

2 焦志偉;決策過程中的邏輯應(yīng)用[D];河南大學(xué);2003年

3 盧虎;基于DSP的以太網(wǎng)技術(shù)及其實(shí)現(xiàn)[D];西北工業(yè)大學(xué);2004年

4 陳漢蓉;基于IP選項的主動包研究[D];西南師范大學(xué);2004年

5 琚喬月;法律專家系統(tǒng)的邏輯學(xué)探析[D];河南大學(xué);2005年

6 賈改琴;知道謂詞邏輯[D];西南師范大學(xué);2005年

7 唐芳芳;哥德爾定理的意義[D];清華大學(xué);2005年

8 徐娟;MPLS及其測試技術(shù)研究[D];西南交通大學(xué);2006年

9 付春雷;基于多階段網(wǎng)絡(luò)攻擊模型的緩沖區(qū)溢出攻擊技術(shù)研究與實(shí)踐[D];重慶大學(xué);2006年

10 黃曉東;長慶企業(yè)網(wǎng)網(wǎng)絡(luò)管理系統(tǒng)研究與設(shè)計[D];西安科技大學(xué);2007年

【二級參考文獻(xiàn)】

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

1 文靜華;余濱;張梅;李祥;;基于SMV的網(wǎng)絡(luò)協(xié)議形式化分析與驗(yàn)證[J];計算機(jī)工程;2006年15期

【相似文獻(xiàn)】

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

1 呂進(jìn);;一個向上線序的命題時態(tài)邏輯PTL[J];西南大學(xué)學(xué)報(社會科學(xué)版);2010年02期

2 王輝;;混合語言與時態(tài)邏輯[J];湖南科技大學(xué)學(xué)報(社會科學(xué)版);2009年02期

3 馮彥波;;決定論、邏輯決定論與時態(tài)邏輯[J];內(nèi)蒙古農(nóng)業(yè)大學(xué)學(xué)報(社會科學(xué)版);2008年01期

4 劉本學(xué);;時態(tài)命題的對當(dāng)關(guān)系及推理[J];赤峰學(xué)院學(xué)報(漢文哲學(xué)社會科學(xué)版);2008年03期

5 裘江杰;;一族不完全的邏輯[J];哲學(xué)研究;2007年04期

6 夏年喜;;從DRT到SDRT——動態(tài)語義理論的新發(fā)展[J];哲學(xué)動態(tài);2006年06期

7 周禎祥;;現(xiàn)代模態(tài)邏輯的多元視野[J];華南師范大學(xué)學(xué)報(社會科學(xué)版);2006年05期

8 張家龍;論亞里士多德的排中律疑難[J];哲學(xué)動態(tài);2004年12期

9 康巧茹;探析道義邏輯的哲學(xué)淵源[J];寧夏黨校學(xué)報;2002年02期

10 馮棉;廣義模態(tài)邏輯研究中的若干問題[J];華東師范大學(xué)學(xué)報(哲學(xué)社會科學(xué)版);2001年05期

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

1 陳永勤;王培龍;;香港城市日用水量的統(tǒng)計模型:趨勢、模式及預(yù)測[A];農(nóng)業(yè)、生態(tài)水安全及寒區(qū)水科學(xué)——第八屆中國水論壇摘要集[C];2010年

2 曾紅衛(wèi);繆淮扣;;優(yōu)化基于模型檢驗(yàn)的測試生成[A];第六屆中國測試學(xué)術(shù)會議論文集[C];2010年

3 常亮;高申;李德波;古天龍;;基于OBDD的描述邏輯ALCIO判定算法[A];廣西計算機(jī)學(xué)會2010年學(xué)術(shù)年會論文集[C];2010年

4 ;基于時間自動機(jī)的實(shí)時系統(tǒng)建模及驗(yàn)證[A];第六屆和諧人機(jī)環(huán)境聯(lián)合學(xué)術(shù)會議（HHME2010)、第19屆全國多媒體學(xué)術(shù)會議（NCMT2010）、第6屆全國人機(jī)交互學(xué)術(shù)會議（CHCI2010）、第5屆全國普適計算學(xué)術(shù)會議（PCC2010）論文集[C];2010年

5 余興超;馬爭先;王玉斌;董榮勝;;基于UPPAAL的簡單網(wǎng)絡(luò)支付協(xié)議形式化驗(yàn)證[A];廣西計算機(jī)學(xué)會2010年學(xué)術(shù)年會論文集[C];2010年

6 譚初兵;張大同;裴媛;呂超君;徐為人;湯立達(dá);;內(nèi)皮素受體拮抗劑的篩選[A];新藥研發(fā)暨新藥發(fā)現(xiàn)學(xué)術(shù)研討會會議論文集[C];2010年

7 李蓬;崔寶江;;基于C/C++代碼的靜態(tài)分析工具的比較研究[A];2010國際計算機(jī)科學(xué)技術(shù)與應(yīng)用論壇論文集[C];2010年

8 郝莉莉;楊惠珍;謝攀;;CPN在聯(lián)邦概念模型形式化建模與驗(yàn)證中的應(yīng)用[A];雷達(dá)與電子對抗一體化及仿真技術(shù)學(xué)術(shù)交流會論文集[C];2010年

9 單志新;林秋雄;朱杰寧;余細(xì)勇;;miR-1調(diào)控CDK6的表達(dá)在心肌肥厚中的作用[A];中國病理生理學(xué)會第九屆全國代表大會及學(xué)術(shù)會議論文摘要[C];2010年

10 苗留洋;趙東明;周清雷;;基于L~*學(xué)習(xí)算法的假設(shè)—保證推理[A];Proceedings of 2010 The 3rd International Conference on Computational Intelligence and Industrial Application(Volume 6)[C];2010年

相關(guān)重要報紙文章 前1條

1 本報記者 邊歆;異常檢測是阻止蠕蟲攻擊的最好方法？[N];網(wǎng)絡(luò)世界;2006年

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

1 徐鳴;程序驗(yàn)證與系統(tǒng)分析中的若干符號計算問題[D];華東師范大學(xué);2010年

2 趙也非;動態(tài)UML子圖的形式語義研究[D];華東師范大學(xué);2010年

3 林榮德;移動界程演算及模型檢測應(yīng)用的關(guān)鍵問題研究[D];華南理工大學(xué);2010年

4 宋波;Web應(yīng)用交互的建模和測試用例生成[D];上海大學(xué);2010年

5 張俊;特征模型驅(qū)動的軟件開發(fā)方法及相關(guān)技術(shù)研究[D];吉林大學(xué);2010年

6 高妍妍;ASIP體系結(jié)構(gòu)形式化建模與驗(yàn)證方法研究[D];中國科學(xué)技術(shù)大學(xué);2009年

7 程亮;基于模型檢測的安全操作系統(tǒng)驗(yàn)證方法研究[D];中國科學(xué)技術(shù)大學(xué);2009年

8 王健;任務(wù)關(guān)鍵系統(tǒng)生存性形式化建模與分析[D];哈爾濱工程大學(xué);2009年

9 門鵬;基于Petri網(wǎng)的Web服務(wù)組合相關(guān)技術(shù)研究[D];西安電子科技大學(xué);2009年

10 王小兵;目面向?qū)ο驧SVL語言及其在組合Web服務(wù)驗(yàn)證中的應(yīng)用[D];西安電子科技大學(xué);2009年

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

1 徐立;基于攻擊圖模型的網(wǎng)絡(luò)安全分析方法研究[D];上海交通大學(xué);2011年

2 高丹丹;無線認(rèn)證協(xié)議的模型檢測與分析研究[D];長春理工大學(xué);2010年

3 李曉聰;基于模型檢測的空間訪問控制系統(tǒng)規(guī)則驗(yàn)證[D];江蘇大學(xué);2010年

4 張穎;基于博弈的多參與者合同簽署協(xié)議的驗(yàn)證[D];山東大學(xué);2010年

5 姜志敏;模型檢測在配置中的應(yīng)用[D];吉林大學(xué);2010年

6 安鑫;面向一類基于輪數(shù)的分布式算法的狀態(tài)空間分析與模型檢測[D];山東大學(xué);2010年

7 褚偉萍;知識工程在轎車系統(tǒng)開發(fā)項目管理中的應(yīng)用[D];上海交通大學(xué);2010年

8 張小研;SOA流程的建模與驗(yàn)證[D];北京交通大學(xué);2010年

9 李明;基于模型驗(yàn)證的故障定位方法研究[D];華中師范大學(xué);2010年

10 謝茜;基于生物調(diào)和序列的軟件故障定位方法研究[D];華中師范大學(xué);2010年

本文編號：1590673