A Behavioral Analysis Approach for Efficient Partial Order Reduction

Partial order reduction is essential to address state explosion when verifying concurrent systems by reducing states irrelevant to the verification results. However, traditional static approaches by analyzing system model structures often do not work well. To address such problem, this paper presents a new behavioral analysis approach where a compositional reach ability analysis method is used to generate the over-approximate state spaces for all modules in a system, and then the independent transitions necessary for the partial order reduction are computed by examining these state spaces. Compared to the static analysis approaches, the independent transitions computed are more refined and accurate. The experimental results on some examples show that the presented approach is promising.