Formal Verification of Multi-Thread Minimax Behavior Using mCRL2 in the Connect 4

Diego Escobar () and Jesus Insuasti
Additional contact information
Diego Escobar: Systems Engineering Department, University of Nariño, Pasto 520001, Colombia
Jesus Insuasti: Systems Engineering Department, University of Nariño, Pasto 520001, Colombia

Mathematics, 2024, vol. 13, issue 1, 1-16

Abstract: This study focuses on the formal verification of a parallel version of the minimax algorithm using the mCRL2 modeling language, applied to the game of Connect 4. The research aims to ensure that the algorithm behaves correctly in concurrent execution environments by providing a formal model and conducting rigorous verification. The parallel version of minimax distributes computations across multiple threads, with each thread evaluating different successor states concurrently. Using mCRL2, we specify the algorithm’s behavior, generate Labeled Transition Systems (LTSs), and verify critical properties such as the absence of deadlocks, liveness, and correctness of state transitions. The formal verification process demonstrates that the proposed model accurately represents the parallel minimax algorithm and ensures its reliability by verifying properties that guarantee unique and non-redundant actions throughout the execution. The findings highlight the value of formal methods in validating the correctness of parallel artificial intelligence algorithms, laying the foundation for future optimizations that focus on performance.

Keywords: minimax; multithreaded; algorithm; formal; verification; mCRL2 (search for similar items in EconPapers)
JEL-codes: C (search for similar items in EconPapers)
Date: 2024
References: View complete reference list from CitEc
Citations:

Downloads: (external link)
https://www.mdpi.com/2227-7390/13/1/96/pdf (application/pdf)
https://www.mdpi.com/2227-7390/13/1/96/ (text/html)

Related works:
This item may be available elsewhere in EconPapers: Search for items with the same title.

Export reference: BibTeX RIS (EndNote, ProCite, RefMan) HTML/Text

Persistent link: https://EconPapers.repec.org/RePEc:gam:jmathe:v:13:y:2024:i:1:p:96-:d:1555881

Access Statistics for this article

Mathematics is currently edited by Ms. Emma He

More articles in Mathematics from MDPI
Bibliographic data for series maintained by MDPI Indexing Manager ().