论文标题
基于依赖关系的构图合成(完整版)
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.