这篇论文解决了现实场景中演示数据不确定的问题,用汉明距离和伪布尔优化改进LTL学习,结果更靠谱,适合做形式化验证的朋友看看。
现有LTL学习方案通常假设演示正确,但实际中传感器故障或数据丢失会导致轨迹不确定。本文提出用汉明距离建模不确定性,为每条观测轨迹生成多个可能估计,并通过约束确保每组至少一条与学习公式一致。问题归约为伪布尔优化,在评估中恢复的规范比现有LTL学习方法更接近真实公式。
Learning Linear Temporal Specifications from Demonstrations with Uncertainty
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.