Accelerating Kind Realizability: A Multi-stage Incremental Realizability Checking Framework

Abstract Non-well-separation is a common quality issue in reactive synthesis specifications, where the synthesized system can avoid satisfying its guarantees by preventing the environment from satisfying its assumptions. Kind realizability extends the usual GR(1) by additionally requiring the system to always enable the environment to satisfy its assumptions, thereby addressing this issue, and is expected to replace the usual GR(1) realizability checking. Kind realizability relies on a reduction and a 4-nested fixed-point algorithm, whose runtime typically exceeds that of the usual GR(1) realizability checking algorithm by more than 3 times, creating a significant performance bottleneck in specification development processes that require frequent realizability checks. This paper presents a framework designed to accelerate kind realizability checking, comprising: (1) a multi-level incremental checking framework that sequentially integrates approximate computation with the complete 4FP algorithm, reusing previously computed sound bounds at each stage to eliminate redundant state-space exploration; and (2) two accompanying approximation algorithms with lower asymptotic time complexity, which efficiently compute sound upper and lower bounds of the system winning region. Experiments on benchmarks comprising hundreds of specifications demonstrate significant performance improvements.