On Combining State Space Reductions With Global Fairness Assumptions
Model checking has established itself as an effective system analysis method, as it is capable of proving/disproving properties automatically. Its application to practical systems is however limited by state space explosion. Among effective state reduction techniques are symmetry reduction and partial order reduction. Global fairness often plays a vital role in designing self-stabilizing population protocols. It is known that combining fairness and symmetry reduction is nontrivial. In this paper, the authors first show that global fairness, unlike weak/strong fairness, can be combined with symmetry reduction.