We present WhyMon, a runtime monitoring tool that produces explanations as verdicts. Receiving as input a metric first-order temporal logic (MFOTL) formula and a stream prefix of time-stamped data-carrying events, WhyMon incrementally outputs explanations that describe why each variable assignment satisfies or violates the formula. The tool includes a graphical user interface that facilitates the exploration and understanding of these explanations. Additionally, it incorporates a formally verified checker that can certify the explanations. In this tool paper, we describe WhyMon's architecture and its command line and interactive user interfaces, and demonstrate its usefulness in a case study.
Paper draft