Solving Boolean Equation Systems using Small Progress Measures

We investigate a parity game interpretation of boolean equation systems. Given this interpretation, we present a version of the algorithm for solving parity games based on small progress measures [3]. The algorithm is applied directly on the boolean equation system (BES), eliminating the intermediate transformation step of BES to parity game. The resulting algorithm runs in O(ad(E)ΣX∈X |rhs(X) | ·…