Model Checking Liveness Properties under Fairness & Anti-fairness Assumptions

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