No matter from the theoretical or practical perspective, solving parity game plays a very important role. On one side, this problem possesses some amazing properties of computational complexity, and people are still searching for a polynomial time algorithm. On the other side, solving it and modal mu-calculus are almost the same in nature, so any efficient algorithm concerning this topic can be applied to model checking problem of modal mu-calculus. Considering the importance of modal mu-calculus in the automatic verification field, a series of model checkers will benefit from it. The main purpose of our study is to use constraints satisfaction problem (CSP), a deeply-studied and widely-accepted method, to settle parity game. The significance lies in that we can design efficient model checker through introducing various CSP algorithms, hence open a door to explore this problem of practical importance from a different viewpoint. In the paper, we propose a CSP-based algorithm and the related experimental results are presented.
展开▼
