2026-03-07T20:41:19Z https://ipsj.ixsq.nii.ac.jp/oai

oai:ipsj.ixsq.nii.ac.jp:00058560 2025-01-22T03:58:47Z 1164:5305:5318:5320

ゲームシナリオのモデル検査 Model Checking for Game Scenarios 清木昌 Masashi, Seiki As an attempt to reduce the production costs of games with interactive stories using computer science methodologies this thesis proposes applying the model checking theory to game scenario verification. It enables systematic and automatic verification of consistency conditions such as reachability and freeness from infinite loops. The simplest model checking method enumerate all states explicitly. However as is well known the "state explosion problem" instantly occurs in this method. Thus we apply symbolic model checking techniques based on BDDs (Binary Decision Diagrams) and CTL (Computation Tree Logic) is adopted to represent specifications. By representing the state space symbolically we are able to deal with mass states are their relational operation as an logical formula and its logical operation. Nevertheless the computation time is still large. To reduce the time we focus on characteristics of game scenarios. The transition graph for a typical game scenario is divided into clusters more clearly than the ones for ordinary targets of model checking. The number of checked states is further reduced by the optimization with the live variable analysis. By using these methods we checked two temporal properties of a game scenario of commercial PC game software reachability and freeness from infinite loops in about five minutes. As an attempt to reduce the production costs of games with interactive stories using computer science methodologies, this thesis proposes applying the model checking theory to game scenario verification. It enables systematic and automatic verification of consistency conditions such as reachability and freeness from infinite loops. The simplest model checking method enumerate all states explicitly. However, as is well known, the "state explosion problem" instantly occurs in this method. Thus, we apply symbolic model checking techniques based on BDDs (Binary Decision Diagrams), and CTL (Computation Tree Logic) is adopted to represent specifications. By representing the state space symbolically, we are able to deal with mass states are their relational operation as an logical formula and its logical operation. Nevertheless, the computation time is still large. To reduce the time, we focus on characteristics of game scenarios. The transition graph for a typical game scenario is divided into clusters more clearly than the ones for ordinary targets of model checking. The number of checked states is further reduced by the optimization with the live variable analysis. By using these methods, we checked two temporal properties of a game scenario of commercial PC game software, reachability and freeness from infinite loops, in about five minutes. 情報処理学会 2004-03-09 jpn technical report https://ipsj.ixsq.nii.ac.jp/records/58560 AA11362144 情報処理学会研究報告ゲーム情報学（GI） 2004 28(2003-GI-011) 51 56 https://ipsj.ixsq.nii.ac.jp/record/58560/files/IPSJ-GI03011010.pdf application/pdf 729.7 kB 2006-03-09