1］ GIANNAKOPOULOU D, MAGEE J, KRAMER J. Checking progress with action priority: is it fair ［J］.ACM SIGSOFT Software Engineering Notes, 1999, 24(6): 511-527．
［2］ SUN Jun, LIU Yang, ROYCHOUDHURY A, et al. Fair model checking with process counter abstraction ［C］∥ Proceedings of Formal Methods. Eindhoven: Springer, 2009: 123-139．
［3］ FISCHER M J, JIANG H. Self-stabilizing leader election in networks of finite-state anonymous agents ［C］∥ Proceedings of the 10th International Conference on Principles of Distributed Systems. Bordeaux: Springer, 2006: 395-409．
［4］ ANGLUIN D, ASPNES J, FISCHER M J, et al. Self-stabilizing population protocols ［C］∥ Proceedings of the 9th International Conference on Principles of Distributed Systems. Pisa: LNCS, 2005, 3974: 103-117．
［5］ LAMPORT L. Proving the correctness of multiprocess programs ［J］. IEEE Transactions on Software Engineering, 1977, 3(2): 125-143．
［6］ HOLZMANN G J. The SPIN model checker: primer and reference manual ［M］. Boston: Wesley, 2003．
［7］ LAMPORT L. Fairness and hyperfairness ［J］. Distributed Computing, 2000, 13(4): 239-245．
［8］ GELDENHUYS J, VALMARI A. More efficient on-the-fly LTL verification with Tarjans algorithm ［J］. Theoritical Computer Science, 2005, 345(1): 60-82．
［9］ HENZINGER M R, TELLE J A. Faster algorithms for the nonemptiness of streett automata and for communication protocol pruning ［C］∥ Proceedings of the 5th Scandinavian Workshop on Algorithm Theory. Gothenburg: Springer, 1996: 16-27．
［10］ KESTEN Y, PNUELI A, RAVIV L, et al. Model checking with strong fairness ［J］. Formal Methods and System Design, 2006, 28(1): 57-84．
［11］ TARJAN R. Depth-first search and linear graph algorithms ［J］. SIAM Journal on Computing, 1972, 2(1): 146-160．
［12］ CANEPA D, POTOP-BUTUCARU M. Stabilizing token schemes for population protocols ［J］. Computing Research Repository, 2008, 806(3471): 765-784．
［13］ JIANG H. Distributed systems of simple interacting agents ［D］. New Haven: Yale University, 2007．
［14］ SUN Jun, LIU Yang, DONG Jin-song, et al. PAT: towards flexible verification under fairness ［C］∥ Proceedings of the 21st International Conference on Computer Aided Verification. Grenoble: Springer, 2009: 709-714．
［15］ LAMPORT L. Proving the correctness of multiprocess programs ［J］. IEEE Transactions on Software Engineering, 1977, 3(2): 125-143．
［16］ APT K R, FRANCEZ N, KATZ S. Appraising fairness in languages for distributed programming ［J］. Distributed Computing, 1988, 2(4): 226-241．
［17］ COURCOUBETIS C, VARDI M Y, WOLPER P, et al. Memory-efficient algorithms for the verification of temporal properties ［J］. Formal Methods in System Design, 1992, 1(2/3): 275-288．
［18］ HARDIN R H, KURSHAN R P, SHUKLA S K, et al. A new heuristic for bad cycle detection using BDDs ［J］. Formal Methods in System Design, 2001, 18(2): 131-140.