Analysis and Checking of Multi-Actor Liveness Rules from Fairness

Liveness properties are important in model checking. We put forward multi-actor liveness rules based on Lesilie Lamport´s TLA (temporal logic of actions) and liveness rules, then prove them, which involve existential or universal quantification under weak and strong fairness., At last we formalize the Internet banking system with TLA+ and check them with TLC. The results show these rules are appropriate.