在不确定数据下学习最小线性时序逻辑公式，提升安全系统规范提取可靠性。
Learning Linear Temporal Specifications from Demonstrations with Uncertainty
- 用汉明距离建模观测轨迹的不确定性，生成可能的补全轨迹
- 通过约束保证每组轨迹至少有一个符合学习到的逻辑公式
- 在噪声数据下比现有方法更接近真实规范，适合安全关键系统
从系统演示中学习时序逻辑规范对形式验证和控制器综合至关重要，尤其在安全关键领域。现有方法通常假设演示是正确的或仅受误分类误差影响。然而实践中，由于传感器故障、测量误差或数据丢失，系统轨迹往往存在不确定性或不完整。本文提出一种从带不确定性的演示中学习最小线性时序逻辑（LTL）公式的框架。该方法通过汉明距离建模不确定性，为每个观测轨迹生成可能的估计，并将这些估计分组，要求每组中至少有一个轨迹与学习到的公式一致。该问题被转化为等价的伪布尔优化问题。我们在多个基准上评估该方法，结果表明其在不确定性条件下能更准确地恢复出接近真实公式的规范。
原文摘要 · Abstract (English)
Learning temporal logic specifications from system demonstrations is essential for tasks such as formal verification and controller synthesis, especially in safety-critical domains. Existing approaches typically assume demonstrations are correct or only affected by misclassification errors. In practice, however, system traces are often uncertain or incomplete due to sensor faults, measurement errors, or data loss. We present a framework for learning minimal Linear Temporal Logic (LTL) formulas from demonstrations with uncertainty. Our approach models uncertainty via Hamming distance to generate possible estimates around each observed trace, which are grouped with constraints requiring that at least one trace per group is consistent with the learned formula. Our problem is then reduced to an equivalent Pseudo-Boolean Optimization. We evaluate our method against state-of-the-art LTL learning approaches and show that it recovers specifications that more closely align with ground-truth formulas under uncertainty.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。