我的阅读状态 （保存写回仓库，全设备同步；首次保存需输入访问令牌）

AI 速览

一句话：研究不依赖模型的 GR(1) 规约固有空泛性，将空泛性分析从模型检查扩展到规约本身。

空泛性是形式化规约中一种著名的质量问题，已有研究多在模型检查语境下，借助模型判断规约是否被平凡满足。本文关注固有空泛性：它不依赖具体模型，而是直接针对规约本身。论文将这一概念引入 GR(1) 规约。GR(1) 是 LTL 的一个具有表达力的 assume-guarantee 片段，支持高效的符号合成，因此常用于反应式合成等场景。规约自身的空泛性可能影响后续合成与验证。摘要未给出具体判定算法、复杂度或实验评估，但论文的问题设定在于：如何在没有模型的情况下定义并处理 GR(1) 规约的固有空泛性。

问题

如何在不依赖具体模型的条件下，刻画并处理 GR(1) 规约中固有的空泛性，以避免规约被平凡满足。

方法

论文面向 GR(1) 这一 assume-guarantee 的 LTL 片段，在无模型语境下研究规约层面的固有空泛性；摘要未具体说明判定算法或技术路线。

评估

摘要未提供实验、案例研究或复杂度分析等评估信息。

链接与引用

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

@inproceedings{paperbot5725,
  title = {Inherent vacuity for GR(1) specifications},
  author = {Shahar Maoz and Rafi Shalom},
  booktitle = {FSE},
  year = {2020},
  doi = {10.1145/3368089.3409669}
}