多智能體系統(tǒng)模型檢測在分布式系統(tǒng)分析領(lǐng)域越來越受到研究者們的重視。傳統(tǒng)的時態(tài)邏輯模型檢測可以建模和驗證多智能體系統(tǒng)時間性質(zhì)規(guī)范。但是多智能體系統(tǒng)的模型檢測技術(shù)越來越趨向于擬人化方向發(fā)展。對于智能體群體通過策略合作保證某個系統(tǒng)性質(zhì)的成立這一情景,傳統(tǒng)的時態(tài)邏輯是無法描述的。另外,對智能體知識的建模和驗證也是十分重要的科學(xué)問題。本文提出的一種基于動作的時態(tài)認(rèn)知邏輯（ATL*K）能夠有效地描述多智能體系統(tǒng)協(xié)議和認(rèn)知特性。此邏輯可分為時態(tài)部分和認(rèn)知部分:時態(tài)部分有線性時態(tài)和基于動作的分叉時態(tài);認(rèn)知部分是對知識性質(zhì)的擴(kuò)展,加入全知和公共知識等知識形態(tài)。如何判定智能體合作保證系統(tǒng)性質(zhì)的成立和智能體知識性質(zhì)的成立是模型檢測基于動作的時態(tài)認(rèn)知邏輯的關(guān)鍵性問題。本文提出了一種混合遷移系統(tǒng)（Mixed Transition System,MTS）,在該系統(tǒng)模型M下提出驗證各類ATL*K邏輯公式的模型檢測算法�？偨Y(jié)文章給出的基于動作的多智能體系統(tǒng)時態(tài)認(rèn)知邏輯模型檢測的研究,主要的研究工作可概括如下:（1）基于傳統(tǒng)的多智能體系統(tǒng)Kripke結(jié)構(gòu),提出基于動作的解釋系統(tǒng)模型IS和推導(dǎo)模型M,給出了M的描述語言及... 

【文章來源】：華僑大學(xué)福建省

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

【學(xué)位級別】：碩士

【文章目錄】：
摘要
Abstract
第1章 引言
    1.1 研究背景和意義
        1.1.1 模型檢測起源與意義
        1.1.2 模型檢測技術(shù)的應(yīng)用和發(fā)展
    1.2 國內(nèi)外研究現(xiàn)狀
        1.2.1 多智能體系統(tǒng)基于動作的邏輯研究現(xiàn)狀
        1.2.2 多智能體時態(tài)認(rèn)知邏輯模型檢測
    1.3 本課題的主要研究內(nèi)容與創(chuàng)新點(diǎn)
        1.3.1 研究內(nèi)容
        1.3.2 創(chuàng)新點(diǎn)
    1.4 論文的框架結(jié)構(gòu)
    1.5 本章小結(jié)
第2章 基礎(chǔ)理論
    2.1 形式化驗證技術(shù)
        2.1.1 定理證明
        2.1.2 模型檢測
    2.2 符號運(yùn)算技術(shù)
        2.2.1 OBDD
        2.2.2 SAT
    2.3 知識推理
        2.3.1 語法和語義
        2.3.2 可判定性及公理系統(tǒng)
        2.3.3 完備性和復(fù)雜度
    2.4 本章小結(jié)
第3章 時態(tài)認(rèn)知邏輯ATL*K及其形式模型
    3.1 多智能體系統(tǒng)Kripke模型
    3.2 時態(tài)邏輯CTL*
    3.3 時態(tài)認(rèn)知邏輯ATL*K及其形式模型
        3.3.1 動作的引入以及合作保證語義
        3.3.2 基于動作的多智能體系統(tǒng)形式模型
        3.3.3 ATL*K的語法語義
    3.4 本章小結(jié)
第4章 ATL*K模型檢測
    4.1 不動點(diǎn)計算
    4.2 基于OBDD的ATL*K模型檢測
        4.2.1 動作映射
        4.2.2 帶可觀察變量的有限狀態(tài)程序
        4.2.3 全局可達(dá)狀態(tài)集
        4.2.4 基于動作的時態(tài)算子的模型檢測
        4.2.5 基于局部命題的知識算子模型檢測
        4.2.6 ATL*K符號模型檢測算法實現(xiàn)框架
    4.3 ATL*K模型檢測的建模語言設(shè)計
        4.3.1 環(huán)境的定義
        4.3.2 智能體的定義
        4.3.3 建模語言形式規(guī)范
    4.4 本章小結(jié)
第5章 囚徒與燈泡問題
    5.1 問題描述
    5.2 解決問題的協(xié)議分析及其建模
    5.3 基于MCTK的模型檢測驗證
    5.4 本章小結(jié)
第6章 總結(jié)與展望
    6.1 研究總結(jié)
    6.2 展望未來工作
參考文獻(xiàn)
致謝
個人簡歷、在校期間發(fā)表的學(xué)術(shù)論文和研究成果


【參考文獻(xiàn)】：
期刊論文
[1]一種基于認(rèn)知模型檢測的Web服務(wù)組合驗證方法[J]. 駱翔宇,譚征,蘇開樂,吳立軍.  計算機(jī)學(xué)報. 2011(06)
[2]一種求解認(rèn)知難題的模型檢測方法[J]. 駱翔宇,蘇開樂,顧明.  計算機(jī)學(xué)報. 2010(03)
[3]基于自動推理技術(shù)的智能規(guī)劃方法[J]. 呂帥,劉磊,石蓮,李瑩.  軟件學(xué)報. 2009(05)
[4]符號化模型檢測CTL[J]. 蘇開樂,駱翔宇,呂關(guān)鋒.  計算機(jī)學(xué)報. 2005(11)

博士論文
[1]多智能體系統(tǒng)的符號模型檢測[D]. 駱翔宇.中山大學(xué) 2006
[2]多智能體模型、學(xué)習(xí)和協(xié)作研究與應(yīng)用[D]. 于江濤.浙江大學(xué) 2003

碩士論文
[1]基于多智能體系統(tǒng)模型檢測與抽象技術(shù)的Web服務(wù)組合驗證[D]. 許興旺.華僑大學(xué) 2014
[2]模型檢測在安全協(xié)議驗證中的研究與應(yīng)用[D]. 王敏飛.南京航空航天大學(xué) 2009
[3]多Agent系統(tǒng)合作認(rèn)知邏輯的研究[D]. 陸志浩.南京航空航天大學(xué) 2008



本文編號：3445940