Description and Analysis of Fairness on Temporal Logic of Actions

TLA(Temporal Logic of Actions) and it’s 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 [5], improve it more clearly and prove the consistency of syntax and semantics of fairness, and subdivide the fairness in the end.