本文選題：模型檢測 + 交互時(shí)序邏輯��； 參考：《鄭州大學(xué)》2017年碩士論文

【摘要】：模型檢測是由美國Clarke教授等提出的一種用于自動(dòng)化驗(yàn)證有窮狀態(tài)并發(fā)系統(tǒng)的技術(shù)。該技術(shù)通過窮舉搜索狀態(tài)空間的模型檢測算法來驗(yàn)證系統(tǒng)模型是否符合預(yù)期屬性。由于狀態(tài)空間隨著系統(tǒng)規(guī)模急劇增長,符號(hào)化模型檢測被提出從而有效地緩解狀態(tài)空間爆炸問題。驗(yàn)證對(duì)弈中某方是否存在必勝策略是博弈論中研究的一個(gè)主要問題�；诜�(hào)模型檢測的高效性,模型檢測可以應(yīng)用于博弈游戲的驗(yàn)證。交互時(shí)序邏輯ATL對(duì)計(jì)算樹邏輯進(jìn)行了擴(kuò)充,可以用來描述開放系統(tǒng)的性質(zhì)。利用ATL符號(hào)模型檢測算法可以對(duì)博弈游戲模型進(jìn)行驗(yàn)證。然而,一些博弈游戲的狀態(tài)空間過于龐大,需要對(duì)博弈模型檢測方法進(jìn)一步改進(jìn)來擴(kuò)大可驗(yàn)證系統(tǒng)的規(guī)模。本課題組前期在NSFC的支持下,在圍棋中引入模型檢測技術(shù)從而在一定范圍內(nèi)實(shí)施窮舉搜索。然而,實(shí)施圍棋模型檢測的關(guān)鍵在于狀態(tài)空間,如何約簡狀態(tài)空間是當(dāng)前迫切需要解決的問題。針對(duì)以上的問題,本文做了一些工作如下:1)在博弈游戲的必勝策略檢測驗(yàn)證中引入了ATL模型檢測技術(shù)。用ATL對(duì)經(jīng)典博弈游戲井字棋進(jìn)行了建模與分析,實(shí)驗(yàn)結(jié)果與其他方法驗(yàn)證的結(jié)果一致。2)將對(duì)稱技術(shù)應(yīng)用于博弈模型檢測中,提出了基于對(duì)稱技術(shù)的博弈模型約簡方法。由于很多博弈游戲具有重復(fù)的特征,對(duì)稱技術(shù)可以有效地用于博弈模型的約簡。3)對(duì)圍棋的博弈模型進(jìn)行約簡,并用符號(hào)模型檢測算法在小棋盤進(jìn)行了必勝策略檢測驗(yàn)證,表明了模型檢測技術(shù)及其約簡算法在圍棋博弈中的有效性和可行性。
[Abstract]:Model checking is a technique proposed by Professor Clarke of the United States to automate the verification of finite state concurrency systems. This technique verifies whether the system model conforms to expected attributes by exhaustive search of the model checking algorithm of state space. As the state space increases rapidly with the system scale, symbolic model detection is proposed to effectively alleviate the state space explosion problem. To verify the existence of a winning strategy is a major problem in game theory. Based on the efficiency of symbolic model detection, model detection can be applied to game verification. Interactive temporal logic (ATL) extends computing tree logic to describe the properties of open systems. ATL symbol model detection algorithm can be used to verify the game model. However, the state space of some game games is too large, so it is necessary to further improve the game model detection method to expand the scale of the verifiable system. With the support of NSFC, the research group introduced model checking technology in go to carry out exhaustive search in a certain range. However, the key to implement go model detection is the state space. How to reduce the state space is an urgent problem to be solved. In order to solve the above problems, this paper does some work as follows: (1) the ATL model detection technique is introduced in the verification of the winning strategy of game games. In this paper, ATL is used to model and analyze the classical game well word chess. The experimental results are in agreement with the results of other methods. (2) the symmetry technique is applied to the game model detection, and a game model reduction method based on the symmetry technology is proposed. Because many game games have the characteristics of repetition, symmetry technique can be used to reduce the game model of go effectively, and the sign model detection algorithm is used to test the winning strategy on the small chessboard. The effectiveness and feasibility of model detection and its reduction algorithm in go game are demonstrated.
【學(xué)位授予單位】：鄭州大學(xué)
【學(xué)位級(jí)別】：碩士
【學(xué)位授予年份】：2017
【分類號(hào)】：TP317;TP311.53

