Synthesis from Recursive-Components Libraries

TL;DR

This paper extends synthesis algorithms to handle recursive component libraries with call and return control flow, using a richer logic formalism, and proves the problem's computational complexity.

Contribution

It introduces Nested-Words Temporal Logic synthesis from recursive component libraries, providing a new algorithm and complexity analysis.

Findings

Developed a synthesis algorithm for NWTL with recursive components.

Proved the synthesis problem is 2EXPTIME-complete.

Extended previous work on library-based synthesis to include call and return structures.

Abstract

Synthesis is the automatic construction of a system from its specification. In classical synthesis algorithms it is always assumed that the system is "constructed from scratch" rather than composed from reusable components. This, of course, rarely happens in real life. In real life, almost every non-trivial commercial software system relies heavily on using libraries of reusable components. Furthermore, other contexts, such as web-service orchestration, can be modeled as synthesis of a system from a library of components. In 2009 we introduced LTL synthesis from libraries of reusable components. Here, we extend the work and study synthesis from component libraries with "call and return"' control flow structure. Such control-flow structure is very common in software systems. We define the problem of Nested-Words Temporal Logic (NWTL) synthesis from recursive component libraries, where NWTL is a specification formalism, richer than LTL, that is suitable for "call and return" computations. We solve the problem, providing a synthesis algorithm, and show the problem is 2EXPTIME-complete, as standard synthesis.