Verifying maze-like game levels with model checker SPIN
Model kontrolcüsü SPIN ile labirent benzeri oyun seviyelerini doğrulamak
- Tez No: 701516
- Danışmanlar: DOÇ. DR. AYSU BETİN CAN, DR. ÖĞR. ÜYESİ ELİF SÜRER
- Tez Türü: Yüksek Lisans
- Konular: Bilgisayar Mühendisliği Bilimleri-Bilgisayar ve Kontrol, Bilim ve Teknoloji, Computer Engineering and Computer Science and Control, Science and Technology
- Anahtar Kelimeler: Belirtilmemiş.
- Yıl: 2021
- Dil: İngilizce
- Üniversite: Orta Doğu Teknik Üniversitesi
- Enstitü: Enformatik Enstitüsü
- Ana Bilim Dalı: Bilişim Sistemleri Ana Bilim Dalı
- Bilim Dalı: Belirtilmemiş.
- Sayfa Sayısı: 98
Özet
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.
Özet (Çeviri)
In this thesis, we present a new methodology that includes procedural generation and verification of maze-like game levels. The methodology employs a model checker, called SPIN, in order to both produce a winning sequence of actions and to formally verify custom game design properties. In order to verify a game level, we propose automated tailoring on template game models, considering the level-in-test, specifically designed according to the game rules. By leveraging the counterexample generation feature of SPIN, we find one or more solutions to the level-in-test, and use PyVGDL to animate the solutions. In order to show this methodology's effectiveness, we conducted five different experiments. These experiments include performance comparisons in level solving between the proposed and existing methodologies, A-star search Monte Carlo tree search, and demonstrations of the proposed approach's usage to verify a game level with respect to existing requirements. The work also includes a pipeline for the generation of maze-like puzzle levels that includes two levels of cellular automata.
Benzer Tezler
- Verifying the interface compliance of federates using pre- and postconditions of RTI services
Çalışma zamanı altyapısı (RTI) servislerinin ön ve son koşullarını kullanarak federe arayüz uyumluluğunun geçerlenmesi
VİJDAN KIZILAY
Yüksek Lisans
İngilizce
2010
Bilgisayar Mühendisliği Bilimleri-Bilgisayar ve Kontrolİstanbul Teknik ÜniversitesiBilgisayar Bilimleri Ana Bilim Dalı
YRD. DOÇ. DR. FEZA BUZLUCA
DR. OKAN TOPÇU
YRD. DOÇ. DR. YUNUS EMRE SELÇUK
- Raylı ulaşım sistemlerinde anklaşman tablolarının doğruluğunun model kontrolü yöntemiyle test edilmesi
Verifying the accuracy of interlocking tables for signalling systems using model checking method
BASRİ TUĞCAN ÇELEBİ
Yüksek Lisans
Türkçe
2016
Bilgisayar Mühendisliği Bilimleri-Bilgisayar ve KontrolYıldız Teknik ÜniversitesiKontrol ve Otomasyon Mühendisliği Ana Bilim Dalı
YRD. DOÇ. DR. ÖZGÜR TURAY KAYMAKÇI
- Tıbbi karar destek sisteminin veri madenciliği yöntemleriyle gerçekleştirilmesi
Verifying medical decision support system with the methods of data mining
TUBA PALA
Yüksek Lisans
Türkçe
2013
Bilgisayar Mühendisliği Bilimleri-Bilgisayar ve KontrolMarmara ÜniversitesiElektronik-Bilgisayar Eğitimi Ana Bilim Dalı
PROF. DR. A. YILMAZ ÇAMURCU
- Binek araç gündüz farının sonlu elemanlar modelinin bilgisayarda şok testleri için güncellenmesi ve doğrulanması
Updating and verifying the finite element model of a passenger vehicle daytime running light for computer shock tests
BARIŞ EDİZ
Yüksek Lisans
Türkçe
2018
Makine MühendisliğiUludağ ÜniversitesiMakine Mühendisliği Ana Bilim Dalı
YRD. DOÇ. DR. SEVDA TELLİ ÇETİN
- Riemann dönüşüm teoremine genel bir bakış
An overview of the Riemann mapping theorem
MELEK ÇAĞMAN
Yüksek Lisans
Türkçe
2019
MatematikAtatürk ÜniversitesiMatematik Ana Bilim Dalı
PROF. DR. EKREM KADIOĞLU