تحليل خودكار بازي رايانه‌اي با استفاده از شبكه پتري رنگي

Automatic Analysis of Computer Game Using Colored Petri Net (Text in Persian)

وجود اشكال در طراحي از عوامل ايجاد نقص در سيستم است. تشخيص و رفع ايرادها در مرحله طراحي مانع از افزايش هزينه و زمان توليد سيستم مي‌گردد. براي اثبات ويژگي‌هاي رفتاري سامانه‌ها از روش‌هاي رسمي استفاده مي‌شود. براي اطمينان از عدم وجود بن‌بست، تضمين وجود جواب و تعيين ميزان پيچيدگي معما، از روش‌هاي رسمي در طراحي معماي بازي‌هاي رايانه‌اي مي‌توان استفاده كرد. شبكه پتري رنگي سلسله مراتبي يك روش رسمي مدل‌سازي است كه مي‌تواند براي ارزيابي معماهاي بازي‌هاي رايانه‌اي مانند جورچين‌هاي طراحي مسير استفاده شود. بازي Unblock Me به‌عنوان يك مثال موردي در اين مقاله مدل‌سازي شده و تحليل خودكار دو معماي آن موردبررسي قرار گرفته است. مدل‌سازي بازي به‌صورت سلسله مراتبي انجام شده است. در اين مقاله راه‌كارهاي جديدي براي حل مشكل انفجار حالت و كاهش زمان اجراي مدل ارائه گرديده است. مدل‌سازي باهدف امكان تحليل خودكار فضاي حالت سيستم انجام شده و توابع موردنياز جهت اثبات ويژگي‌هاي رفتاري پياده‌سازي شده است. اين مقاله روشي براي مدل‌سازي و اثبات ويژگي‌هاي رفتاري بازي‌هاي رايانه‌اي از نوع جورچين را با استفاده از شبكه پتري رنگي سلسله مراتبي ارائه كرده و قابل‌تعميم به بازي‌هاي مشابه است.

Existence of design faults is a source of failure in the system. Detection and removal of faults in design phase prohibits increase of cost and time of system development. Formal methods are used for proving behavioral properties of systems. Formal methods can be used in crux design of computer games to ensure absence of deadlock، guarantee of answer's existence and to determine complexity of crux. Hierarchical colored Petri net is a formal method that can be used to evaluate cruxes of computer games such as path planning puzzle games. Unblock me game is modeled as a case study and automatic analysis of its two cruxes are studied in this paper. Modeling of game is done hierarchically. New approaches for eliminating state space explosion problem and decreasing running time of model is presented in this paper. Modeling is done with aim of automatic state space analysis of the system and required functions for proving behavioral properties are implemented. This paper is presented a method for modeling and proving behavioral properties of puzzle type computer games using hierarchical colored Petri net that and can be generalized to similar games.