Pattern-Based Refinement of Assume-Guarantee Specifications in Reactive Synthesis?

Abstract. We consider the problem of compositional refinement of com-ponents ’ specifications in the context of compositional reactive synthe-sis. Our solution is based on automatic refinement of assumptions and guarantees expressed in linear temporal logic (LTL). We show how be-haviors of the environment and the system can be inferred from counter-strategies and strategies, respectively, as formulas in special forms called patterns. Instantiations of patterns are LTL formulas which hold over all runs of such strategies, and are used to refine the specification by adding new input assumptions or output guarantees. We propose three different approaches for compositional refinement of specifications, based on how much information is shared between the components, and demonstrate and compare the methods empirically.