Model Checking and XSB
C.R. Ramakrishnan
Abstract:
This tutorial describes how a tabled logic programming system, such as
XSB, can be used to
derive efficient model checkers from relatively high-level
specifications. We present the specification (in XSB) of the
operational semantics of a family of process specification languages,
Milner's basic CCS; value-passing CCS; and synchronous CCS, and an
expressive temporal logic, model mu-calculus. We then discuss how
efficient model checkers can be constructed by applying
meaning-preserving transformations to the above specifications. We
also describe some preliminary experiences with applying logic
programming-based approaches to address problems in areas of active
research in model checking, such as verification of parameterized,
infinite-state, and real time systems and combination of deduction and
model checking.
The tutorial describes work done in the
LMC project at Stony Brook.
The tutorial notes are available in two parts