Temporal Logics and Model Checking for Fairly Correct Systems

We motivate and study a generic relaxation of correctness of reactive and concurrent systems with respect to a temporal specification. We define a system to be fairly correct if there exists a fairness assumption under which it satisfies its specification. Equivalently, a system is fairly correct if the set of runs satisfying the specification is large from a topological point of view, i.e., it is a co-meager set. We compare topological largeness with its more popular sibling, probabilistic largeness, where a specification is probabilistically large if the set of runs satisfying the specification has probability 1. We show that topological and probabilistic largeness of omega-regular specifications coincide for bounded Borel measures on finite-state systems. As a corollary, we show that, for specifications expressed in LTL or by Buchi automata, checking that a finite-state system is fairly correct has the same complexity as checking that it is correct. Finally we study variants of the logics CTL and CTL*, where the ´for all runs´ quantifier is replaced by a ´for a large set of runs´ quantifier. We show that the model checking complexity for these variants is the same as for the original logics