Reactive synthesis is the task of automatically deriving an implementation from a specification. It is a promising technique for the development of verified programs and hardware. Despite recent advances, reactive synthesis is still not practical when the specified systems reach a certain bound in size and complexity. In this paper, we present a modular synthesis algorithm that decomposes the specification into smaller subspecifications. For them, independent synthesis tasks are performed, and the composition of the resulting implementations is guaranteed to satisfy the full specification. Our algorithm is a preprocessing technique that can be applied to a wide range of synthesis tools. We evaluate our approach with state-of-the-art synthesis tools on established benchmarks and obtain encouraging results: The overall runtime decreases significantly when synthesizing implementations modularly.
翻译:主动合成是自动从规格中产生执行的任务,是开发经核实的程序和硬件的有希望的技术。尽管最近有所进步,但当特定系统达到一定的大小和复杂程度时,反应合成仍然不切实际。在本文件中,我们提出了一个模块合成算法,将规格分解成较小的子规格。对于它们来说,要执行独立合成任务,因此,执行的构成保证满足全部规格。我们的算法是一种预处理技术,可以应用于广泛的综合工具。我们用最先进的综合工具评估我们的方法,在既定基准方面,并取得令人鼓舞的结果:在模块化实施时,总体运行时间会大大缩短。