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