Breaking symmetries †
Breaking symmetries †
复制标题
打破对称性 †
DOI：
--
复制
发表时间：
2010
影响因子：
0.5
通讯作者：
U. Nestmann
中科院分区：
文献类型：
--
作者：
Kirstin Peters;U. Nestmann
Palamidessi 的一个著名结果告诉我们，πmix（具有混合选择的 π 演算）比 πsep（其仅具有单独选择的子集）更具表现力。这一结果的证明分析了它们在对称网络中关于领导人选举的不同表达能力。后来，Gorla 提供了一个可以说更简单的证明，即在并行运行两个副本时，采用“乱伦”过程的可简化性（包括启用同一通道的发送者和接收者的混合选择），而不是对称网络中的领导者选举。在这两个证明中，破缺（初始）对称性的作用或多或少是显而易见的。在本文中，我们通过重新证明上述结果（基于打破对称性意味着什么的适当形式化）来更多地阐明这一角色，而没有提及领导者选举等另一个问题领域。 Palamidessi 和 Gorla 都重新表述了他们的结果，指出从 πmix 到 πsep 没有统一且合理的编码。我们指出了如何调整他们的证明，并展示不同的一致性和合理性概念的后果。在每种情况下，打破初始对称性的能力都是至关重要的。此外，通过放弃均匀性标准，我们表明确实存在合理的编码。我们强调其基本原则，强调局部对称性破缺与全局对称性破缺之间的区别。
A well-known result by Palamidessi tells us that πmix (the π-calculus with mixed choice) is more expressive than πsep (its subset with only separate choice). The proof of this result analyses their different expressive power concerning leader election in symmetric networks. Later on, Gorla offered an arguably simpler proof that, instead of leader election in symmetric networks, employed the reducibility of ‘incestual’ processes (mixed choices that include both enabled senders and receivers for the same channel) when running two copies in parallel. In both proofs, the role of breaking (initial) symmetries is more or less apparent. In this paper, we shed more light on this role by re-proving the above result – based on a proper formalization of what it means to break symmetries – without referring to another problem domain like leader election. Both Palamidessi and Gorla rephrased their results by stating that there is no uniform and reasonable encoding from πmix into πsep. We indicate how their proofs can be adapted and exhibit the consequences of varying notions of uniformity and reasonableness. In each case, the ability to break initial symmetries turns out to be essential. Moreover, by abandoning the uniformity criterion, we show that there indeed is a reasonable encoding. We emphasize its underlying principle, which highlights the difference between breaking symmetries locally instead of globally.