Liveness Property Safety Rules of Multi-Action Based on TLA+

In this paper, we put forward the definitions of safety transition system and the theorem which proof that every state in safety transition system is safe; Then we put forward safety multi-actor Liveness property rules under weak and strong fairness and prove them, the example of multi-user´s mutually exclusive action of drawing out in Internet bank based TLA+ to check the rules.