查看文章

In the field of concurrent distributed systems, model checking has been used to verify the correctness of these systems. However, due to state explosion, the exponential growth of a system’s state space, it is rather difficult and challenging to apply this method and acquire reliable results regarding a given system. Partial order reduction (POR) simplifies the problem by restricting the verification to a reduced state space while maintaining the soundness of properties of the system being tested.

Research scientists have been pursuing this issue during the last three decades, developing model checking exploration algorithms based on partial order reduction, in order to alleviate the problem as much as possible. These algorithms however, vary in their logic and implementation, which makes it difficult to decide, which algorithms are more efficient without thoroughly testing them. This procedure costs a lot of time and effort …