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 Tarjans 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. |