Temporal Logics and Model Checking for Fairly Correct Systems

I will present recent results on model checking for fairly correct systems (D. Varacca, H. Voelzer, LICS'06). A fair variant of a specfication is obtained by replacing "for all paths" by "for a large set of paths". For regular linear-time specifications, probabilistic and topological largness coincide. Hence, by results on probabilistic model checking, fair variants of LTL, omega-regular, and CTL* specifications are not harder to check than the originals. For CTL, the linear model checking algorithm can be adapted to the fair variant.