paperbot · PL 论文追踪

全部论文 待读 收藏

P2 Just-in-time reactive synthesis

即时反应式合成
ASE Proceedings of the 35th IEEE/ACM International Conference on Automated Software Engineering2020匹配度 2/10 · 论文属于形式化方法与反应式程序合成，核心是 GR(1) 时序规约下的按需合成，与用户关注的静态分析、LLM/Agent 交叉、浮点程序分析及贝叶斯程序分析均无直接关系。虽然同属 PL/形式化验证大领域，但未涉及 LLM、工业落地或问题驱动的失效分析，因此匹配度很低。引用 12 inbox
Shahar Maoz, Ilia Shevrin
程序合成逻辑与自动机
crossref: 2026-09-12

AI 速览

一句话：提出即时（just-in-time）反应式合成，按需从 GR(1) 时序规约构造正确反应式系统。

反应式合成是一种从时序逻辑规约自动获得正确构造（correct-by-construction）的反应式系统的过程。GR(1) 是 LTL 中一个表达力强且支持高效合成的 assume-guarantee 片段，近年来已在不同上下文和应用领域中使用。本文标题表明其核心是“即时（just-in-time）反应式合成”，即把合成推迟到需要时按需进行，而不是完全离线预合成，以应对传统合成可能带来的高开销与实用性问题。摘要仅给出上述背景，未展开具体算法、实现或实验评估。

问题
如何高效地从时序逻辑规约自动合成反应式系统；传统离线合成可能开销较大，本文关注即时/按需的 GR(1) 合成。
方法
基于 GR(1) 这一 LTL 的 assume-guarantee 片段进行合成，并采用标题所示的即时（just-in-time）策略按需触发合成。
评估
摘要未说明具体评估方式；仅提到 GR(1) 合成已被用于不同上下文和应用领域。
原文摘要（Abstract）

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.

链接与引用

DOI 原文 · PDF（开放获取） ·

BibTeX 
@inproceedings{paperbot5933,
  title = {Just-in-time reactive synthesis},
  author = {Shahar Maoz and Ilia Shevrin},
  booktitle = {ASE},
  year = {2020},
  doi = {10.1145/3324884.3416557}
}