从轨迹学习GR(1)规范
Learning GR(1) Specifications from Traces
浏览论文内容
中文总结 AI 辅助
本文提出基于SAT的工具GR1MINE，利用GR(1)时序骨架与学习子句提升效率，在GR(1)及非GR(1)规范基准上，其学习可实现公式的速度与性能均优于现有基线工具。
中文摘要 AI 辅助
约束规范挖掘可从系统轨迹自动发现所需属性，广义1级反应性（GR(1)）是具有多项式时间综合能力的线性时序逻辑（LTL）片段，原生编码了硬件与机器人领域常见的假设-保证属性。本文提出GR1MINE，一种基于SAT的工具，用于从示例高效学习GR(1)公式。利用GR(1)时序骨架增量枚举公式候选，借助学习子句避免重复计算。在布尔GR(1) Syntech套件上，GR1MINE对全部60个基准学习出可实现公式，速度比通用及约束LTL挖掘工具快30倍以上；在SYNTCOMP的非GR(1)规范上，GR1MINE在超时内恢复的可实现规范仍比基线多2倍以上。
英文摘要
Constrained specification mining enables the automatic discovery of desired properties from system traces. Generalized Reactivity of Rank 1, or GR(1), is a fragment of LTL with polynomial-time synthesis that natively encodes assume-guarantee properties present in most hardware and robotics domains. In this paper, we present GR1MINE, a SAT-based tool for efficiently learning GR(1) formulas from examples. We exploit the GR(1) temporal skeleton to incrementally enumerate formula candidates, leveraging learnt clauses to avoid recomputation. On the Boolean GR(1) Syntech suite, GR1MINE learns a realizable formula for all 60 benchmarks over 30X faster than generic and constrained LTL mining tools. On non-GR(1) specifications from SYNTCOMP, GR1MINE is still able to recover >2X more realizable specifications than baselines within the timeout.
