State-Space Analysis and Complexity Assessment of Puzzle Games Using Colored Petri Nets

Abstract

The verification of complex systems has traditionally relied on semi-automatic theorem-proving methods. However, model checking represents a paradigm shift by enabling automated, exhaustive verification of behavioral properties through systematic state exploration. Among advanced formal verification tools, Colored Petri Net (CPN) stands out for its integration of the ML programming language, facilitating robust model checking and system validation. Nevertheless, the application of CPN to complex systems is often constrained by the state-space explosion problem, which presents a significant challenge in contemporary research. While state-space analysis offers powerful capabilities for validation and scenario extraction, its potential remains largely untapped due to computational complexity constraints. This limitation is particularly pronounced in concurrent systems with multiple interacting variables, exemplified by game systems where intricate rule sets, deadlock conditions, and termination scenarios demand sophisticated modeling approaches. This paper presents a novel methodological framework for modeling and analyzing such game riddles, introducing methods to mitigate the state-space explosion problem. We demonstrate the efficacy of our approach through a comprehensive case study of the Merchant Ship puzzle game, though the methodology generalizes across various game typologies. By synthesizing model-checking techniques with ML-based algorithmic implementations, we develop an optimized search strategy for traversing the state space graph, enabling the derivation of quantitative complexity metrics. These metrics encompass critical indicators such as the success-to-total scenario ratio and the minimal trajectory length for both successful and unsuccessful game completions. Our research contributes to both the theoretical understanding of game complexity analysis and practical applications in game design through formal methods.

Keywords

• state-space analysis
• model-checking
• colored petri net
• riddle game