發(fā)布時(shí)間：2018-03-09 23:08

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

【摘要】：為了能夠有效的描述現(xiàn)實(shí)世界中的相對(duì)靜止?fàn)顟B(tài),分析了在哲學(xué)邏輯理論中的線序時(shí)態(tài)邏輯定理系統(tǒng)中引入自反性質(zhì)的可行性,在此基礎(chǔ)上建立了具有自反性質(zhì)的線序時(shí)態(tài)邏輯系統(tǒng)TA。敘述了TA時(shí)態(tài)系統(tǒng)的主要定理以及該系統(tǒng)具有無(wú)端稠密線序性質(zhì),并表明了該系統(tǒng)的緊致性、可靠性和完全性。運(yùn)用狀態(tài)重命名方法說(shuō)明了TA系統(tǒng)與行為時(shí)序邏輯TLA系統(tǒng)之間的聯(lián)系,從而將TA的定理系統(tǒng)運(yùn)用到行為時(shí)序邏輯的研究中。
[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ì)算機(jī)軟件與理論研究所;
【分類(lèi)號(hào)】：B819

【共引文獻(xiàn)】

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

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

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

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

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

5 王繼曾,張鍵,王小剛;基于Lotos的面向宏的規(guī)范風(fēng)格[J];計(jì)算機(jī)工程與設(shè)計(jì);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é)報(bào);2004年02期

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

7 唐芳芳;哥德?tīng)柖ɡ淼囊饬x[D];清華大學(xué);2005年

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

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

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

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

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

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

【相似文獻(xiàn)】

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

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

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

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

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

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

6 夏年喜;;從DRT到SDRT——?jiǎng)討B(tài)語(yǔ)義理論的新發(fā)展[J];哲學(xué)動(dòng)態(tài);2006年06期

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

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

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

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

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

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

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

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

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

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

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

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

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

9 單志新;林秋雄;朱杰寧;余細(xì)勇;;miR-1調(diào)控CDK6的表達(dá)在心肌肥厚中的作用[A];中國(guó)病理生理學(xué)會(huì)第九屆全國(guó)代表大會(huì)及學(xué)術(shù)會(huì)議論文摘要[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)重要報(bào)紙文章 前1條

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

本文編號(hào)：1590673