Effect of Fairness in Model Checking of Self-stabilizing Programs

摘要

Existing approaches for verifying self-stabilization with symbolic model checker have relied on the use of weak fairness. We point out that this approach has limited scalability. To overcome this limitation, we show that if self-stabilization is possible without fairness then cost of verifying self-stabilization is substantially lower. The practical meaning of this observation is if the extra effort required to verify self-stabilization under weak fairness is not necessary then the state space reached by model checking of self-stabilizing programs could be substantially larger.