【摘要】：模型檢測是一種應(yīng)用于驗證并發(fā)系統(tǒng)性質(zhì)的自動化技術(shù),其中系統(tǒng)性質(zhì)規(guī)約用時序邏輯公式描述,檢測過程依賴于高效靈活的基于圖理論的可達問題算法。模型檢測技術(shù)吸引了國內(nèi)外學(xué)者的高度重視得到了飛速發(fā)展,并廣泛應(yīng)用到社會的各個領(lǐng)域,如電路設(shè)計、協(xié)議驗證等。隨著人工智能技術(shù)的發(fā)展,智能產(chǎn)品出現(xiàn)在人們的生活中,如智能家居、百度地圖的智能路線規(guī)劃、網(wǎng)站推薦和過濾商品、機器人足球賽。雖然這些智能產(chǎn)品給人們帶來了極大便利,但是也引入了很多安全隱患。因此,近年來很多學(xué)者致力于研究如何保障智能產(chǎn)品的安全性問題,其中模型檢測方法已經(jīng)應(yīng)用到人工智能領(lǐng)域中并取得了顯著成果。模型檢測中系統(tǒng)的性質(zhì)用時序邏輯公式形式化描述,所以時序邏輯在模型檢測方法中起著至關(guān)重要的作用。交替時序邏輯(Alternating Temporal Logic,簡稱ATL)是Alur提出的應(yīng)用于驗證反應(yīng)系統(tǒng)性質(zhì)的時序邏輯,其將反應(yīng)系統(tǒng)的交互過程看作是開放系統(tǒng)與外界環(huán)境的博弈過程。命題投影時序邏輯(Proposition Projection Temporal Logic,簡稱PPTL)可以方便的描述有窮或無窮狀態(tài)路徑的性質(zhì);PPTL公式簡潔直觀并且可以表達完全正則性質(zhì),在模型檢測領(lǐng)域起著舉足輕重的作用。交替投影時序邏輯(Alternating Projection Temporal Logic,簡稱APTL)是PPTL的擴展邏輯,APTL不僅可以表達經(jīng)典時序邏輯LTL可以表達的性質(zhì),而且可以表達與區(qū)間相關(guān)的順序和循環(huán)性質(zhì)以及開放系統(tǒng)和多智能體系統(tǒng)中與博弈相關(guān)的性質(zhì)。本文完善了APTL的邏輯規(guī)則,研究改進了檢查APTL公式可滿足性的方法,并且設(shè)計了APTL符號模型檢測算法。為了實現(xiàn)自動化驗證,開發(fā)了APTL公式的可滿足性檢查工具和APTL模型檢測器。具體工作包括以下四方面:第一,本文完善并證明了APTL的邏輯規(guī)則,基于APTL邏輯規(guī)則研究設(shè)計了將APTL公式轉(zhuǎn)化為范式的算法并開發(fā)了轉(zhuǎn)化器。接著改進了已有的APTL公式的可滿足性檢查方法,具體的檢查過程為:(i)將APTL公式轉(zhuǎn)化為范式,根據(jù)公式的范式構(gòu)造范式圖并且轉(zhuǎn)化為自動機;(ii)將得到的自動機進行轉(zhuǎn)化并化簡;(iii)判斷得到的最簡自動機是否為空,如果自動機為空那么對應(yīng)的APTL公式不可滿足,反之亦然。第二,本文研究設(shè)計了APTL的基于BDD的符號模型檢測算法,詳細過程為:(i)用解釋系統(tǒng)編程語言描述要驗證的系統(tǒng),用APTL公式描述要驗證的系統(tǒng)性質(zhì);(ii)符號化表示系統(tǒng)并且將公式的‘非’轉(zhuǎn)化為范式;(iii)計算所有滿足公式的‘非’的路徑的起始狀態(tài)集合。如果得到的狀態(tài)集合中包含系統(tǒng)的初始狀態(tài),說明系統(tǒng)不滿足該APTL公式;反之則滿足該公式。第三,APTL公式的可滿足性檢查是后續(xù)進行系統(tǒng)驗證的前提。根據(jù)APTL公式可滿足性檢查算法開發(fā)實現(xiàn)了檢查工具APTL2BCG,檢查了三組代表性APTL公式以展示工具強大的工作能力。接著開發(fā)了APTL模型檢測器MCMAS APTL實現(xiàn)了檢測過程的自動化,由于從底層開發(fā)一個完整的模型檢測器是很復(fù)雜的,因此MCMAS APTL利用了多智能體系統(tǒng)模型檢測器MCMAS的系統(tǒng)符號化部分。第四,為了將APTL模型檢測方法應(yīng)用到更復(fù)雜的系統(tǒng)驗證中,我們完善了檢測器MCMAS APTL的功能并提高了檢測效率。文中驗證了云計算中的單點登錄中的OpenID協(xié)議以及機器人足球賽的場景,說明了檢測器MCMAS APTL具有較高的工作效率和實用性。
【學(xué)位授予單位】：西安電子科技大學(xué)
【學(xué)位級別】：博士
【學(xué)位授予年份】：2018
【分類號】：TP18;TP301.1

