View article

Model checking for transition systems specified in π-calculus has been a difficult problem due to the infinite-branching nature of input prefix, name-restriction and scope extrusion. We propose here an approach to model checking for π-calculus by encoding it into a logic which supports reasoning about bindings and fixed points. This logic, called FOλ ^Δ ∇, is a conservative extension of Church’s Simple Theory of Types with a “generic” quantifier. By encoding judgments about transitions in pi-calculus into this logic, various conditions on the scoping of names and restrictions on name instantiations are captured naturally by the quantification theory of the logic. Moreover, standard implementation techniques for (higher-order) logic programming are applicable for implementing proof search for this logic, as illustrated in a prototype implementation discussed in this paper. The use of logic …