A Provably Correct Compiler for Efficient Model Checking of Mobile Processes

Abstract:

We present an optimizing compiler for the pi-calculus that significantly improves the time and space performance of the MMC model checker. MMC exploits the similarity between the manner in which resolution techniques handle variables in a logic program and the manner in which the operational semantics of the pi-calculus handles names by representing pi-calculus names in MMC as Prolog variables, with distinct names represented by distinct variables. Given a pi-calculus process P, our compiler for MMC produces an extremely compact representation of P's symbolic state space as a set of transition rules. It also uses AC unification to recognize states that are equivalent due to symmetry.

Bibtex Entry:

@inproceedings{YRS:PADL05,
author = {Ping Yang and  Yifei Dong and C. R. Ramakrishnan and  Scott A. Smolka},
title = {A Provably Correct Compiler for Efficient Model Checking of
  Mobile Processes},
booktitle = {Practical Aspects of Declarative Languages ({PADL})},
address = {Los Angeles, California},
month = {Jan},
series = {Lecture Notes in Computer Science},
volume = {3350},
pages = {113--127},
publisher = {Springer},
year = {2005}
}

Full Paper:

[pdf]

C. R. Ramakrishnan
(cram@cs.sunysb.edu)