Abstract
Model checking liveness properties needs antifairnessas well as fairness assumptions. As a formula expressing fairness assumptions becomes too long to make livenessmodel checking feasible, so does one expressing anti-fairness ones. ABP is used as an example to demonstrate that a divide amp; conquer approach can make liveness model checking under those assumptions feasible.