传统的对付传值进程的途径是将其转换为单纯同步的基本进程，这种转化的核心步骤是把输入变量实例化为所有可能的值，因而会带来无穷性或状态爆炸的问题。本项目探讨传值进程的语义模型和模态逻辑，设计传值进程的验证算法，研制直接适用于传值进程的证明工具。研究的成果将成为进程代数理论走向实际应用的桥梁。