Reasoning about systems with transition fairness

Abstract. Formal verification methods model systems by Kripke structures. In order to model live behaviors of systems, Kripke structures are augmented with fairness condi-tions. Such conditions partition the computations of the systems into fair computations, with respect to which verification proceeds, and unfair computations, which are ignored. Reasoning about Kripke structures augmented with fairness is typically harder than rea-soning about non-fair Kripke structures. We consider the transition fairness condition, where a computation pi is fair iff each transition that is enabled in pi infinitely often is also taken in pi infinitely often. Transition fairness is a natural and useful fairness condi-tion. We show that reasoning about Kripke structures augmented with transition fairness is not harder than reasoning about non-fair Kripke structures. We demonstrate it for fair CTL and LTL model checking, and the problem of calculating the dominators and post-dominators.