【相似文獻】

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

1 方建印;謝欣欣;;具有飽和輸入和通信約束的多智能體系統(tǒng)的包含控制[J];河南工程學(xué)院學(xué)報(自然科學(xué)版);2016年04期

2 李健;沈艷軍;劉允剛;;線性多智能體系統(tǒng)一致性的自適應(yīng)動態(tài)規(guī)劃求解方法[J];系統(tǒng)科學(xué)與數(shù)學(xué);2016年07期

3 楊瑞;葉冬;;多智能體系統(tǒng)一致性研究[J];山東工業(yè)技術(shù);2017年07期

4 張曉嬌;崔寶同;齊斌;;二階多智能體系統(tǒng)一致性的幾個條件（英文）[J];控制工程;2017年04期

5 姜香菊;紀(jì)志堅;孫方剛;李自強;;二階多智能體系統(tǒng)的能觀性[J];工業(yè)控制計算機;2017年05期

6 朱美玲;趙蕊;徐勇;;速度不可測的異構(gòu)多智能體系統(tǒng)一致性分析[J];計算機工程與科學(xué);2017年09期

7 莫立坡;于永光;;多智能體系統(tǒng)的有限時間旋轉(zhuǎn)環(huán)繞控制（英文）[J];自動化學(xué)報;2017年09期

8 聞國光;黃俊;于玉潔;;異質(zhì)多智能體系統(tǒng)在固定拓撲下的分組一致性[J];北京交通大學(xué)學(xué)報;2016年03期

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

1 張文廣;郭振凱;;一類高階多智能體系統(tǒng)的一致控制研究[A];中國自動化學(xué)會控制理論專業(yè)委員會C卷[C];2011年

2 陳增強;;多智能體系統(tǒng)魯棒編隊跟蹤控制及包容控制研究[A];2015年中國自動化大會摘要集[C];2015年

3 張馨元;陳中高;吉國華;;基于多智能體系統(tǒng)的建筑自動排布工具原型研究[A];數(shù)字技術(shù)·建筑全生命周期——2018年全國建筑院系建筑數(shù)字技術(shù)教學(xué)與研究學(xué)術(shù)研討會論文集[C];2018年

4 楊洪勇;劉啟明;;時延不同的二階多智能體系統(tǒng)的編隊控制[A];2009中國控制與決策會議論文集（1）[C];2009年

5 薛宏濤;沈林成;;基于協(xié)進化方法的多智能體系統(tǒng)及其符號演繹理論模型[A];第二十六屆中國控制會議論文集[C];2007年

6 虞文武;;多智能體系統(tǒng)分布式協(xié)同控制與優(yōu)化的新挑戰(zhàn)[A];2015年中國自動化大會摘要集[C];2015年

