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

【共引文獻(xiàn)】

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

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

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

3 虞蕾;趙宗濤;;PSL的有界模型檢驗(yàn)[J];電子學(xué)報(bào);2009年03期

4 劉春;王越;金芝;;基于知識(shí)的軟件可信性需求獲取[J];電子學(xué)報(bào);2010年S1期

5 段采宇;張維明;余濱;;武器裝備需求問(wèn)題框架及特性分析[J];國(guó)防科技大學(xué)學(xué)報(bào);2009年03期

6 杜國(guó)平;;經(jīng)典邏輯視野中的弗協(xié)調(diào)邏輯[J];華南師范大學(xué)學(xué)報(bào)(社會(huì)科學(xué)版);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 周從華;陳振宇;鞠時(shí)光;;基于SAT的軟件驗(yàn)證[J];計(jì)算機(jī)研究與發(fā)展;2008年S1期

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

1 楊琛;打結(jié)不變的命題投影時(shí)序邏輯與模型檢測(cè)[D];西安電子科技大學(xué);2010年

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

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

4 涂鈺青;基于IEC61499標(biāo)準(zhǔn)的組件化模型集成數(shù)控系統(tǒng)形式化建模與驗(yàn)證的研究[D];華南理工大學(xué);2011年

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

6 蔣建民;對(duì)稱(chēng)與動(dòng)作細(xì)化[D];中國(guó)科學(xué)院研究生院（成都計(jì)算機(jī)應(yīng)用研究所）;2006年

7 孫秀莉;基于動(dòng)作細(xì)化的異步電路自動(dòng)綜合[D];中國(guó)科學(xué)院研究生院（成都計(jì)算機(jī)應(yīng)用研究所）;2005年

8 江敏;多視點(diǎn)需求工程中不一致性的檢測(cè)與處理[D];武漢大學(xué);2007年

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

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

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

1 韓冰;線性時(shí)序邏輯在失業(yè)保險(xiǎn)審計(jì)中的應(yīng)用研究[D];哈爾濱工程大學(xué);2010年

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

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

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

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

6 王莉萍;基于網(wǎng)絡(luò)的工業(yè)設(shè)計(jì)信息系統(tǒng)的研究與實(shí)現(xiàn)[D];西北工業(yè)大學(xué);2003年

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

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

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

10 王朝陽(yáng);軍隊(duì)院校數(shù)字化校園建設(shè)問(wèn)題研究[D];國(guó)防科學(xué)技術(shù)大學(xué);2005年

，

本文編號(hào)：2617184