论文标题
异步分布式系统的有限合成的有效痕量编码
Efficient Trace Encodings of Bounded Synthesis for Asynchronous Distributed Systems
论文作者
论文摘要
由于组件和环境的异步相互作用，分布式系统的手动实现是一项容易出错的任务。有限的合成会自动生成一个实现，如果存在一个分布式系统的规范。到目前为止，分布式系统的有限合成并未利用其异步性。取而代之的是，组件的并发行为均由所有交织来编码，然后根据规范进行检查。我们通过在合成彼得里游戏的异步分布式系统中确定真正的并发来缩小这一差距。这定义了何时可以通过一个真正的并发跟踪来累积几个交织。因此，在有限合成算法的每次迭代中必须解决较少和较短的验证问题。对于Petri Games，实验结果表明，我们使用真正的并发的实施方法优于检查所有交织的实现。
The manual implementation of distributed systems is an error-prone task because of the asynchronous interplay of components and the environment. Bounded synthesis automatically generates an implementation for the specification of the distributed system if one exists. So far, bounded synthesis for distributed systems does not utilize their asynchronous nature. Instead, concurrent behavior of components is encoded by all interleavings and only then checked against the specification. We close this gap by identifying true concurrency in synthesis of asynchronous distributed systems represented as Petri games. This defines when several interleavings can be subsumed by one true concurrent trace. Thereby, fewer and shorter verification problems have to be solved in each iteration of the bounded synthesis algorithm. For Petri games, experimental results show that our implementation using true concurrency outperforms the implementation based on checking all interleavings.
