基于依赖性的合成(完整版)
Dependency-based Compositional Synthesis (Full Version)
摘要:
尽管最近取得了许多进展,但反应合成仍然不是一种真正实用的技术。最大的挑战是从合成性能良好的小型过渡系统扩展到复杂的多组件设计。组合方法,例如为单个组件构建主导策略,显著降低了复杂性,但如果不广泛地重写规范,通常是不适用的。在本文中,我们提出了一种改进的合成,不需要这样的干预。我们的算法将系统分解为一系列组件,使得每个组件都有一个占主导地位的策略,即,性能至少与任何可能的替代品一样好,前提是前面的组件遵循它们的(已经合成的)策略。系统的分解是基于依赖分析,我们提供语义和语法技术。我们确定了该方法的合理性和完整性,并报告了令人鼓舞的实验结果。
英文摘要:
Despite many recent advances, reactive synthesis is still not really a practical technique. The grand challenge is to scale from small transition systems, where synthesis performs well, to complex multi-component designs. Compositional methods, such as the construction of dominant strategies for individual components, reduce the complexity significantly, but are usually not applicable without extensively rewriting the specification. In this paper, we present a refinement of compositional synthesis that does not require such an intervention. Our algorithm decomposes the system into a sequence of components, such that every component has a strategy that is dominant, i.e., performs at least as good as any possible alternative, provided that the preceding components follow their (already synthesized) strategies. The decomposition of the system is based on a dependency analysis, for which we provide semantic and syntactic techniques. We establish the soundness and completeness of the approach and report on encouraging experimental results.
机构、总结、中文摘要均由AI分析而来,可能存在错误,请以论文正文为准。