Geri Dön

Verifying maze-like game levels with model checker SPIN

Model kontrolcüsü SPIN ile labirent benzeri oyun seviyelerini doğrulamak

PDF İndir

  1. Tez No: 701516
  2. Yazar: ONUR TEKİK
  3. Danışmanlar: DOÇ. DR. AYSU BETİN CAN, DR. ÖĞR. ÜYESİ ELİF SÜRER
  4. Tez Türü: Yüksek Lisans
  5. Konular: Bilgisayar Mühendisliği Bilimleri-Bilgisayar ve Kontrol, Bilim ve Teknoloji, Computer Engineering and Computer Science and Control, Science and Technology
  6. Anahtar Kelimeler: Belirtilmemiş.
  7. Yıl: 2021
  8. Dil: İngilizce
  9. Üniversite: Orta Doğu Teknik Üniversitesi
  10. Enstitü: Enformatik Enstitüsü
  11. Ana Bilim Dalı: Bilişim Sistemleri Ana Bilim Dalı
  12. Bilim Dalı: Belirtilmemiş.
  13. Sayfa Sayısı: Belirtilmemiş.

Ö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

  1. Tez No

    386936

    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

    İngilizce

    2010

    Bilgisayar Mühendisliği Bilimleri-Bilgisayar ve Kontrolİstanbul Teknik Üniversitesi

    Bilgisayar Bilimleri Ana Bilim Dalı

    YRD. DOÇ. DR. FEZA BUZLUCA

    DR. OKAN TOPÇU

    YRD. DOÇ. DR. YUNUS EMRE SELÇUK

  2. Tez No

    309877

    Techniques for verifying transactional programs and linearizability

    İşlemsel programların ve doğrusallaştırılabilirliğin doğrulaması için teknikler

    ÖMER SUBAŞİ

    Yüksek Lisans

    İngilizce

    İngilizce

    2012

    Bilgisayar Mühendisliği Bilimleri-Bilgisayar ve KontrolKoç Üniversitesi

    Bilgisayar Bilimleri ve Mühendisliği Ana Bilim Dalı

    YRD. DOÇ. DR. SERDAR TAŞIRAN

  3. Tez No

    409137

    Developing and verifying a set of principles for the cyber security of the critical infrastructures of Turkey

    Türkiye'nin kritik alt yapılarının siber güvenliği için prensiplerin geliştirilmesi ve doğrulanması

    BİLGE KARABACAK

    Doktora

    İngilizce

    İngilizce

    2015

    Kamu YönetimiOrta Doğu Teknik Üniversitesi

    Bilişim Sistemleri Ana Bilim Dalı

    DOÇ. DR. SEVGİ ÖZKAN YILDIRIM

    PROF. DR. NAZİFE BAYKAL

  4. Tez No

    472600

    A tool for verifying noninterference property for HDL

    Donanım tasarlama dilinin birbirine karışmamışlık özelliğini doğrulayan araç

    DOĞUHAN GÜMÜŞOĞLU

    Yüksek Lisans

    İngilizce

    İngilizce

    2017

    Bilgisayar Mühendisliği Bilimleri-Bilgisayar ve KontrolYeditepe Üniversitesi

    Bilgisayar Mühendisliği Ana Bilim Dalı

    YRD. DOÇ. DR. ONUR DEMİR

  5. Tez No

    830324

    An artificial intelligence based algorithm for verifying clinical biochemistry tests

    Klinik biyokimya testlerini doğrulamak için yapay zeka tabanlı algoritma

    KADRİ CAN EROĞLU

    Yüksek Lisans

    İngilizce

    İngilizce

    2023

    Elektrik ve Elektronik MühendisliğiEskişehir Teknik Üniversitesi

    Elektrik-Elektronik Mühendisliği Ana Bilim Dalı

    DOÇ. DR. HAKAN GÜRAY ŞENEL

Geri Dön