Constraint logic programming for local and symbolic model-checking

Abstract

We propose a model checking scheme for a semantically com- plete fragment of CTL by combining techniques from constraint logic programming, a restricted form of constructive negation and tabled resolution. Our approach is symbolic in that it encodes and manipulates sets of states using constraints; it supports local model checking using goal-directed computation enhanced by tabulation. The framework is parameterized by the constraint domain and supports any finite constraint domain closed under disjunction, projection and complementation. We show how to encode our fragment of CTL in constraint logic programming; we outline an abstract execution model for the resulting type of programs and provide a preliminary evaluation of the approach.