MightyPPL : Towards model checking MTL
TL;DR
An upgraded version of MIghtyPPL is introduced that enables for the first time, the model checking of Metric Temporal Logic 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.
Abstract
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.