Leveraging Symmetry in GR(1) Synthesis

Reactive synthesis is an automated procedure to obtain a correct-by-construction reactive system from its temporal logic specification. GR(1) is an expressive fragment of LTL that enables efficient synthesis and has been recently used across different contexts and domains. However, as specification size grows, synthesizer performance becomes a major challenge because, like many formal algorithms, synthesis suffers from state-space explosion. That said, we observe that in practice, many large specifications exhibit symmetry, namely, they grow with one or more parameters and have an inherent structure – they are composed of groups of isomorphic blocks. In this work we introduce GR(1) symmetry, a mapping between specification variables that preserves the specification’s semantics, and show how to detect it and leverage it to skip costly semantic operations and instead use lightweight syntactic substitution at the BDD level. We implemented GR(1) symmetry utilization in the Spectra language and IDE, including a heuristic detection algorithm and an annotation allowing engineers to declare symmetries in the specification. Our experiments show that symmetry can be efficiently detected for small-scale specifications, extended to larger ones, and leveraged to significantly speed up GR(1) synthesis – specifically the realizability checking phase – for many specifications in known benchmarks.