Formal Verification of Multi-Thread Minimax Behavior Using mCRL2 in the Connect 4
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 cond...
Saved in:
| Main Authors: | , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
MDPI AG
2024-12-01
|
| Series: | Mathematics |
| Subjects: | |
| Online Access: | https://www.mdpi.com/2227-7390/13/1/96 |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1841549140630175744 |
|---|---|
| author | Diego Escobar Jesus Insuasti |
| author_facet | Diego Escobar Jesus Insuasti |
| author_sort | Diego Escobar |
| collection | DOAJ |
| description | 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. |
| format | Article |
| id | doaj-art-5ad8a8f959d2472f85b57a0f79ac4395 |
| institution | Kabale University |
| issn | 2227-7390 |
| language | English |
| publishDate | 2024-12-01 |
| publisher | MDPI AG |
| record_format | Article |
| series | Mathematics |
| spelling | doaj-art-5ad8a8f959d2472f85b57a0f79ac43952025-01-10T13:18:14ZengMDPI AGMathematics2227-73902024-12-011319610.3390/math13010096Formal Verification of Multi-Thread Minimax Behavior Using mCRL2 in the Connect 4Diego Escobar0Jesus Insuasti1Systems Engineering Department, University of Nariño, Pasto 520001, ColombiaSystems Engineering Department, University of Nariño, Pasto 520001, ColombiaThis 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.https://www.mdpi.com/2227-7390/13/1/96minimaxmultithreadedalgorithmformalverificationmCRL2 |
| spellingShingle | Diego Escobar Jesus Insuasti Formal Verification of Multi-Thread Minimax Behavior Using mCRL2 in the Connect 4 Mathematics minimax multithreaded algorithm formal verification mCRL2 |
| title | Formal Verification of Multi-Thread Minimax Behavior Using mCRL2 in the Connect 4 |
| title_full | Formal Verification of Multi-Thread Minimax Behavior Using mCRL2 in the Connect 4 |
| title_fullStr | Formal Verification of Multi-Thread Minimax Behavior Using mCRL2 in the Connect 4 |
| title_full_unstemmed | Formal Verification of Multi-Thread Minimax Behavior Using mCRL2 in the Connect 4 |
| title_short | Formal Verification of Multi-Thread Minimax Behavior Using mCRL2 in the Connect 4 |
| title_sort | formal verification of multi thread minimax behavior using mcrl2 in the connect 4 |
| topic | minimax multithreaded algorithm formal verification mCRL2 |
| url | https://www.mdpi.com/2227-7390/13/1/96 |
| work_keys_str_mv | AT diegoescobar formalverificationofmultithreadminimaxbehaviorusingmcrl2intheconnect4 AT jesusinsuasti formalverificationofmultithreadminimaxbehaviorusingmcrl2intheconnect4 |