State-Space Analysis and Complexity Assessment of Puzzle Games Using Colored Petri Nets
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...
Saved in:
| Main Authors: | , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
University of science and culture
2024-09-01
|
| Series: | International Journal of Web Research |
| Subjects: | |
| Online Access: | https://ijwr.usc.ac.ir/article_211538.html |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1846116272259989504 |
|---|---|
| author | Ahmad Taghinezhad-Nia Saeid Pashazadeh |
| author_facet | Ahmad Taghinezhad-Nia Saeid Pashazadeh |
| author_sort | Ahmad Taghinezhad-Nia |
| collection | DOAJ |
| description | 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. |
| format | Article |
| id | doaj-art-c7d2053a08634b9ca88387d4cd2882dc |
| institution | Kabale University |
| issn | 2645-4343 |
| language | English |
| publishDate | 2024-09-01 |
| publisher | University of science and culture |
| record_format | Article |
| series | International Journal of Web Research |
| spelling | doaj-art-c7d2053a08634b9ca88387d4cd2882dc2024-12-19T08:51:13ZengUniversity of science and cultureInternational Journal of Web Research2645-43432024-09-01741327https://doi.org/10.22133/ijwr.2024.482725.1241State-Space Analysis and Complexity Assessment of Puzzle Games Using Colored Petri NetsAhmad Taghinezhad-Nia0https://orcid.org/0000-0003-2353-9335Saeid Pashazadeh1https://orcid.org/0000-0002-8949-9180Faculty of Electrical and Computer Engineering, University of Tabriz, Tabriz, IranFaculty of Electrical and Computer Engineering, University of Tabriz, Tabriz, IranThe 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.https://ijwr.usc.ac.ir/article_211538.htmlstate-space analysismodel-checkingcolored petri netriddle game |
| spellingShingle | Ahmad Taghinezhad-Nia Saeid Pashazadeh State-Space Analysis and Complexity Assessment of Puzzle Games Using Colored Petri Nets International Journal of Web Research state-space analysis model-checking colored petri net riddle game |
| title | State-Space Analysis and Complexity Assessment of Puzzle Games Using Colored Petri Nets |
| title_full | State-Space Analysis and Complexity Assessment of Puzzle Games Using Colored Petri Nets |
| title_fullStr | State-Space Analysis and Complexity Assessment of Puzzle Games Using Colored Petri Nets |
| title_full_unstemmed | State-Space Analysis and Complexity Assessment of Puzzle Games Using Colored Petri Nets |
| title_short | State-Space Analysis and Complexity Assessment of Puzzle Games Using Colored Petri Nets |
| title_sort | state space analysis and complexity assessment of puzzle games using colored petri nets |
| topic | state-space analysis model-checking colored petri net riddle game |
| url | https://ijwr.usc.ac.ir/article_211538.html |
| work_keys_str_mv | AT ahmadtaghinezhadnia statespaceanalysisandcomplexityassessmentofpuzzlegamesusingcoloredpetrinets AT saeidpashazadeh statespaceanalysisandcomplexityassessmentofpuzzlegamesusingcoloredpetrinets |