今後の課題

本研究の今後の課題としては，次のような事が考えられる．

• 補償プロトコルの検証(Delay< Wait仮定の消去)

– 本研究では，バケット同期法のみに焦点を絞って検証を行った．つまり，一般 にバケット同期法は，Delay <Wait仮定があるならば，因果順序性を保証する ことが検証された．このような方法によって，Delay<Waitであることをある 補償プロトコルが保証するならば，その補償プロトコルとバケット同期法を合 わせたプロトコルも因果順序性を保証することが確認された．しかし，本研究 では補償プロトコルを用いればDelay < Waitが保証されることを検証してい ない．そのため，何らかの具体的な補償プロトコルがDelay < Waitを保証す ることを検証しなければならない．

• セッションへ参加するプレイヤー数の増加・減少への対応

– 本研究では，セッションに参加しているプレイヤー数は，開始時から増加も減 少もしないという仮定でバケット同期法を検証している．このような仮定を満 たすネットワークゲームは実際に多く存在しているため，決して無理な仮定で はない．しかし，プレイヤー数の増減があるゲームもやはり存在しており，増 減がありうるという一般的な仮定の下で検証を行う事が望ましい．

謝辞

本研究を進めるにあたり，ご指導賜りました二木厚吉教授に厚くお礼を申し上げます．

また，有益な助言を頂いた同大学院 青木利晃准教授，緒方和博准教授，千葉勇輝助教に 感謝の意を示します．また，本研究を進めるために，相談にのって頂いた，二木研究室  有本泰仁さん，大井聡史さん，TRINH, BAO NGOC QUOCさん，青木研究室 谷崎裕 明さん，波多野秀行さん，陳江さんに感謝いたします．最後に，研究に関する議論にも応 じてくださった，二木研究室，青木研究室，緒方研究室の皆さんにも感謝いたします．

参考文献

[BK99] T. Bova and T. Krivoruchka. Reliable udp protocol. Network Working Group INTERNET-DRAFT, Feburary 1999.

[BLL07] N. E. Baughman, M. Liberatore, and B. N. Levine. Cheat-proof playout for centralized and peer-to-peer gaming. IEEE/ACM Trans. Netw., Vol. 15, No. 1, pp. 1–13, 2007.

[CKFJ04] E. Cronin, A. R. Kurc, B. Filstrup, and S. Jamin. An efficient synchronization mechanism for mirrored game architectures. Multimedia Tools and Applica-tions, Vol. 23, No. 1, pp. 7–30, 2004.

[FR05] S. Ferretti and M. Roccetti. Fast delivery of game events with an optimistic synchronization mechanism in massive multiplayer online games. In Proc. of Advances in computer entertainment technology, pp. 405–412. ACM, 2005.

[Fut06] K. Futatsugi. Verifying specifications with proof scores in CafeOBJ. In Proc.

of Advances in computer entertainment technology, pp. 3–10, 2006.

[GD98] L. Gautier and C. Diot. Design and evaluation of MiMaze, a multi-player game on the internet. In Proc. of IEEE Multimedia Systems Conference, pp.

233–236, 1998.

[MC05] David R. Michael and Sandra L. Chen. Serious Games: Games That Educate, Train, and Inform. Muska & Lipman/Premier-Trade, 2005.

[NNS03] E. Najm, U. Nestmann, and P. Stevens, editors. Formal methods for open object-based distributed systems, Vol. 2884 ofLNCS. Springer, 2003.

[OF03] K. Ogata and K. Futatsugi. Proof scores in the OTS/CafeOBJ method. In Proc. of Formal Methods for Open Object-Based Distributed Systems, pp. 170–

184, 2003.

[PW02] Lothar Pantel and Lars C. Wolf. On the impact of delay on real-time multi-player games. In Proceedings of the 12th international workshop on Network and operating systems support for digital audio and video, NOSSDAV ’02, pp.

23–29, New York, NY, USA, 2002. ACM.

付録 A バケット同期法モデルの記述

A.1 PNAT.mod

-- PNAT Model

mod! PNAT principal-sort Nat {

[ Zero NzNat < Nat ] op 0 : -> Zero {constr} .

op s _ : Nat -> NzNat {constr} . pred _ = _ : Nat Nat { comm } . pred _ < _ : Nat Nat .

op _ + _ : Nat Nat -> Nat { assoc comm } . op sd : Nat Nat -> Nat { comm } .

vars N M : Nat . var NN : NzNat . -- + definitions

eq s(N) + M = s(N + M) . -- 0 is left idempotency of + eq 0 + N = N .

-- 0 is right idempotency of + eq N + 0 = N .

-- = definitions eq (NN = 0) = false . eq (N = N) = true . eq (s(N) = N) = false . eq (s(N) = s(M)) = (N = M) .

-- < definitions eq N < N = false . eq 0 < s(N) = true . eq s(N) < 0 = false . eq s(N) < s(M) = N < M . }