异步分布式系统有界综合的高效迹编码
Efficient Trace Encodings of Bounded Synthesis for Asynchronous Distributed Systems
摘要：
由于组件和环境的异步交互，分布式系统的手动实现是一项容易出错的任务。有界合成自动生成一个实现的规范的分布式系统，如果存在的话。到目前为止，分布式系统的有界合成并没有利用它们的异步特性。相反，组件的并发行为由所有交织编码，然后才根据规范进行检查。我们关闭这个差距，确定真正的并发合成的异步分布式系统表示为Petri网游戏。这定义了几个交织何时可以被一个真正的并发跟踪所包含。因此，更少和更短的验证问题，必须解决在每次迭代的有界综合算法。对于Petri网游戏，实验结果表明，我们的实现使用真正的并发性优于基于检查所有交织的实现。
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
