作為一種規(guī)范語言,時(shí)序邏輯已經(jīng)被廣泛用于計(jì)算機(jī)程序、數(shù)字電路和通信協(xié)議的驗(yàn)證以及人工智能的時(shí)序推理中。此外,時(shí)序邏輯也被用作程序設(shè)計(jì)語言來編寫程序。一個(gè)時(shí)序邏輯程序設(shè)計(jì)語言編寫的程序稱作是一個(gè)時(shí)序邏輯程序,其本質(zhì)上是一個(gè)時(shí)序邏輯公式。跟傳統(tǒng)的非形式化編程語言（如Pascal,C等）不同,時(shí)序邏輯程序的執(zhí)行過程是根據(jù)給定的規(guī)則對(duì)公式進(jìn)行化簡的過程。通常時(shí)序邏輯程序的執(zhí)行過程更加復(fù)雜,執(zhí)行效率已經(jīng)成為影響時(shí)序邏輯程序能否應(yīng)用于實(shí)際大型復(fù)雜系統(tǒng)的一個(gè)關(guān)鍵因素。為此,本文以建模、仿真和驗(yàn)證語言MSVL（Modeling,Simulation and Verification Language）為研究對(duì)象,提出了一種MSVL程序的編譯執(zhí)行方法并實(shí)現(xiàn)了一個(gè)MSVL編譯器。在此基礎(chǔ)上,研究了基于MSVL和MSVL編譯器的C程序驗(yàn)證方法以及自動(dòng)規(guī)劃方法。此外,為了支持對(duì)C程序的時(shí)序性質(zhì)驗(yàn)證,研究了時(shí)序性質(zhì)自動(dòng)挖掘方法從程序中挖掘PPTL（Propositional Projection Temporal Logic）性質(zhì)。本文主要工作概括如下:第一,為了高效執(zhí)行MSVL程序,提出了一種MSVL程序的編... 

【文章來源】：西安電子科技大學(xué)陜西省 211工程院校 教育部直屬院校

【文章頁數(shù)】：137 頁

【學(xué)位級(jí)別】：博士

【部分圖文】：

例子C程序Exa1.c

例2.1. MSVL程序frame(x) and ((int x<==2 or int x<==3)and (while(x<5){x:=x+2}))對(duì)應(yīng)的NFG如圖2.2所示。圖2.2 MSVL程序的NFG圖示2.3 命命題題投投影影時(shí)時(shí)序序邏邏輯輯本節(jié)介紹命題投影時(shí)序邏輯PPTL。PPTL是投影時(shí)序邏輯PTL的一個(gè)子集。準(zhǔn)確地說，PPTL是PTL的命題形式。PPTL中不包含PTL中的一階成分，例如變量，謂詞和量詞。文章[10, 11]證明了PPTL是可判定的，并給出了PPTL的判定過程。此外，文章[129]中證明PPTL的表達(dá)能力是完全正則的。本節(jié)簡單介紹PPTL的語法和語義，以及PPTL公式對(duì)應(yīng)的帶標(biāo)記的范式圖（Labeled Normal Form Graph，簡稱LNFG）[11, 28]。2.3.1語法和語義一個(gè)PPTL公式 在一個(gè)可數(shù)的原子命題集合P上的歸納定義如下： ::= | ○ | | ∨ | ( 1

“?”表示任意命題可能在該狀態(tài)成立。作為對(duì)比，圖2.3給出了PPTL公式 ( ; )+對(duì)應(yīng)的LNFG。直觀地，該公式表示從區(qū)間的某個(gè)狀態(tài)開始，命題 和 周期重復(fù)成立，且至少重復(fù)一次。同樣的，圖2.6給出了滿足了四個(gè)滿足公式 ( ; )+的狀態(tài)區(qū)間的例子。圖2.4中的狀態(tài)區(qū)間1滿足公式 ( ; )*但不滿足公式 ( ; )+。圖2.3公式 ( ; )*對(duì)應(yīng)的LNFG圖2.4滿足公式 ( ; )*的狀態(tài)區(qū)間圖示2.4 本本章章小小結(jié)結(jié)本章簡要介紹了本文的研究基礎(chǔ)，包括一階投影時(shí)序邏輯PTL的語法和語義，24

【參考文獻(xiàn)】：
期刊論文
[1]基于線性時(shí)序邏輯的移動(dòng)端快遞派送路徑規(guī)劃[J]. 禹鑫燚,郭永奎,歐林林,汪濤,盧靚,張愛美.  高技術(shù)通訊. 2017(06)
[2]Model checking concurrent systems with MSVL[J]. Nan ZHANG,Zhenhua DUAN,Cong TIAN.  Science China（Information Sciences）. 2016(11)
[3]基于線性時(shí)序邏輯理論的倉儲(chǔ)機(jī)器人路徑規(guī)劃[J]. 禹鑫燚,陳浩,郭永奎,程誠,歐林林,俞立.  高技術(shù)通訊. 2016(01)
[4]未知環(huán)境下移動(dòng)機(jī)器人安全路徑規(guī)劃的一種神經(jīng)網(wǎng)絡(luò)方法[J]. 樊長虹,陳衛(wèi)東,席裕庚.  自動(dòng)化學(xué)報(bào). 2004(06)
[5]大規(guī)模真實(shí)地形數(shù)據(jù)中的全局路徑規(guī)劃方法——基于遺傳算法的研究[J]. 梁曉輝,吳威,趙沁平.  計(jì)算機(jī)研究與發(fā)展. 2002(03)
[6]XYZ系統(tǒng)在電信領(lǐng)域中的應(yīng)用[J]. 沈武威,唐稚松.  軟件學(xué)報(bào). 1996(06)



本文編號(hào)：2989636