本文選題：模型檢測 + 交互時序邏輯�。� 參考：《鄭州大學》2017年碩士論文

【摘要】：模型檢測是由美國Clarke教授等提出的一種用于自動化驗證有窮狀態(tài)并發(fā)系統(tǒng)的技術(shù)。該技術(shù)通過窮舉搜索狀態(tài)空間的模型檢測算法來驗證系統(tǒng)模型是否符合預(yù)期屬性。由于狀態(tài)空間隨著系統(tǒng)規(guī)模急劇增長,符號化模型檢測被提出從而有效地緩解狀態(tài)空間爆炸問題。驗證對弈中某方是否存在必勝策略是博弈論中研究的一個主要問題�；诜柲Ｐ蜋z測的高效性,模型檢測可以應(yīng)用于博弈游戲的驗證。交互時序邏輯ATL對計算樹邏輯進行了擴充,可以用來描述開放系統(tǒng)的性質(zhì)。利用ATL符號模型檢測算法可以對博弈游戲模型進行驗證。然而,一些博弈游戲的狀態(tài)空間過于龐大,需要對博弈模型檢測方法進一步改進來擴大可驗證系統(tǒng)的規(guī)模。本課題組前期在NSFC的支持下,在圍棋中引入模型檢測技術(shù)從而在一定范圍內(nèi)實施窮舉搜索。然而,實施圍棋模型檢測的關(guān)鍵在于狀態(tài)空間,如何約簡狀態(tài)空間是當前迫切需要解決的問題。針對以上的問題,本文做了一些工作如下:1)在博弈游戲的必勝策略檢測驗證中引入了ATL模型檢測技術(shù)。用ATL對經(jīng)典博弈游戲井字棋進行了建模與分析,實驗結(jié)果與其他方法驗證的結(jié)果一致。2)將對稱技術(shù)應(yīng)用于博弈模型檢測中,提出了基于對稱技術(shù)的博弈模型約簡方法。由于很多博弈游戲具有重復(fù)的特征,對稱技術(shù)可以有效地用于博弈模型的約簡。3)對圍棋的博弈模型進行約簡,并用符號模型檢測算法在小棋盤進行了必勝策略檢測驗證,表明了模型檢測技術(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.
【學位授予單位】：鄭州大學
【學位級別】：碩士
【學位授予年份】：2017
【分類號】：TP317;TP311.53

【相似文獻】

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

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

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

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

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

5 劉吉鋒;孫吉貴;;基于抽象-驗證-細化范例的軟件模型檢測[J];計算機科學;2006年12期

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

7 王飛明;胡元闖;董榮勝;;模型檢測研究進展[J];廣西科學院學報;2008年04期

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

5 劉劍;傳值進程與移動進程的模型檢測方法[D];中國科學院研究生院（軟件研究所）;2005年

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

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

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

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

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

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

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

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

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

4 張興興;基于廣義可能性測度的互模擬及CTL不動點語義[D];陜西師范大學;2015年

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

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

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

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

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

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

，

本文編號：1942555