SYNTECH

Abstract (journal version)

Reactive synthesis is an automated procedure to obtain a correct-by-construction reactive system from its temporal logic specification. GR(1) is an expressive assume-guarantee fragment of LTL that enables efficient synthesis and has been recently used in different contexts and application domains. A common form of providing system's requirements is through use cases, which are existential in nature. However, GR(1), as a fragment of LTL, is limited to universal properties. In this paper we introduce GR(1)*, which extends GR(1) with existential guarantees. We show that GR(1)* is strictly more expressive than GR(1) as it enables the expression of guarantees that are inexpressible in LTL. We solve the realizability problem for GR(1)* and present a symbolic strategy construction algorithm for GR(1)* specifications. Importantly, in comparison to GR(1), GR(1)* remains efficient: the time complexity of our realizability checking and synthesis procedures for GR(1)* is identical to the time complexity of the known corresponding procedures for GR(1).

G. Amram, S. Maoz and O. Pistiner, GR(1)*: GR(1) Specifications Extended with Existential Guarantees. Formal Aspects of Computing, Springer, 2021.