概要

本研究はボードゲームBAOを形式的に記述しその動作を解析することで，この
ゲームの特徴を明らかにしたものである．

BAOはMancalaと呼ばれるグループの一種である．Mancalaの歴史は古く，今も
世界各地で広く親しまれている．そのルールは単純で2人のプレイヤーが穴に
入った石を交互に動かして取り合い，石の総数を競うゲームである．石の動か
す規則は単純だが，BAOの場合は1手で局面が大きく変化するという特徴を持つ．
そのため人間の手で次の着手を先読みすることは難しい．その一方でBAOのも
つ探索空間は比較的狭く，1手の動きは確定的であるため，コンピュータ上で
実装しやすい．しかしBAOに関する研究は少なく，戦略の有効性や動きの解析
はほとんど行われていない．

対戦実験の結果から，BAOでは他のボードゲームでは見られない興味深い特徴
を持つことが分かった．BAOは石の動きの規則から，千日手以外にゲームが終
了しない状態が存在する．それは特定の局面およびそのときに選択される穴に
よって，1手の間に盤面の変化は停止せずしかも周期的な変化をする場合であ
る．

本研究ではBAOの持つこの特徴を調べるため，プロセス代数とモデルチェッカ
という形式検証で使われているツールを使用し，動作の記述や検証を行う．形
式検証の手法を使うことで検証を機械的にできかつその正しさを保証すること
ができる．まずBAOの動きと性質をプロセス代数CCSで記述し，1手が終了せず
盤面が周期的に変化する動きを調べる．次にモデルチェッカSPINを用いて初期
局面から到達可能な終了しない手筋を自動検出し，検出した周期性を持つ局面
に関して解析する．1手が終了しない局面はその周期で大きく2種類に分類され
る．それぞれについて解析を行ない，局面が周期性を持つために必要な条件を
求める．また1手の動きを逆向きに解析することで1手が停止するための条件を
求める．そして解析した1手が終了しない条件と1手の停止条件は同時に満たさ
れないことを示す．

さらにBAOを実装し対戦を行うことで，先読みによる評価関数を強化する．そ
の結果，獲得する石だけでなく局面の静的評価が評価値として重要であること
が分かった．

発表論文
"ボードゲームBAOの対戦戦略の解析と評価,"
情報科学技術フォーラム(FIT)2003論文集, pp.271--273, 2003.

"ボードゲームBAOの CCS による記述と解析",
情報処理学会第48回プログラミング研究会発表資料, 2004.

"ボードゲームBAOの動作の解析とモデルチェッカによる検証"
第9回ゲームプログラミングワークショップ2004, pp.151--158, 2004.

"ボードゲームBAOにおける周期的動作の解析,"
情報処理学会研究報告, 2005-MPS-53, pp.29--32, 2005.

"ボードゲームBAOにおける周期的動作の解析,"
情報処理学会論文誌：数理モデル化と応用，Vol.46, No.SIG17(TOM13),
pp.88-101, December, 2005.