计算机工程与应用 ›› 2008, Vol. 44 ›› Issue (17): 58-60.

• 理论研究 • 上一篇    下一篇

基于符号化模型检测的对弈必胜策略验证

何 青1,骆翔宇2,苏开乐3   

  1. 1.湖南文理学院 计算机科学与技术系，湖南 常德 415000
    2.桂林电子科技大学 计算机与控制学院 计算机系，广西 桂林 541004
    3.中山大学 信息科学与技术学院 计算机科学系，广州 510275
  • 收稿日期:2007-11-09 修回日期:2008-02-03 出版日期:2008-06-11 发布日期:2008-06-11
  • 通讯作者: 何 青

Verifying winning strategy with symbolic model checking

HE Qing1,LUO Xiang-yu2,SU Kai-le3   

  1. 1.Department of Computer Science，Hunan University of Arts and Science，Changde，Hunan 415000，China
    2.Department of Computer Science，Guilin University of Electronic Technology，Guilin，Guangxi 541004，China
    3.Department of Computer Science，Sun Yat-Sen University，Guangzhou 510275，China
  • Received:2007-11-09 Revised:2008-02-03 Online:2008-06-11 Published:2008-06-11
  • Contact: HE Qing

PDF

摘要： 在对弈的研究中，验证对弈双方是否存在必胜策略的问题一直没能很好地解决，因为这涉及到超大规模的状态空间搜索。而随着符号化模型检测技术的发展，大规模系统的验证成为了可能。给出了使用符号化模型检测来验证对弈必胜策略的一般方法，并给出了一个井字棋必胜策略验证的实例。

Abstract: In the research of two-player zero-sum games，verifying whether there exists winning strategy has not been solved properly，since it refers to the search of the grand scale state space.With the development of the symbolic model checking，however，verifying large systems becomes possible.This paper presents a common method of verifying the winning strategy of games with symbolic model checking，and gives a case study of Tic-Tac-Toe.

京ICP备13024262号-1
Copyright © 《计算机工程与应用》编辑部
技术支持：北京玛格泰克科技发展有限公司
总访问量
今日访问
在线人数