A temporal logic to deal with fairness in transition systems

In this paper, we propose a notion of fairness for transition systems and a logic for proving properties under the fairness assumption corresponding to this notion. We consider that the concept of fairness which is useful is "fair reachability" of a given set of states P in a system, i.e. reachability of states of P when considering only the computations such that if, during their execution, reaching states of P is possible infinitely often, then states of P are visited infinitely often. This definition of fairness suggests the introduction of a branching time logic FCL, the temporal operators of which express, for a given set of states P, the modalities "it is possible that P" and "it is inevitable that P" by considering fair reachability of P. The main result is that, given a transition system S and a formula f of FCL expressing some property of S under the assumption of fairness, there exists a formula f′ belonging to a branching time logic CL such that : f is valid for S in FCL iff f′ is valid for S in CL. This result shows that proving a property under the assumption of fairness is equivalent to proving some other property without this assumption and that the study of FCL can be made via the "unfair" logic CL, easier to study and for which several results already exist.