An Optimizing Compiler for the pi-calculus
We developed an optimizing compilation technique which transforms
high-level pi-calculus specifications into rules
from which transitions of the global automata can be efficiently
generated without requiring user's annotation. Our compiler uses a compact
state representation and pre-computes the synchronizations in polynomial time
during compilation while generating transitions during verification.
We have also
developed an AC-matching based symmetry reduction technique to recognize
states that are equivalent due to symmetry, thereby
reducing state space traversed
during model checking. The compiler reduces both time
and memory requirements of MMC by up to an order of magnitude.