paperbot · PL 论文追踪

全部论文 待读 收藏

P2 Kind Controllers and Fast Heuristics for Non-Well-Separated GR(1) Specifications

Kind 控制器与面向非良分离 GR(1) 规约的快速启发式
ICSE Proceedings of the IEEE/ACM 46th International Conference on Software Engineering2024匹配度 2/10 · 该论文属于反应式合成与形式化方法，讨论 GR(1) 规约的非良分离质量问题，与用户关注的 LLM/Agent 改进静态分析或形式化验证这一交叉方向没有直接关联。虽然形式化验证是相关领域，但本文未涉及 LLM、Agent、浮点程序分析或贝叶斯程序分析等核心主题。引用 7 inbox
Ariel Gorenstein, Shahar Maoz, Jan Oliver Ringert
程序合成逻辑与自动机
crossref: 2026-09-12

AI 速览

一句话：提出面向非良分离 GR(1) 规约的 Kind 控制器与快速启发式，以处理 NWS 质量问题。

非良分离（NWS）是反应式合成规约中的已知质量问题：当合成系统能够通过阻止环境满足其假设来避免满足自身保证时，就会出现 NWS。本文针对非良分离的 GR(1) 规约，提出 Kind 控制器与快速启发式方法。其目的可能是让合成出的控制器在满足自身保证的同时，尽可能不阻碍环境实现其假设，从而缓解 NWS 带来的规约缺陷。标题表明方法面向 GR(1) 这一常用的反应式合成片段，并强调启发式的速度。摘要未给出具体实验评估。

问题
GR(1) 反应式合成中，非良分离（NWS）规约允许合成系统通过阻止环境满足假设来规避保证，构成规约质量缺陷。
方法
论文提出 Kind 控制器与快速启发式，面向非良分离的 GR(1) 规约进行处理；标题暗示方法关注控制器的友善性与启发式效率。
评估
给出的摘要仅说明 NWS 问题，未描述具体评估；标题表明工作面向 GR(1) 规约并提出快速启发式。
原文摘要（Abstract）

Non-well-separation (NWS) is a known quality issue in specifications for reactive synthesis. The problem of NWS occurs when the synthesized system can avoid satisfying its guarantees by preventing the environment from being able to satisfy its assumptions.

链接与引用

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

BibTeX 
@inproceedings{paperbot11409,
  title = {Kind Controllers and Fast Heuristics for Non-Well-Separated GR(1) Specifications},
  author = {Ariel Gorenstein and Shahar Maoz and Jan Oliver Ringert},
  booktitle = {ICSE},
  year = {2024},
  doi = {10.1145/3597503.3608131}
}