【相似文獻(xiàn)】

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

1 林惠民,張文輝;模型檢測:理論、方法與應(yīng)用[J];電子學(xué)報(bào);2002年S1期

2 戎玫;張廣泉;;模型檢測新技術(shù)研究[J];計(jì)算機(jī)科學(xué);2003年05期

3 肖健宇;張德運(yùn);鄭衛(wèi)斌;;過程提取用于改善程序模型檢測的可伸縮性[J];西安交通大學(xué)學(xué)報(bào);2006年06期

4 袁志斌;徐正權(quán);王能超;;軟件模型檢測中的抽象[J];計(jì)算機(jī)科學(xué);2006年07期

5 劉吉鋒;孫吉貴;;基于抽象-驗(yàn)證-細(xì)化范例的軟件模型檢測[J];計(jì)算機(jī)科學(xué);2006年12期

6 化志章;吳傳孫;揭安全;薛錦云;;軟件模型檢測新技術(shù)研究[J];微計(jì)算機(jī)信息;2007年36期

7 王飛明;胡元闖;董榮勝;;模型檢測研究進(jìn)展[J];廣西科學(xué)院學(xué)報(bào);2008年04期

8 鄺宏斌;羅貴明;;并行軟件模型檢測[J];計(jì)算機(jī)工程;2008年19期

9 何愷鐸;顧明;宋曉宇;李力;李江;;面向源代碼的軟件模型檢測及其實(shí)現(xiàn)[J];計(jì)算機(jī)科學(xué);2009年01期

10 林璇;;模型檢測方法在入侵檢測中的應(yīng)用研究[J];現(xiàn)代計(jì)算機(jī)(專業(yè)版);2009年02期

相關(guān)會(huì)議論文 前5條

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

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

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

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

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

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

1 高興;武田開始減肥藥ATL—962Ⅲ期臨床試驗(yàn)[N];醫(yī)藥經(jīng)濟(jì)報(bào);2009年

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

1 奚琪;基于模型檢測的二進(jìn)制代碼惡意行為識(shí)別技術(shù)研究[D];解放軍信息工程大學(xué);2014年

2 黃鎮(zhèn)謹(jǐn);基于模型檢測的時(shí)空性能分析若干問題研究[D];合肥工業(yè)大學(xué);2016年

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

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

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

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

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

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

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

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

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

1 焦林楓;基于ATL的博弈模型檢測研究及其在圍棋中的應(yīng)用[D];鄭州大學(xué);2017年

2 李永亮;基于DNA計(jì)算的CTL模型檢測方法研究[D];鄭州大學(xué);2015年

3 楊樹峰;基于統(tǒng)計(jì)模型檢測的無線傳感器網(wǎng)絡(luò)協(xié)議建模與分析[D];鄭州大學(xué);2015年

4 張興興;基于廣義可能性測度的互模擬及CTL不動(dòng)點(diǎn)語義[D];陜西師范大學(xué);2015年

5 王彬;基于多值模型檢測的SaaS應(yīng)用測試及其自動(dòng)化研究[D];陜西師范大學(xué);2015年

6 王凱;基于模型檢測多反例對(duì)軟件進(jìn)行調(diào)試[D];電子科技大學(xué);2015年

7 鄧楠軼;基于廣義可能性測度的模型檢測器GPoCheck的設(shè)計(jì)與實(shí)現(xiàn)[D];陜西師范大學(xué);2015年

8 張恒;多值模型檢測器的研究與實(shí)現(xiàn)[D];陜西師范大學(xué);2015年

9 高毅;不同模型檢測下信號(hào)并串轉(zhuǎn)換模塊功能建模的研究[D];電子科技大學(xué);2014年

10 崔曉爽;基于GSTE模型檢測的信號(hào)并串轉(zhuǎn)換模塊功能驗(yàn)證的研究[D];電子科技大學(xué);2014年

，

本文編號(hào)：1942555