一句话：提出演化感知的 GR(1) 可实现性检查启发式，复用先前检查的中间数据加速迭代开发中的检查。
反应式综合旨在从时序逻辑规约自动构造正确性由构造保证的反应式系统，但可实现性检查与综合耗时过长，阻碍了其实际采用。本文基于一个关键观察：开发者在迭代式规约开发过程中会频繁执行可实现性检查，因此复用先前检查的中间数据可显著缩短运行时间。为此，作者提出一种演化感知方法：计算规约新旧版本之间的局部语义 diff，结合上一次的可实现性检查结果，应用一组可靠的（sound）启发式，复用先前规约检查过程中收集的中间数据来加速当前规约的可实现性检查。在包含数千条真实规约的数据集上的评估表明，这些启发式在 70% 的情况下适用，并且其应用显著改善了可实现性检查的运行时间。
Reactive synthesis is an automated procedure to obtain a correct-by-construction reactive system from its temporal logic specification. Despite significant research progress over the past few decades, reactive synthesis is still in its early stages of practical adoption. One significant barrier to using reactive synthesis outside academia is the long realizability checking and synthesis time of specifications.This paper introduces a novel, evolution-aware approach for realizability checking. Our approach leverages the key observation that realizability checking is an operation that developers frequently perform during iterative specification development; therefore, utilizing intermediate data from previous realizability checks can substantially improve running times. Our approach computes a local semantic diff between previous and current versions of the specification, and, based on the diff and the previous realizability checking result, applies a set of sound heuristics. These heuristics reuse intermediate data collected during the previous specification’s realizability checking to accelerate the current specification’s realizability checking. Our evaluation demonstrates that these heuristics are applicable in 70% of cases from a real-world dataset containing thousands of specifications, and that their application significantly improves the running time of realizability checking.
DOI 原文 ·
@inproceedings{paperbot9430,
title = {Evolution-Aware Heuristics for GR(1) Realizability Checking},
author = {Dor Ma’ayan and Shahar Maoz and Jan Oliver Ringert},
booktitle = {ASE},
year = {2025},
doi = {10.1109/ase63991.2025.00030}
}