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

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

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

【學位級別】：博士

【部分圖文】：

例子C程序Exa1.c

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

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

【參考文獻】：
期刊論文
[1]基于線性時序邏輯的移動端快遞派送路徑規(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]基于線性時序邏輯理論的倉儲機器人路徑規(guī)劃[J]. 禹鑫燚,陳浩,郭永奎,程誠,歐林林,俞立.  高技術(shù)通訊. 2016(01)
[4]未知環(huán)境下移動機器人安全路徑規(guī)劃的一種神經(jīng)網(wǎng)絡(luò)方法[J]. 樊長虹,陳衛(wèi)東,席裕庚.  自動化學報. 2004(06)
[5]大規(guī)模真實地形數(shù)據(jù)中的全局路徑規(guī)劃方法——基于遺傳算法的研究[J]. 梁曉輝,吳威,趙沁平.  計算機研究與發(fā)展. 2002(03)
[6]XYZ系統(tǒng)在電信領(lǐng)域中的應用[J]. 沈武威,唐稚松.  軟件學報. 1996(06)



本文編號：2989636