Download MMC

MMC is a model checker implemented using the XSB tabled logic programming system. MMC is an explicit-state, local model checker for pi-calculus, and the alternation-free fragment of the modal mu-calculus. So far, MMC has only text (non-graphic) mode.

MMC is now available in the following format:

See README for terms of use.

MMC with compilation, with AC and with AC nets are available in comp.tar.gz

System Requirements for MMC:

XSB logic programming system v2.1 or higher running in Linux. For acquiring and installing XSB, please consult the official XSB home page.

If you have any problems downloading, installing, or running MMC, please send mail to with a short description of the problem and the platform (OS, XSB version) you are operating on.


A Logical Encoding of the Pi-Calculus: Model Checking Mobile Processes Using Tabled Resolution.