MODALITIES FOR MODEL CHECKING - BRANCHING TIME LOGIC STRIKES BACK

We consider automatic verification of finite state concurrent programs. The global state graph of such a program can be viewed as a finite (Kripke) structure, and a model checking algorithm can be given for determining if a given structure is a model of a specification expressed in a propositional temporal logic. In this paper, we present a unified approach for efficient model checking under a broad class of generalized fairness constraints in a branching time framework extending that of E. M. Clarke et al. We also consider an application of our work to the theory of finite automata on infinite strings.