English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Global: Zendy Tools annual

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Insights

Presents the pdf analysis as premium feature

PDF Analysis

Presents the zaia usage as premium feature

ZAIA

Global: Zendy Tools monthly

Global: Zendy Plus monthly

Presents the access of premium content as premium feature

Premium Content

Global: Zendy Plus annual

Global: Zendy Free Plan

This study presents a framework that procedurally generates maze-like levels and leverages an automated verification technique called model checking to verify and produce a winning action sequence for that level. By leveraging the counterexample generation feature of the SPIN model checker, one or more solutions to the level-in-test are found, and the solutions are animated using a video game description language, PyVGDL. The framework contains four behavioral templates developed to model the logic of maze-like puzzle games in the modeling language of SPIN. These models automatically are tailored according to the level-in-test. To show the proposed methodology&#x2019;s effectiveness, we conducted five different experiments. These experiments include performance comparisons in level-solving between the proposed and existing methodologies &#x2014;A&#x002A; Search and Monte Carlo Tree Search&#x2014;and demonstrations of the use of the proposed approach to check a game level with respect to requirements. This study also proposes a pipeline to generate maze-like puzzle levels with two levels of cellular automata.

Verifying Maze-Like Game Levels With Model Checker SPIN