HORNSAT, model checking, verification and games

Abstract

We develop a HORNSAT-based methodology for verification of finite state systems. This general methodology leads naturally to algorithms, that are local [25, 19], on the fly [28, 11, 13, 5] and incremental [24]. It also leads naturally to diagnostic behavioral relation checking [7] algorithms. Here we use it to develop model checking algorithms for various fragments of modal mu-calculus. We also use our methodology to develop a uniform game theoretic formulations of all the relations in the linear time/branching time hierarchy of [27]. As a corollary, we obtain natural sufficient conditions on a behavioral relation p, for p to be polynomial time decidable for finite state transition systems.