## Paper: Temporal logics and model checking for fairly correct systems (at LICS 2006)

**Daniele Varacca Hagen Völzer**

### Abstract

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 w-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.

### BibTeX

@InProceedings{Vlzer-Temporallogicsandmo, author = {Daniele Varacca and Hagen Völzer}, title = {Temporal logics and model checking for fairly correct systems}, booktitle = {Proceedings of the Twenty-First Annual IEEE Symposium on Logic in Computer Science (LICS 2006)}, year = {2006}, month = {August}, pages = {389--398}, location = {Seattle, Washington, USA}, publisher = {IEEE Computer Society Press} }