异步分布式自动机：模态$\mu$-演算片段的刻画

我们确立了在有限有向图上，一类异步分布式自动机与最小不动点逻辑的一个小片段之间的等价性。具体而言，我们考虑的逻辑是模态 $\mu$-演算的一个片段（或其变体），该片段允许最小不动点但禁止最大不动点。相应的自动机模型使用由相同有限状态机组成的网络，这些机器以异步方式通信，且其状态图除自环外必须是无环的。利用与逻辑的联系，我们还证明了这些机器的表达能力不依赖于消息是否会丢失。