Softlock Detection for Super Metroid with Computation Tree Logic

Videogame level designs can contain errors called softlocks where a player traversing the level in an unintended manner can become permanently stuck. In this paper, we explore the automated detection of softlocks in the game Super Metroid using Computation Tree Logic (CTL). Super Metroid distinguishes itself as an example domain because of its velocity-based movement and rich item upgrade hierarchy. These factors can cause softlocks in Super Metroid to be challenging to detect visually. We contribute a tile-based gameplay abstraction for Super Metroid, and demonstrate verification of CTL properties for scenarios based on a segment of the original game’s level design. CTL can be used to define and test many other gameplay properties (e.g. which bosses can be skipped or which order items may be collected) and is immediately applicable to other game designs for which a compact abstraction of their state space can be enumerated. By making plausible design changes to a Super Metroid level fragment, we show how highly nonobvious softlocks can be detected and how the counterexamples resulting from verification failure can be turned into visualizations that explain the problem.