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

Authors: 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}
  }