度量区间时态逻辑的综合研究
On Synthesis of Metric Interval Temporal Logics
浏览论文内容
中文总结 AI 辅助
针对现有被动学习方法局限，提出首个不依赖预定义模板的度量区间时态逻辑（MITL）精确被动学习框架，通过归约为非定时问题实现，经基准测试验证有效。
中文摘要 AI 辅助
形式规格说明的自动挖掘对实时系统验证至关重要，但现有被动学习方法仍局限于确定性规格说明或定时正则表达式（TRE）的有限片段。据我们所知，本文提出首个框架，用于对表达性定时逻辑——度量区间时态逻辑（MITL）进行精确的被动学习，且不依赖预定义模板或受限逻辑片段。我们的方法将定时学习问题形式化归约为可扩展的非定时问题，通过识别正、负轨迹间的定量时序差异，合成精确的定时约束并将其注入为新的布尔原子命题。这将时序信息嵌入字母表，把复杂公式评估委托给高度优化的现成非定时LTL工具。关键在于，我们的框架是完备的，保证总能找到可区分的规格说明。我们在多个基准测试中评估了实现，证明了方法的有效性。
英文摘要
Automated mining of formal specifications is vital for verifying real-time systems. However, existing passive learning approaches remain restricted to deterministic specifications or limited fragments of Timed Regular Expressions (TRE). To our knowledge, this paper presents the first framework to tackle \emph{precise} passive learning for an expressive timed logic, \emph{Metric Interval Temporal Logic} (MITL) without relying on predefined templates or restricted logic fragments. Our approach formally reduces the timed learning problem into a scalable untimed one. By identifying quantitative timing differences between positive and negative traces, we synthesise precise timed constraints and inject them as new Boolean atomic propositions. This embeds timing into the alphabet, delegating the complex formula evaluation to highly optimised, off-the-shelf untimed LTL tools. Crucially, our framework is complete, guaranteeing a separating specification can always be found. We evaluate our implementation across several benchmarks, demonstrating the effectiveness of our approach.
发表机构
- University of Sussex（萨塞克斯大学）
- IIT Bombay（印度理工学院孟买分校）
- IIT Guwahati（印度理工学院古瓦哈提分校）
机构由 AI 辅助整理，请以论文原文为准。
