Unrealizable Cores for Reactive Systems Specifications

TL;DR

This paper introduces QuickCore and Punch, two algorithms that efficiently compute unrealizable cores in reactive system specifications, improving speed and support for complex constructs beyond traditional GR(1).

Contribution

The paper presents novel algorithms QuickCore and Punch for faster, comprehensive unrealizable core computation, extending support to specifications with advanced constructs.

Findings

QuickCore outperforms previous algorithms in speed, especially at larger scales.

Most specifications contain multiple unrealizable cores.

Punch efficiently finds all cores faster than naive methods.

Abstract

One of the main challenges of reactive synthesis, an automated procedure to obtain a correct-by-construction reactive system, is to deal with unrealizable specifications. One means to deal with unrealizability, in the context of GR(1), an expressive assume-guarantee fragment of LTL that enables efficient synthesis, is the computation of an unrealizable core, which can be viewed as a fault-localization approach. Existing solutions, however, are computationally costly, are limited to computing a single core, and do not correctly support specifications with constructs beyond pure GR(1) elements. In this work we address these limitations. First, we present QuickCore, a novel algorithm that accelerates unrealizable core computations by relying on the monotonicity of unrealizability, on an incremental computation, and on additional properties of GR(1) specifications. Second, we present Punch, a novel algorithm to efficiently compute all unrealizable cores of a specification. Finally, we present means to correctly handle specifications that include higher-level constructs beyond pure GR(1) elements. We implemented our ideas on top of Spectra, an open-source language and synthesis environment. Our evaluation over benchmarks from the literature shows that QuickCore is in most cases faster than previous algorithms, and that its relative advantage grows with scale. Moreover, we found that most specifications include more than one core, and that Punch finds all the cores significantly faster than a competing naive algorithm.