【摘要】：傳統(tǒng)的觀點認為保持系統(tǒng)刻畫的協(xié)調性1是并發(fā)系統(tǒng)開發(fā)過程基本的要求,但隨著所設計并發(fā)系統(tǒng)的規(guī)模越來越大,功能越來越復雜,使得自始至終維持系統(tǒng)的協(xié)調性成為一個具有挑戰(zhàn)性的課題。分布式的開發(fā)方式,系統(tǒng)信息所固有的不確定性,進一步惡化了維持系統(tǒng)刻畫協(xié)調性的難度和代價。因此我們需要一種超越經典邏輯觀念的方法學,以一種合理的方式處理含有非協(xié)調信息的系統(tǒng)刻畫 經典邏輯具有許多直覺的屬性和較強的表達、推理能力,適于刻畫并發(fā)系統(tǒng)。但由于平凡推理的緣故,含有非協(xié)調性的形式刻畫無意義。基于超協(xié)調邏輯的方法學,通過把時序的觀念與超協(xié)調性的方法學相結合,本文提出了一種時序邏輯QCTL(Quasi-classical temporal logic),一方面,QCTL具有刻畫并發(fā)系統(tǒng)時序屬性的能力,另一方面,避免了非協(xié)調情形下的平凡推理問題。本文主要研究QCTL邏輯體系,包括它的語義學、證明系統(tǒng)及基于QCTL的模型檢測問題。 為了取得形式推理上的超協(xié)調性,QCTL的證明系統(tǒng)與經典邏輯有著顯著的差別。這個證明系統(tǒng)是由兩種不同的推理規(guī)則構成,分為分解規(guī)則和合成規(guī)則。一個具體的證明過程由分解過程和合成過程兩部分組成,并且分解過程應用分解規(guī)則,合成過程應用合成規(guī)則,這樣就避免了一些能導致平凡推理的證明理論。同時,我們給出了該證明系統(tǒng)的可靠性和完備性證明。QCTL的語義由paraKripke結構表達,它是標準Kripke結構的一種擴展。通過這種擴展,在語義層次上解開公式α和?α之間的聯系,取得了語義上的超協(xié)調性,可以用于刻畫、推理含有非協(xié)調信息的并發(fā)系統(tǒng)。 經典時序邏輯的模型檢測問題得到了廣泛而且深入的研究,例如CTL和LTL,但由于QCTL的邏輯理論的特殊性,傳統(tǒng)的方法學并不適用。基于
【學位授予單位】：中國科學院研究生院（成都計算機應用研究所）
【學位級別】：博士
【學位授予年份】：2006
【分類號】：TP302

【共引文獻】

相關期刊論文 前10條

1 付敏;;語義封閉性、“真矛盾論”與“悖論邏輯”[J];安徽大學學報(哲學社會科學版);2009年05期

2 劉志鋒;葛云;章東;周從華;;知識時態(tài)邏輯有界模型檢測中的完備性(英文)[J];Journal of Southeast University(English Edition);2010年03期

3 虞蕾;趙宗濤;;PSL的有界模型檢驗[J];電子學報;2009年03期

4 劉春;王越;金芝;;基于知識的軟件可信性需求獲取[J];電子學報;2010年S1期

5 段采宇;張維明;余濱;;武器裝備需求問題框架及特性分析[J];國防科技大學學報;2009年03期

6 杜國平;;經典邏輯視野中的弗協(xié)調邏輯[J];華南師范大學學報(社會科學版);2007年05期

7 Walter Hussak;;Formal Reduction of Interfaces to Large-scale Process Control Systems[J];International Journal of Automation & Computing;2007年04期

8 ;Formal verification of safety protocol in train control system[J];Science China(Technological Sciences);2011年11期

9 ;Capability description and discovery of Internetware entity[J];Science China(Information Sciences);2010年04期

10 周從華;陳振宇;鞠時光;;基于SAT的軟件驗證[J];計算機研究與發(fā)展;2008年S1期

相關博士學位論文 前10條

1 楊琛;打結不變的命題投影時序邏輯與模型檢測[D];西安電子科技大學;2010年

2 舒新峰;投影時序邏輯的完備公理系統(tǒng)與形式驗證[D];西安電子科技大學;2010年

3 田聰;命題投影時序邏輯的判定性、復雜性、表達性及模型檢測[D];西安電子科技大學;2010年

4 涂鈺青;基于IEC61499標準的組件化模型集成數控系統(tǒng)形式化建模與驗證的研究[D];華南理工大學;2011年

5 陳靖;帶實時的傳值與移動系統(tǒng)研究[D];中國科學院研究生院（軟件研究所）;2003年

6 蔣建民;對稱與動作細化[D];中國科學院研究生院（成都計算機應用研究所）;2006年

7 孫秀莉;基于動作細化的異步電路自動綜合[D];中國科學院研究生院（成都計算機應用研究所）;2005年

8 江敏;多視點需求工程中不一致性的檢測與處理[D];武漢大學;2007年

9 張海賓;混合系統(tǒng)的形式化驗證[D];西安電子科技大學;2007年

10 鄧小妮;基于模型檢驗與仿真的C~4ISR系統(tǒng)需求驗證方法研究[D];國防科學技術大學;2008年

相關碩士學位論文 前10條

1 韓冰;線性時序邏輯在失業(yè)保險審計中的應用研究[D];哈爾濱工程大學;2010年

2 賀楊成;基于RCP的GIS系統(tǒng)及聚類技術研究[D];江南大學;2011年

3 高靜;面向環(huán)境演算系統(tǒng)的模型檢測算法的研究[D];南京航空航天大學;2009年

4 余加振;基于OOR框架的作戰(zhàn)任務分析方法研究[D];國防科學技術大學;2010年

5 劉友澈;紡織車間集散型生產管理與監(jiān)測系統(tǒng)研究[D];電子科技大學;2011年

6 王莉萍;基于網絡的工業(yè)設計信息系統(tǒng)的研究與實現[D];西北工業(yè)大學;2003年

7 徐藝;人機工程設計信息系統(tǒng)研究[D];西北工業(yè)大學;2004年

8 徐雨波;實時系統(tǒng)模型檢測工具FPTAT的算法與實現[D];中國科學院研究生院（軟件研究所）;2005年

9 李明宇;UML模型一致性檢測的研究[D];山東大學;2005年

10 王朝陽;軍隊院校數字化校園建設問題研究[D];國防科學技術大學;2005年

，

本文編號：2617184