Description and Analysis of Fairness on Temporal Logic of Actions

TLA (temporal logic of actions) and itpsilas specifying language TLA+ have become an efficient and convenient approach for model checking, and fairness is a vital property in TLA. We try to analyze the definitions of fairness based on TLA, point out a fallible question on the definition of fairness in cited literature, improve it more clearly and prove the consistency of syntax and semantics of fairness, and subdivide the fairness in the end.