7 楊洪勇;路蘭;李曉;;時延多智能體系統(tǒng)的群集運動[A];第五屆全國復(fù)雜網(wǎng)絡(luò)學(xué)術(shù)會議論文（摘要）匯集[C];2009年

8 梁泉;許曉鳴;張鐘俊;;多智能體系統(tǒng)智能體協(xié)作層的設(shè)計與實現(xiàn)[A];1995年中國智能自動化學(xué)術(shù)會議暨智能自動化專業(yè)委員會成立大會論文集（下冊）[C];1995年

9 鄢昒易;何瀟;王子棟;周東華;;一類LPV多智能體系統(tǒng)的分布式故障診斷[A];第25屆中國控制與決策會議論文集[C];2013年

10 ;索引[A];2012-2013控制科學(xué)與工程學(xué)科發(fā)展報告[C];2014年

相關(guān)重要報紙文章 前1條

1 本報記者 常麗君;讓人類與機器人聯(lián)手[N];科技日報;2016年

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

1 游秀;一類非匹配非線性多智能體系統(tǒng)的分布式一致性控制[D];燕山大學(xué);2017年

2 萬穎;時滯網(wǎng)絡(luò)系統(tǒng)的動力學(xué)分析及采樣控制[D];東南大學(xué);2017年

3 馬婧瑛;多智能體系統(tǒng)的性能優(yōu)化[D];西安電子科技大學(xué);2017年

4 張婷;幾類多智能體系統(tǒng)量化學(xué)習(xí)一致性研究[D];西安電子科技大學(xué);2017年

5 王海洋;APTL模型檢測方法及多智能體系統(tǒng)驗證的研究[D];西安電子科技大學(xué);2018年

6 張卓;多智能體系統(tǒng)協(xié)同控制方法及在分布式衛(wèi)星應(yīng)用研究[D];哈爾濱工業(yè)大學(xué);2017年

7 李平;復(fù)雜條件下多智能體系統(tǒng)的魯棒一致性控制研究[D];電子科技大學(xué);2017年

8 陳凱銳;多智能體系統(tǒng)一致性控制若干問題研究[D];廣東工業(yè)大學(xué);2017年

9 徐云劍;幾類多智能體系統(tǒng)的一致性問題研究[D];廣東工業(yè)大學(xué);2017年

10 梁洪晶;多智能體系統(tǒng)的協(xié)同控制及輸出調(diào)節(jié)問題研究[D];東北大學(xué);2016年

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

1 楊東岳;存在外部擾動的線性多智能體系統(tǒng)分布式協(xié)調(diào)控制[D];哈爾濱工業(yè)大學(xué);2017年

2 梁建;異質(zhì)網(wǎng)絡(luò)中二階多智能體系統(tǒng)分布式協(xié)調(diào)控制[D];哈爾濱工業(yè)大學(xué);2017年

3 劉洪明;復(fù)雜網(wǎng)絡(luò)滯后同步與牽制控制多智能體系統(tǒng)一致性[D];杭州電子科技大學(xué);2018年

4 張增英;多智能體系統(tǒng)群集行為動力學(xué)分析及控制方法研究[D];蘭州交通大學(xué);2017年

5 謝朝龍;基于Web的多智能體系統(tǒng)實驗平臺的設(shè)計與實現(xiàn)[D];哈爾濱工業(yè)大學(xué);2018年

6 陳亞楠;異質(zhì)多智能體系統(tǒng)基于事件的一致性和包圍控制[D];青島大學(xué);2018年

7 付芳芳;高階線性時滯多智能體系統(tǒng)的一致性[D];曲阜師范大學(xué);2018年

8 陳春楊;帶有隨機延遲和拓撲的多智能體系統(tǒng)一致性研究[D];江南大學(xué);2018年

9 李曉;多智能體系統(tǒng)L_2-L_∞一致性研究[D];安徽工業(yè)大學(xué);2018年

10 桑成艷;幾類隨機多智能體系統(tǒng)的一致性研究[D];安徽工業(yè)大學(xué);2018年

本文編號：2757845