本文關(guān)鍵詞：責(zé)任政策形式化驗(yàn)證方法

  更多相關(guān)文章： 多Agent系統(tǒng) 形式化方法 政策建模 社會承諾 模型檢測 責(zé)任政策

【摘要】：為了驗(yàn)證多Agent系統(tǒng)設(shè)計(jì)的正確性,將責(zé)任政策作為約束多Agent交互行為的高層"需求規(guī)格"或"通信協(xié)議",對其進(jìn)行形式化建模及驗(yàn)證。研究了建模責(zé)任政策的形式化框架語言,基于責(zé)任狀態(tài)模型建模責(zé)任政策的動態(tài)演化過程。給出了政策模型形式化驗(yàn)證方法,將政策模型的操作語義定義為Kripke結(jié)構(gòu)的狀態(tài)遷移系統(tǒng),政策中Agent行為的約束規(guī)則聲明為線性時(shí)序邏輯公式,使用模型檢測器Nu SMV驗(yàn)證政策模型對線性時(shí)序邏輯公式的可滿足性。實(shí)驗(yàn)結(jié)果表明,該方法可有效分析責(zé)任政策的設(shè)計(jì)缺陷,提高多Agent系統(tǒng)設(shè)計(jì)的正確性。
【作者單位】： 哈爾濱工程大學(xué)計(jì)算機(jī)科學(xué)與技術(shù)學(xué)院;哈爾濱工程大學(xué)信息與通信工程學(xué)院;
【關(guān)鍵詞】： 多Agent系統(tǒng) 形式化方法 政策建模 社會承諾 模型檢測 責(zé)任政策
【基金】：國家科技支撐計(jì)劃(2012BAH08B02) 中央高�；究蒲袠I(yè)務(wù)費(fèi)專項(xiàng)基金項(xiàng)目(HEUCF100603,HEUCF041204) 黑龍江省博士后基金資助項(xiàng)目(3236310148)
【分類號】：TP18;D035
【正文快照】： 復(fù)雜適應(yīng)系統(tǒng)中多Agent間的行為交互是系統(tǒng)具備“適應(yīng)性”的前提,也是導(dǎo)致系統(tǒng)“復(fù)雜性”的主要原因之一[1]。為在系統(tǒng)設(shè)計(jì)過程中正確建模A-gent間的交互行為,本文提出一種多Agent系統(tǒng)責(zé)任政策的形式化驗(yàn)證方法。多Agent系統(tǒng)中,責(zé)任一般是Agent為了滿足某些要求而執(zhí)行的動作[2

【相似文獻(xiàn)】

中國重要會議論文全文數(shù)據(jù)庫 前7條

1 高靜;曹子寧;;基于空間邏輯和計(jì)算樹邏輯的模型檢測[A];2009年中國高校通信類院系學(xué)術(shù)研討會論文集[C];2009年

2 許梅;曹子寧;;基于謂詞μ演算和空間邏輯的模型檢測算法研究[A];2009年中國高校通信類院系學(xué)術(shù)研討會論文集[C];2009年

3 何青;駱翔宇;蘇開樂;;對弈必勝策略的符號化模型檢測[A];2006年全國理論計(jì)算機(jī)科學(xué)學(xué)術(shù)年會論文集[C];2006年

4 王飛明;胡元闖;董榮勝;;模型檢測中狀態(tài)爆炸及其優(yōu)化策略研究[A];廣西計(jì)算機(jī)學(xué)會2008年年會論文集[C];2008年

5 陳道喜;張廣泉;陳冬火;;NSPK協(xié)議的Spin模型檢測[A];2008年全國開放式分布與并行計(jì)算機(jī)學(xué)術(shù)會議論文集(下冊)[C];2008年

6 邢立國;張光甫;劉薇;胥維昌;金一和;;人皮膚模型評價(jià)殺菌類農(nóng)藥腐蝕/刺激性研究[A];2014線粒體毒性與基于毒性通路的安全性評價(jià)新策略學(xué)術(shù)研討會暨中國毒理學(xué)會毒理學(xué)替代法與轉(zhuǎn)化毒理學(xué)專業(yè)委員會成立大會論文集[C];2014年

7 張明玉;;我國對外開放、通貨膨脹與經(jīng)濟(jì)增長相關(guān)關(guān)系的模型檢測[A];面向21世紀(jì)的科技進(jìn)步與社會經(jīng)濟(jì)發(fā)展（下冊）[C];1999年

中國博士學(xué)位論文全文數(shù)據(jù)庫 前10條

1 江華;界程演算模型檢測[D];貴州大學(xué);2008年

2 林榮德;移動界程演算及模型檢測應(yīng)用的關(guān)鍵問題研究[D];華南理工大學(xué);2010年

3 劉劍;傳值進(jìn)程與移動進(jìn)程的模型檢測方法[D];中國科學(xué)院研究生院（軟件研究所）;2005年

4 劉志鋒;模型檢測中關(guān)鍵技術(shù)的研究及其應(yīng)用[D];南京大學(xué);2011年

5 朱維軍;時(shí)間區(qū)間時(shí)序邏輯模型檢測：理論、算法及應(yīng)用[D];西安電子科技大學(xué);2011年

6 尹良澤;基于SAT的組合遷移系統(tǒng)模型檢測技術(shù)研究[D];清華大學(xué);2014年

7 陳冬火;超協(xié)調(diào)時(shí)序邏輯及其模型檢測方法[D];中國科學(xué)院研究生院（成都計(jì)算機(jī)應(yīng)用研究所）;2006年

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

9 黃宏濤;基于懶惰切片的模型檢測技術(shù)研究[D];哈爾濱工程大學(xué);2012年

10 劉金卓;基于符號化模型檢測的軟件演化過程模型驗(yàn)證[D];云南大學(xué);2013年

中國碩士學(xué)位論文全文數(shù)據(jù)庫 前10條

1 張衍志;符號化模型檢測算法的研究[D];吉林大學(xué);2009年

2 黎吾平;模型檢測在軟件方面的應(yīng)用[D];吉林大學(xué);2008年

3 吳小娟;并行完備模型檢測技術(shù)的研究[D];電子科技大學(xué);2013年

4 姜志敏;模型檢測在配置中的應(yīng)用[D];吉林大學(xué);2010年

5 金怡愛;基于模型檢測方法的規(guī)劃[D];吉林大學(xué);2005年

6 施小純;基于反例搜索的啟發(fā)式模型檢測算法的研究[D];中國科學(xué)院研究生院（軟件研究所）;2004年

7 王舒鵬;基于外存的大規(guī)模模型檢測新方法的研究[D];電子科技大學(xué);2015年

8 陳亞軍;模型檢測在安全協(xié)議形式化驗(yàn)證中的應(yīng)用[D];電子科技大學(xué);2012年

9 殷朝冉;測試目的引導(dǎo)的模型檢測方法與技術(shù)研究[D];北方工業(yè)大學(xué);2015年

10 廉智超;模型檢測在模型診斷領(lǐng)域中的應(yīng)用[D];吉林大學(xué);2007年

，

本文編號：814021