发表机构
University of Sussex; Indian Institute of Technology Bombay; Indian Institute of Technology Guwahati; Max Planck Institute for Software Systems (MPI-SWS)（萨塞克斯大学; 孟买印度理工学院; 古瓦哈提印度理工学院; 马克斯·普朗克软件系统研究所）
机构由 AI 辅助整理，请以论文原文为准。AI 中文总结
本文介绍升级版MightyPPL工具，首次支持MTL中“事件p发生后恰好在k时间单位内跟随事件q”性质的模型检测，并兼容Pnueli和过去模态，性能显著优于Tempora。
AI 中文摘要
针对度量区间时序逻辑（MITL）的定时系统模型检测的理论基础早在20世纪90年代初就已建立，然而，首个支持未来MITL（MightyL）的实用工具直到2017年才出现。近年来，人们越来越关注扩展这一工具链以支持更具表达力的逻辑算子，包括过去模态、Pnueli模态以及奇异区间的有限使用。MightyPPL就是这样一个工具链。我们介绍了MightyPPL的升级版本，该版本首次实现了对度量时序逻辑（MTL）性质的模型检测，这些性质的形式为（每当事件p发生时，它最终会在恰好k个时间单位后被某个事件q跟随），此外还支持Pnueli和过去模态。我们讨论了该工具的底层架构和实现，并展示了与Tempora工具在不同可满足性和模型检测基准上的性能对比评估，结果表明MightyPPL提供了显著更优的性能。
英文摘要
The theoretical foundation for model checking timed systems against Metric Interval Temporal Logic (MITL) was established in the early 1990s, yet the first practical tool supporting future MITL (MightyL) did not emerge until 2017. Recently, there has been growing interest in extending this toolchain to support more expressive logical operators, including past modalities, Pnueli modalities, and limited use of singular intervals. MightyPPL is one such toolchain. We introduce an upgraded version of MIghtyPPL that enables for the first time, the model checking of Metric Temporal Logic (MTL) properties of the form (whenever an event p occurs, it is eventually followed by some event q after exactly some k time units) in addition to Pnueli and Past modalities. We discuss the tool's underlying architecture and implementation, and present a performance evaluation against the Tempora tool across diverse satisfiability and model checking benchmarks, demonstrating that MightyPPL delivers significantly better performance.
CommentsBest paper Award at QEST+FORMATS 2026, nominated for Best Artifact Award at QEST+FORMATS 2026
