Analysis of N-Queens Stochastic Algorithms Using Probabilistic Model Checking

Probabilistic model checking extends model checking to domains in which actions will be taken based on a certain probability. This aligns nicely with modeling many real-world systems in which actions are taken in a stochastic manner. Unfortunately, probabilistic model checking further complicates the already high computational complexity challenges associated deterministic model checking. N-Queens is a commonly studied computer science and mathematics problem. There are many algorithms that solve this problem under different constraints. Some algorithms are iterative and deterministic, while other algorithms are stochastic in nature. In this paper, we present a probabilistic model checking approach to check a fundamental property of these algorithms; namely, their ability to find a solution within a given number of transitions (iterations). This number is not fixed, but rather a probability of successful completion within some number of transitions. We utilize PRISM, a probabilistic model checker, to model these algorithms and find the probability that this property is satisfied after I interactions. We present and discuss some relevant challenges associated with probabilistic model checking and make some suggestions for future research.

The PRISM models are available on GitHub here under an MIT License