algorithm - Pi Calculus 是否有任何模型检查器或证明系统

Question

我对 Milner 的 Pi 微积分有点着迷，虽然我可以在白板上画出小图，但我很好奇是否有任何好的（或坏的）建模系统可以用来检查你的逻辑，以类似于 TLA+ 之类的方式。

如果这样的系统不存在或由于 没有必要reason x，我希望尽可能解释原因。