Verifying maze-like game levels with model checker SPIN

Bu tezde, labirent benzeri oyun seviyelerinin yöntemsel üretimi ve doğrulamasını içeren yeni bir metodoloji sunmaktayız. Bu metodoloji hem kazanan eylemler dizisini üretmek hem de özel oyun tasarım özellikleri doğrulamak için kullanılan SPIN isimli bir model kontrolcüsünü içermektedir. Bir oyun seviyesini doğrulamak için oyun kurallarına göre özel tasarlanmış oyun modeli şablonlarının teste tabii olan seviyeye göre otomatik düzenlenmesini öneriyoruz. SPIN'in karşı örnek üretme özelliğini kullanarak, teste tabii olan seviyeye bir ya da daha fazla çözüm bulup, PyVGDL'i kullanarak bu çözümleri canlandırmaktayız. Bu metodolojinin etkenliğini göstermek için beş farklı deney düzenlenmiştir. Bu deneyler önerilen metodolojinin var olan metodolojilerle- A-Star Search ve Monte Carlo Tree Search- performans kıyaslarını ve önerilen metodolojinin oyun seviyelerinin var olan gereksinimlere göre doğrulanmasında kullanımını gösterimini içermektedir. Tezde ayrıca labirent benzeri bulmaca seviyelerinin üretimi için kullanılabilecek iki seviye hücresel otomat içeren bir hat bulunmaktadır.