著者

清木昌

出版者

一般社団法人情報処理学会

雑誌

情報処理学会研究報告ゲーム情報学(GI) (ISSN:09196072)

巻号頁・発行日

vol.2004, no.28, pp.51-56, 2004-03-09

参考文献数

6

---

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.