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 spec

• Type: Conference
• Year: 2006
• Where: LICS
• Authors: Daniele Varacca, Hagen Völzer
• Keywords: Computer Science, Concurrent Systems, Fairness Assumption, Generic Relaxation, LICS 2006