π-演算中的分层通信拓扑

本文关注 π-项通信拓扑所满足的形状不变量，以及这些不变量的自动推断。若存在有限森林 T 使得从 P 可达的每一项的通信拓扑均满足 T 形不变量，则 π-项 P 是分层的。我们设计了一种静态分析，借助一种具有可判定推断能力的新型类型系统来证明某项的分层性。该类型系统的可靠性证明采用了一种非标准的 π-演算反应视角。分层项的覆盖问题是可判定的。这可以通过证明每个分层项都是深度有界的来证明，而后者是文献中已知不可判定的性质。因此我们获得了一个具有可判定安全验证问题的、富有表达力的 π-演算静态片段。