What You Really Need To Know About Your Neighbor

TL;DR

This paper explores how to synthesize system components compositionally in reactive synthesis, especially when dominant strategies depend on assumptions about other components' future behaviors, introducing an incremental method to construct these assumptions.

Contribution

It generalizes previous compositional synthesis approaches by enabling incremental assumption construction for cases where dominant strategies are conditional.

Findings

Proposes an incremental synthesis method based on automatic assumption construction

Extends compositional synthesis to broader settings with conditional dominant strategies

Demonstrates the approach's effectiveness through case studies or experiments

Abstract

A fundamental question in system design is to decide how much of the design of one component must be known in order to successfully design another component of the system. We study this question in the setting of reactive synthesis, where one constructs a system implementation from a specification given in temporal logic. In previous work, we have shown that the system can be constructed compositionally, one component at a time, if the specification admits a "dominant" (as explained in Introduction) strategy for each component. In this paper, we generalize the approach to settings where dominant strategies only exist under certain assumptions about the future behavior of the other components. We present an incremental synthesis method based on the automatic construction of such assumptions.