Explainable Online Monitoring of Metric Temporal Logic

Abstract

Runtime monitors analyze system execution traces for policy compliance. Monitors for propositional specification languages, such as metric temporal logic (MTL), produce Boolean verdicts denoting whether the policy is satisfied or violated at a given point in the trace. Given a sufficiently complex policy, it can be difficult for the monitor’s user to understand how the monitor arrived at its verdict. We develop an MTL monitor that outputs verdicts capturing why the policy was satisfied or violated. Our verdicts are proof trees in a sound and complete proof system that we design. We demonstrate that such verdicts can serve as explanations for end users by augmenting our monitor with a graphical interface for the interactive exploration of proof trees. As a second application, our verdicts serve as certificates in a formally verified checker we develop using the Isabelle proof assistant.

Lima and Traytel are supported by a Novo Nordisk Fonden start package grant (NNF20OC0063462). Raszyk’s work was carried out during his past employment at ETH Zürich supported by the Swiss National Science Foundation grant Big Data Monitoring (167162). All authors thank David Basin for supporting this work.

1 Introduction

In runtime verification, monitoring is the task of analyzing an event stream produced by a running system for violations of specified policies. An online monitor for a propositional policy specification language, such as metric temporal logic (MTL), consumes the stream event-wise and gradually produces a stream of Boolean verdicts denoting the policy’s satisfaction or violation at every point in the event stream. MTL monitors [3, 19, 24, 27, 33] use complex algorithms, whose correctness is not obvious, to efficiently arrive at the verdicts. Yet, users must rely on the algorithms being correct and correctly implemented, as the computed verdicts carry no information as to why the policy is satisfied or violated.

The two main approaches to increase the reliability of complex algorithm implementations are verification and certification. Formal verification using proof assistants or software verifiers is laborious and while it provides an ultimate level of trust, the user of a verified tool still gains no insight into why a specific, surely correct verdict was produced. In contrast, certification can yield both trust (especially when the certificate checker is itself formally verified) and insight, provided that the certificate is not only machine-checkable but also human-understandable.

In this paper, we develop a certification approach to MTL monitoring: instead of Boolean verdicts, we require the monitor to produce checkable and understandable certificates. To this end, we develop a sound and complete local proof system (§2) for the satisfaction and violation of MTL policies. Following Cini and Francalanza [15], local means that a proof denotes the policy satisfaction on a given stream of events and not general MTL satisfiability (for any stream). Our proof system is an adaptation of Basin et al.’s [4] local proof system for LTL satisfiability on lasso words to MTL with past and bounded future temporal operators. A core design choice for our proof system was to remain close to the MTL semantics and thus to be understandable for users who reason about policies in terms of the semantics. Therefore, proof trees in our proof system, or rather their compact representation as proof objects (§3), serve as understandable certificates.

With the certificate format in place, we devise an algorithm that computes minimal (in terms of size) proof objects (§4). We implement the algorithm in OCaml and augment it with an interactive web application¹ to visualize and explore the computed proof objects (§5). Independently, we prove the soundness and completeness of our proof system and formally verify a proof checker using the Isabelle/HOL proof assistant. We extract OCaml code from this formalization and use it to check the correctness of the verdicts produced by our unverified algorithm. To ensure that our correct verdicts are also minimal, we develop a second formally verified but less efficient monitoring algorithm in Isabelle, which we use to compute the minimal proof object size when testing our unverified algorithm.

Finally, we demonstrate how our work provides explainable monitoring output through several examples (§6) and empirically evaluate our algorithm’s performance in comparison to other monitors (§7). In summary, we make the following contributions:

• We develop a sound and complete local proof system for past and bounded future MTL that follows closely the semantics of the MTL operators.

• We develop and empirically evaluate an efficient algorithm to compute size-minimal proof objects representing proof trees in our proof system.

• We implement our algorithm in a new, publicly available monitoring tool Explanator2 [22] that includes a web front end and a formally verified proof object checker.

Related Work. We take the work by Basin et al. [4] on optimal proofs for LTL on lasso words as our starting point but change the setting from lasso words to streams of time-stamped events and the logic from LTL to MTL. Moreover, Basin et al. considered the offline path checking problem, whereas we tackle online monitoring here.

Parts of the work presented here are also described in two B.Sc. theses by Yuan [39] and Herasimau [16]. Yuan developed the MTL proof system we present here as well as a monitoring algorithm for computing optimal proofs based on dynamic programming (similarly to Basin et al.’s algorithm [4]). Herasimau formalized Yuan’s development in Isabelle/HOL. We use his work as the basis for our formally verified checker. Here, we present a different algorithm that resembles the algorithms used by state-of-the-art monitors for metric first-order temporal logic [5, 29], which perform much better than dynamic programming algorithms for non-trivial metric interval bounds.

Basin et al.’s approach [4] is parameterized by a comparison relation on proof objects that specifies what the algorithm should optimize for. Yuan [39] discovers a flaw in the correctness claim for Basin et al.’s algorithm and corrects it by further restricting the supported comparisons. Herasimau [16] relaxes Yuan’s requirements while formally verifying the correctness statement. Our algorithm minimizes the computed proof objects’ size as this both simplifies the presentation and caters for a more efficient algorithm.

Formal verification of monitors is a timely topic. Some verified monitors were developed recently using proof assistants, e.g., VeriMon [29] and Vydra [28] in Isabelle and lattice-mtl [8] in Coq. Others leveraged SMT technology to increase their trustworthiness [12, 14]. To the best of our knowledge, we present the first verified checker for an online monitor’s output, even though verified certifiers are standard practice in other areas such as distributed systems [35], model checking [37, 38], and SAT solving [11, 21].

Several monitors visualize their output [1, 2, 7, 18, 25, 30]; some of these even present visually separate verdicts for different parts of the policy. Our work takes inspiration from these approaches, but goes deeper: our minimal proof trees characterize precisely how the verdicts for the different parts compose to a verdict for the overall policy.

Our work follows the “proof trees as explanations” paradigm and thereby joins a series of works on LTL [4, 15, 32], CFTL [13], and CTL [9]. Of these only Basin et al. [4] supports past operators and none support metric intervals. Two of the above works [9, 15] use proof systems based on the unrolling equations for temporal operators instead of the operator’s semantics, which we believe is suboptimal for understandability: users think about the operators in terms of their semantics and not in terms of unrolling equations.

Outside of the realm of temporal logics one can find the “proof trees as explanations” paradigm in regular expression matching [31] and in the database community [10].

Fig. 1.

Semantics of MTL for a fixed trace $\rho = \left\langle (\pi _i,\tau _i)\right\rangle _{i \in \mathbb {N}}$

Metric Temporal Logic. We briefly recall MTL’s syntax and point-based semantics [6]. MTL formulas are built from atomic propositions (a, b, c, $\ldots$) via Boolean ($\wedge$, $\vee$, $\lnot$) and metric temporal operators (previous $\CIRCLE _{I}$, next $\Circle _{I}$, since $\mathrel {\mathcal {S}_{I}}$, until $\mathrel {\mathcal {U}_{I}}$), where $I=[l,r]$ is a non-empty interval of natural numbers with $l \in \mathbb {N}$ and $r \in \mathbb {N} \cup \{\infty \}$. We omit the interval when $l = 0$ and $r = \infty$. For the until operator $\mathrel {\mathcal {U}_{[l,r]}}$, we require the interval to be bounded, i.e., $r \ne \infty$. Formulas are interpreted over streams of time-stamped events $\rho = \left\langle (\pi _i,\tau _i)\right\rangle _{i \in \mathbb {N}}$, also called traces. An event $\pi _i$ is a set of atomic propositions that hold at the respective time-point i. Time-stamps $\tau _i$ are natural numbers that are required to be monotone (i.e., $i \le j$ implies $\tau _i \le \tau _j$) and progressing (i.e., for all $\tau$ there exists a time-point i with $\tau _i > \tau$). Note that consecutive time-points can have the same time-stamp. Figure 1 shows MTL’s standard semantics for a formula $\varphi$ at time-point i for a fixed trace $\rho$.

Fix a trace $\rho = \left\langle (\pi _i,\tau _i)\right\rangle _{i \in \mathbb {N}}$. The earliest time-point of a time-stamp $\tau$ on $\rho$ is the smallest time-point i such that $\tau _i \ge \tau$ and is denoted as $\textsf{ETP}_\rho (\tau )$. Similarly, the latest time-point of a time-stamp $\tau \ge \tau _0$ on $\rho$ is the greatest time-point i such that $\tau _i \le \tau$ and is denoted as $\textsf{LTP}_\rho (\tau )$. Whenever the trace $\rho$ is fixed, we will only write $\textsf{ETP}(\tau )$ and $\textsf{LTP}(\tau )$.

2 Local Proof System

Fig. 2.

Local proof system for MTL for a fixed trace $\rho = \left\langle (\pi _i,\tau _i)\right\rangle _{i \in \mathbb {N}}$

We introduce a local proof system for monitoring MTL formulas as the least relation satisfying the rules shown in Figure 2. It contains two mutually dependent judgments: $\vdash ^+$ (for satisfaction proofs) and $\vdash ^-$ (for violation proofs). A satisfaction (violation) proof describes the satisfaction (violation) of a formula at a given time-point on a fixed trace $\rho$. Each rule is suffixed by $^+$ or $^-$, indicating whether an operator has been satisfied or violated. Moreover, we define $\textsf{E}_{i}^{\text {p}}(I) {:}{=}\textsf{ETP}(\tau _i-r)$ and $\textsf{L}_{i}^{\text {p}}(I) {:}{=}\min (i,\textsf{LTP}(\tau _i-l))$ for $I=[l,r]$, which correspond to the earliest and latest time-point within the interval I, respectively, when formulas having $\mathrel {\mathcal {S}_{I}}$ as their topmost operator are considered. In the definition of $\textsf{L}_{i}^{\text {p}}(I)$ we take the minimum to account for consecutive time-stamps with the same value. For formulas having $\mathrel {\mathcal {U}_{I}}$ as their topmost operator, both definitions are mirrored, resulting in $\textsf{E}_i^{\text {f}}(I) {:}{=}\max (i, \textsf{ETP}(\tau _i+l))$ and $\textsf{L}_i^{\text {f}}(I) {:}{=}\textsf{LTP}(\tau _i+r)$.

The semantics of the MTL operators directly corresponds to the satisfaction rules $ap^{+}$, $\lnot ^{+}$, $\vee ^{+}_L$, $\vee ^{+}_R$, $\wedge ^{+}$, $\mathrel {\mathcal {S}_{}}^{+}$, $\mathrel {\mathcal {U}_{}}^{+}$, $\CIRCLE _{}^{+}$, and $\Circle _{}^{+}$. For instance, consider two time-points j and i such that $j \le i$. The rule $\mathrel {\mathcal {S}_{}}^{+}$ is applied whenever the time-stamp difference $\tau _i - \tau _j$ belongs to the interval I, and there is a witness for a satisfaction proof of $\beta$ in the form of $j \vdash ^+\beta$ together with a finite sequence of satisfaction proofs of $\alpha$ for all $k \in \left( j,i\right]$. The violation rules for the non-temporal operators $ap^{-}$, $\lnot ^{-}$, $\vee ^{-}$, $\wedge ^{-}_L$, $\wedge ^{-}_R$ are dual to their satisfaction counterparts. On the other hand, the violation rules for the temporal operators $\CIRCLE _{I}$, $\Circle _{I}$, $\mathrel {\mathcal {S}_{I}}$, and $\mathrel {\mathcal {U}_{I}}$ are derived by negating and rewriting their semantics. Consider $\mathrel {\mathcal {S}_{I}}$ with $I = [l, r]$:

The rules $\mathrel {\mathcal {S}_{}}^{-}$, $\mathrel {\mathcal {S}_{}}^{-}_{\infty }$, and $\mathrel {\mathcal {S}_{}}^{-}_{<I}$ correspond to the three disjuncts in Equation (1). We argue that these three cases intuitively represent different ways of violating a since operator. In the first disjunct, $\alpha$ is violated at some time-point after the interval starts and $\beta$ is violated from that time-point until the interval ends. Indeed, the violation proof $j \vdash ^-\alpha$ is enough to dismiss all previous occurrences of a satisfaction of $\beta$. Moreover, if $l \ne 0$, i.e., if the interval does not include the current time-point, then $\alpha$ may be violated between the interval’s end and the current time-point. Figure 3(a) shows both cases, where $\overline{\varphi }$ denotes a violation of $\varphi$. In the second disjunct, $\beta$ is violated at every time-point inside the interval (Figure 3(b)). The third disjunct captures the special case at the beginning of the trace when the interval is located before the first time-point (Figure 3(c)). Next, we consider $\mathrel {\mathcal {U}_{I}}$:

Fig. 3.

Graphical representation of the violation cases for $\alpha \mathrel {\mathcal {S}_{I}} \beta$ with $I = [l, r]$

The rules $\mathrel {\mathcal {U}_{}}^{-}$ and $\mathrel {\mathcal {U}_{}}^{-}_{\infty }$ correspond to the two disjuncts in Equation (2). In the first disjunct, $\beta$ is violated from the interval start until a time-point j at which also $\alpha$ is violated. Symmetrically to $\mathrel {\mathcal {S}_{}}^{-}$, we can dismiss all satisfactions of $\beta$ after j because of the violation proof $j \vdash ^-\alpha$. In the second disjunct, $\beta$ is violated at every time-point inside the interval.

Theorem 1

Fix an arbitrary trace $\rho = \left\langle (\pi _i,\tau _i)\right\rangle _{i \in \mathbb {N}}$. For any formula $\varphi$ and $i \in \mathbb {N}$, we have $i\vdash ^+\varphi$ iff $i\vDash \varphi$ and $i\vdash ^-\varphi$ iff $i\nvDash \varphi$, i.e., the proof system is sound and complete.

In other words, proof trees in our proof system contain all the necessary information to explain why a formula has been satisfied or violated on a given trace. A mechanically checked proof of the above statement can be found in our Isabelle formalization [22].

Example 1

Let $\rho = \langle (\{a,b,c\}, 1), (\{a,b\}, 3),(\{a,b\}, 3), (\{\cdot \}, 3), (\{a\}, 3), (\{a\}, 4)\rangle$ and $\varphi = a\mathrel {\mathcal {S}_{[1,2]}}(b\wedge c)$. A proof of $5\not \models \varphi$ has the following form:

In $\rho$, only events with time-stamp 3 satisfy the interval conditions, resulting in $\textsf{E}_{5}^{\text {p}}(I) = 1$ and $\textsf{L}_{5}^{\text {p}}(I) = 4$, where $I = [1,2]$. (Time-points are zero-based.) Thus, the portion of the trace we are interested in is $\langle (\{a,b\}, 3),(\{a,b\}, 3),(\{\cdot \}, 3), (\{a\}, 3)\rangle$. Here, a is only violated at time-point 3, so our proof includes the witness $3 \vdash ^-a$. From there until time-point $\textsf{L}_{5}^{\text {p}}(I) = 4$ the subformula $b \wedge c$ is violated, witnessed by $3 \vdash ^-b$ and $4 \vdash ^-b$. $\blacksquare$

3 Proof Objects

To make proofs from our proof system explicit, we define an inductive syntax for satisfaction ($\mathfrak {sp}$) and violation ($\mathfrak {vp}$) proofs and call this representation proof objects. Proof objects allow us to easily compute with, modify and compare the size of proof trees. From now on, the term proof will be used for both proof tree and proof object.

Here, $\overline{\mathfrak {sp}}$ and $\overline{\mathfrak {vp}}$ denote finite non-empty sequences of $\mathfrak {sp}$ and $\mathfrak {vp}$ subproofs and $\overline{\mathfrak {sp}_\varnothing }$ and $\overline{\mathfrak {vp}_\varnothing }$ denote finite possibly empty sequences of $\mathfrak {sp}$ and $\mathfrak {vp}$ subproofs. We define $\mathfrak {p}= \mathfrak {sp}\uplus \mathfrak {vp}$ to be the disjoint union of satisfaction and violation proofs. Given a proof $p \in \mathfrak {p}$, we define $\mathbb {V}(p)$ to be $\top$ if $p \in \mathfrak {sp}$ and $\bot$ if $p \in \mathfrak {vp}$. Each constructor corresponds to a rule in our proof system. Each proof p has an associated time-point $\textsf{tp}(p)$ for which it witnesses the satisfaction or violation. In some cases, $\textsf{tp}(p)$ can be computed recursively from p’s subproofs. For example, $\textsf{tp}( \mathrel {\mathcal {S}_{}}^{+} (p,[q_1, \dots , q_n]))$ is $\mathord {\mathsf {{tp}}}(q_n)$ if $n > 0$ and $\mathord {\mathsf {{tp}}}(p)$ otherwise. Similarly, $\mathord {\mathsf {{tp}}}( \mathrel {\mathcal {U}_{}}^{+} (p,[q_1, \dots , q_n]))$ is $\mathord {\mathsf {{tp}}}(q_1)$ if $n > 0$ and $\mathord {\mathsf {{tp}}}(p)$ otherwise. Other cases, namely $ap^{+}$, $ap^{-}$, $\CIRCLE _{<I}^{-}$, $\CIRCLE _{>I}^{-}$, $\Circle _{<I}^{-}$, $\Circle _{>I}^{-}$, $\mathrel {\mathcal {S}_{}}^{-}_{<I}$, $\mathrel {\mathcal {S}_{}}^{-}$, and $\mathrel {\mathcal {S}_{}}^{-}_{\infty }$, explicitly store the associated time-points as an argument of type $\mathbb {N}$ because we cannot compute them from the respective subproofs. For example, $\mathord {\mathsf {{tp}}}( ap^+ (j,a)) = j$ and $\mathord {\mathsf {{tp}}}( \mathrel {\mathcal {S}_{}}^{-} (j,q,[p_1, \dots , p_n])) = j$.

Given a trace $\rho = \left\langle (\pi _i,\tau _i)\right\rangle _{i \in \mathbb {N}}$ and a formula $\varphi$, we call a proof p valid at $\mathord {\mathsf {{tp}}}(p)$, denoted by $p \vdash \varphi$, if p represents a valid proof according to the rules of our local proof system. Note that once again we leave the dependency on $\rho$ implicit in $p \vdash \varphi$. Formally, validity $p \vdash \varphi$ is defined recursively, checking for each constructor that the corresponding rule has been correctly applied. For example, atomic proofs are valid if the mentioned atom is (not) contained in the trace at the specified time-points: $ap^+ (i,a) \vdash a \mathrel \leftrightarrow a \in \pi _i$ ($ap^- (i,a) \vdash a \mathrel \leftrightarrow a \notin \pi _i$). Moreover, for $r = \mathrel {\mathcal {S}_{}}^{+} (p,[q_1, \dots , q_n])$ we have

$$ \begin{array}{@{}lcl@{}}r \vdash \alpha \mathrel {\mathcal {S}_{I}} \beta &{}{}\mathrel \leftrightarrow {}&{} \mathord {\mathsf {{tp}}}(p)\le \mathord {\mathsf {{tp}}}(r) \wedge \tau _{\mathord {\mathsf {{tp}}}(r)} - \tau _{\mathord {\mathsf {{tp}}}(p)} \in I \wedge {}\\ {} &{}&{} [\mathord {\mathsf {{tp}}}(q_1), \dots , \mathord {\mathsf {{tp}}}(q_n)] = [\mathord {\mathsf {{tp}}}(p) + 1,\mathord {\mathsf {{tp}}}(r)] \wedge p \vdash \beta \wedge (\forall k \in [1,n].\;q_k \vdash \alpha )\text {.} \end{array}$$

Multiple valid proofs may exist for a time-point i and formula $\varphi$ as we demonstrate next.

Example 2

The proof object representing the proof tree from Example 1 is $P_1 = \, \mathrel {\mathcal {S}_{}}^{-} (5, ap^- (3,a),[ \wedge ^{-}_{L} ( ap^- (3,b)), \wedge ^{-}_{L} ( ap^- (4,b))])$. However, we could have argued differently, using the fact that c is violated at all time-points inside the interval. Then, $\mathrel {\mathcal {S}_{}}^{-}_{\infty }$ would be used instead to construct the proof $P_2 = \, \mathrel {\mathcal {S}_{}}^{-}_\infty (5,[ \wedge ^{-}_{R} ( ap^- (1,c)), \wedge ^{-}_{R} ( ap^- (2,c)), \wedge ^{-}_{R} ( ap^- (3,c)), \wedge ^{-}_{R} ( ap^- (4,c))])$, which is also a valid proof at $\mathord {\mathsf {{tp}}}(P_2) = 5$. In addition, $P_3 = \, \mathrel {\mathcal {S}_{}}^{-} (5, ap^- (3,a),[ \wedge ^{-}_{L} ( ap^- (3,c)), \wedge ^{-}_{L} ( ap^- (4,c))])$ is another valid proof at $\mathord {\mathsf {{tp}}}(P_3) = 5$. It is structurally identical to $P_1$, but instead of using the violations of b as witnesses for time-points 3 and 4, it uses the violations of c. In fact, both b and c are violated at time-points 3 and 4, so we can use either to justify the violations of $b \wedge c$.

We now compare $P_1$, $P_2$, and $P_3$. The proof $P_2$ uses $\mathrel {\mathcal {S}_{}}^{-}_{\infty }$, so we must store a witness of the violation of $b \wedge c$ for each one of the 4 time-points inside the interval. The proofs $P_1$ and $P_3$ use $\mathrel {\mathcal {S}_{}}^{-}$, taking advantage of the violation proof $3 \vdash ^-a$ that allows us to dismiss both $1 \vdash ^+a$ and $2 \vdash ^+a$. Formally, we define the size $|{p}|$ of a proof p to be the number of proof object constructors occurring in p. Then, $|{P_1}|=|{P_3}|=6$, and $|{P_2}|=9$.$\blacksquare$

We are particularly interested in small proofs as they tend to be easier to understand. Given a trace $\rho$ and a formula $\varphi$, a proof p is minimal at time-point i if and only if it is valid at i ($p \vdash \varphi$ and $\mathord {\mathsf {{tp}}}(p) = i$), and all other valid proofs q (at i) have greater or equal size ($q \vdash \varphi$ and $\mathord {\mathsf {{tp}}}(q) = i$ implies $|{p}| \le |{q}|$). In our example, $P_1$ and $P_3$ are minimal.

4 Computing Minimal Proofs

Given an MTL formula $\varphi$, our (online) monitor incrementally processes a trace and for each time-point i it outputs a minimal proof of the satisfaction or violation of $\varphi$ at i. The algorithm constructs this minimal proof of $\varphi$ by combining minimal proofs of $\varphi$’s immediate subformulas. To do this efficiently, the monitor maintains just enough information about the trace in its state so that it can guarantee to output minimal proofs. In case the monitored formula includes (bounded) future operators, the monitor’s output may be delayed, such that a single event may trigger the output of multiple proofs at once. In this section, we describe our algorithm in detail and explain its correctness.

4.1 Monitor’s State

Figure 4 shows the types of our algorithm’s main functions $\mathord {\mathsf {{init}}}$, which computes the monitor’s initial state, and $\mathord {\mathsf {{eval}}}$, which processes a time-stamped event while updating the monitor’s state and producing a list of minimal proofs (satisfactions or violations) for an in-order (potentially empty) sequence of time-points. Our monitor’s state (type $\mathord { state }$ in Figure 4) has the same tree-like structure as the monitored MTL formula. Additionally, it stores operator-specific information for each Boolean and temporal operator. For example, in the state of $\alpha \mathrel {\mathcal {S}_{I}}\beta$, we store the interval I, the states of the subformulas $\alpha$ and $\beta$, a buffer $\mathord { buft }$ for proofs (and associated time-stamps) coming from the recursive evaluation of subformulas and the operator-specific data structures $\mathord { saux }$. Our monitor’s overall structure is modeled after VeriMon [29], which has a similar interface ($\mathord {\mathsf {{init}}}$ and $\mathord {\mathsf {{eval}}}$) and $\mathord { state }$ type including the used buffers $\mathord { buf }$ and $\mathord { buft }$. The main novelty is our design of the $\mathord { saux }$ and $\mathord { uaux }$ data structures, which store sufficient information to compute minimal proofs for formulas with topmost operator $\mathrel {\mathcal {S}_{}}$ and $\mathrel {\mathcal {U}_{}}$. Here, we only describe $\mathord { saux }$ in detail.

Fig. 4.

Types of the monitor’s state and evaluation functions

The data structure $\mathord { saux }$ for a formula $\varphi = \alpha \mathrel {\mathcal {S}_{I}} \beta$ is a record consisting of nine fields. We will describe it next assuming that $\varphi$ is being evaluated at the current time-point cur. Furthermore, some fields have the type $\mathord { option }$, which means they are of the form $\bot$ (if no value is available) or $\lfloor v \rfloor$ (storing the value v). The function $\textsc {the}$ retrieves the optional value from $\lfloor v \rfloor$, i.e., $\textsc {the}\;(\lfloor v \rfloor )=v$. The field $\mathord {\mathsf {{ts}}}_{zero}$ stores $\bot$ in the initial state, and after the first event arrives, it stores the first time-stamp $\lfloor \tau _0 \rfloor$. Fields $\mathord {\mathsf {{ts\_tp}}}_{in}$ and $\mathord {\mathsf {{ts\_tp}}}_{out}$ store lists of time-stamp-time-point pairs inside the interval (between $\textsf{E}_{cur}^{\text {p}}(I)$ and $\textsf{L}_{cur}^{\text {p}}(I)$) and after the interval (between $\textsf{L}_{cur}^{\text {p}}(I) + 1$ and cur), respectively. The other fields store satisfaction (prefix $\mathord {\mathsf {{s\_}}}$) or violation ($\mathord {\mathsf {{v\_}}}$) proofs. Specifically, $\mathord {\mathsf {{s\_beta\_alphas}}}_{in}$ stores $\mathrel {\mathcal {S}_{}}^{+}$ proofs inside and $\mathord {\mathsf {{s\_beta\_alphas}}}_{out}$ stores $\mathrel {\mathcal {S}_{}}^{+}$ proofs after the interval. Crucially, while $\mathord {\mathsf {{s\_beta\_alphas}}}_{out}$ is an ordinary list, $\mathord {\mathsf {{s\_beta\_alphas}}}_{in}$ has type $\mathord { slist }$, which is a variant of the list type that indicates that the stored proofs are sorted in ascending order (with respect to size). We maintain this invariant to optimize the number of proofs we must store, i.e., if a proof enters the interval, we can delete all larger proofs that entered the interval prior to it. In addition, we can quickly access the first proof of this list which necessarily has minimal size. On the other hand, $\mathord {\mathsf {{s\_beta\_alphas}}}_{out}$ must store all proofs because it is not possible to predict when and which of these proofs will enter the interval.

Furthermore, $\mathord {\mathsf {{v\_alpha\_betas}}}_{in}$ is the analogue of $\mathord {\mathsf {{s\_beta\_alphas}}}_{in}$ for $\mathrel {\mathcal {S}_{}}^{-}$ proofs with a violation of $\alpha$ inside the interval, and a sequence of violations of $\beta$ until the end of the interval. Note that $\mathrel {\mathcal {S}_{}}^{-}$ proofs can also be constructed using a single violation proof of $\alpha$ that occurs after the interval, and these are instead stored in the also sorted list $\mathord {\mathsf {{v\_alphas}}}_{out}$. Moreover, $\mathrel {\mathcal {S}_{}}^{-}_{\infty }$ proofs require that $\beta$ is violated at all time-points inside the interval, so $\mathord {\mathsf {{v\_betas}}}_{in}$ stores a suffix of $\beta$ violations inside the interval. Finally, $\mathord {\mathsf {{v\_alphas\_betas}}}$ stores all $\alpha$ and $\beta$ violations outside the interval, so all other components that store violation proofs inside the interval can be efficiently updated when the interval shifts.

4.2 State Update

Algorithm 1: State update algorithm for Since

Algorithm 1 shows the skeleton of our procedure for updating (and simultaneously evaluating) the state of a since operator. The state update for $\varphi = \alpha \mathrel {\mathcal {S}_{I}} \beta$ is parametrized by the interval $I = [l,r]$, the current time-point cur and its time-stamp $\tau _{cur}$, minimal proofs $p_1$ and $p_2$ (obtained recursively) for the subformulas $\alpha$ and $\beta$, respectively, and the current state $\mathord { saux }$. The procedure first checks if cur is the first time-point to arrive and initializes $\mathord {\mathsf {{ts}}}_{zero}$ accordingly (line 2). Next, we add the new subproofs to their destinations (add_subps). For example, if $p_1 \in \mathfrak {sp}$ then all proofs from $\mathord {\mathsf {{s\_betas\_alphas}}}_{in}$ and $\mathord {\mathsf {{s\_betas\_alphas}}}_{out}$ are extended with this additional satisfaction proof for $\alpha$. In contrast, if $p_1 \in \mathfrak {vp}$ then both $\mathord {\mathsf {{s\_betas\_alphas}}}$ lists are emptied and the violation of $\alpha$ is stored in $\mathord {\mathsf {{v\_alphas}}}_{out}$ and $\mathord {\mathsf {{v\_alphas_betas}}}_{out}$ instead. A similar case distinction happens for $p_2$. After storing the proofs, we handle the case where cur is a time-point at the beginning of the trace for which the past interval has not started yet (lines 4–6), which corresponds to the $\mathrel {\mathcal {S}_{}}^{-}_{<I}$ case depicted in Figure 3(b) on the right. Here, we add a new time-stamp-time-point pair to $\mathord {\mathsf {{ts_tp}}}_{out}$ (line 5), and return the proof $\mathrel {\mathcal {S}_{}}^{-}_{<I} (cur)$ and the updated $\mathord { saux }$.

In the general case (when the interval has started), we compute the absolute time-stamp pair lr that constitute the boundaries of the past interval I relative to $\tau _{cur}$ (line 8). We use the absolute boundaries to identify a potential interval shift and move proofs in $\mathord { saux }$ from the out lists to the in lists accordingly (line 9). Lines 13–18 provide additional details in which order the various components are shifted. Lastly, we compute a minimal proof (line 10), performing a case distinction. If $\mathord {\mathsf {{s\_beta\_alphas}}}_{in}$ is non-empty, then its head must be a minimal satisfaction proof. Otherwise, the formula is violated and a minimal violation proof is either the head of $\mathord {\mathsf {{v\_alpha\_betas}}}_{in}$ or the head of $\mathord {\mathsf {{v\_alphas}}}_{out}$ (after adding a $\mathrel {\mathcal {S}_{}}^{-}$ constructor) or the application of $\mathrel {\mathcal {S}_{}}^{-}_{\infty }$ to $\mathord {\mathsf {{v\_betas}}}_{in}$ (provided that this suffix spans the entire interval which can be deduced by comparing the lengths of $\mathord {\mathsf {{v\_betas}}}_{in}$ and $\mathord {\mathsf {{ts\_tp}}}_{in}$). We extract these (at most three) candidates, compute their sizes, and pick one of minimal size. This minimal proof and the updated $\mathord { saux }$ are then returned (line 11).

Fig. 5.

The monitor’s $\mathord { saux }$ states when executing Example 1

Example 3

To illustrate how the state is updated, we once again consider the formula and trace introduced in Example 1. Figure 5 shows the $\mathord { saux }$ states of our algorithm and the produced minimal proof after processing every event. In every state, we only show the non-empty components. Initially, all components of the state are empty except for $\mathord {\mathsf {{ts}}}_{zero}$, which is $\bot$. When the first event $\left( \{a,b,c\}, 1\right)$ arrives, the list $\mathord {\mathsf {{ts\_tp}}}_{out}$ is updated accordingly and a pair with time-stamp 1 and a $\mathrel {\mathcal {S}_{}}^{+}$ proof using the satisfactions of b and c is added to $\mathord {\mathsf {{s\_beta\_alphas}}}_{out}$. This proof is clearly not valid for the current time-point 0, considering that the interval [1, 2] has not yet started, so the monitor outputs the trivial proof $\mathrel {\mathcal {S}_{}}^{-}_{<I} (0)$. The time-stamp of the first event moves inside the interval when the second event $\left( \{a,b\}, 3\right)$ arrives, and both $\mathord {\mathsf {{ts\_tp}}}_{out}$ and $\mathord {\mathsf {{ts\_tp}}}_{in}$ are updated accordingly. Furthermore, the algorithm extends the $\mathrel {\mathcal {S}_{}}^{+}$ proof previously stored in $\mathord {\mathsf {{s\_beta\_alphas}}}_{out}$ by adding $ap^+ (1,a)$ to the sequence of a satisfactions, after which the resulting proof is moved to $\mathord {\mathsf {{s\_beta\_alphas}}}_{in}$. The algorithm also appends the proof $ap^- (1,c)$ to $\mathord {\mathsf {{v\_alphas\_betas}}}_{out}$. Because $\mathord {\mathsf {{s\_beta\_alphas}}}_{in}$ is not empty, the monitor outputs the first proof of this list.

In the next step, event $\left( \{a,b\}, 3\right)$ arrives and the monitor proceeds similarly, adding the proof $ap^+ (2,a)$ to the $\mathrel {\mathcal {S}_{}}^{+}$ proof in $\mathord {\mathsf {{s\_beta\_alphas}}}_{in}$. Aside from outputting the extended satisfaction proof, the algorithm also adds the proof $ap^- (2,c)$ to $\mathord {\mathsf {{v\_alphas\_betas}}}_{out}$. When event $\left( \{\cdot \}, 3\right)$ arrives, the sequence of a satisfactions comes to an end, which indicates that the proofs in $\mathord {\mathsf {{s\_beta\_alphas}}}_{in}$ and $\mathord {\mathsf {{s\_beta\_alphas}}}_{out}$ are no longer valid nor useful. Hence, we clear both lists. In addition, the proof $ap^- (3,a)$ is stored in $\mathord {\mathsf {{v\_alphas}}}_{out}$, since the a violation happens after the interval. This subproof is also appended to $\mathord {\mathsf {{v\_alphas\_betas}}}_{out}$ along with the violation of the conjunction $\wedge ^{-}_L$. The algorithm then proceeds to construct a violation proof $\mathrel {\mathcal {S}_{}}^{-} (3, ap^- (3,a),[\cdot ])$ using the subproof stored in $\mathord {\mathsf {{v\_alphas}}}_{out}$ and outputs it. When $\left( \{a\}, 3\right)$ arrives, the algorithm appends the proof $\wedge ^{-}_L$ to $\mathord {\mathsf {{v\_alphas\_betas}}}_{out}$ and again uses the same subproof stored in $\mathord {\mathsf {{v\_alphas}}}_{out}$ to construct $\mathrel {\mathcal {S}_{}}^{-} (4, ap^- (3,a),[\cdot ])$. Note that this proof has an associated time-point of 4, which is the only distinction from the last proof that the monitor output.

Finally, when the last event $\left( \{a\}, 4\right)$ arrives, the interval shifts and $\mathord {\mathsf {{ts\_tp}}}_{in}$ and $\mathord {\mathsf {{ts\_tp}}}_{out}$ change accordingly. At this stage, the algorithm populates $\mathord {\mathsf {{v\_alpha\_betas}}}_{in}$ and $\mathord {\mathsf {{v\_betas}}}_{in}$ with the subproofs stored in $\mathord {\mathsf {{v\_alphas\_betas}}}_{out}$. In particular, it constructs and stores the proof $\mathrel {\mathcal {S}_{}}^{-} (5, ap^- (3,a),[ \wedge ^{-}_{L} ( ap^- (3,b)), \wedge ^{-}_{L} ( ap^- (4,b))])$ in $\mathord {\mathsf {{v\_alpha\_betas}}}_{in}$. Moreover, a sequence of violations of the conjunction inside the interval is stored in $\mathord {\mathsf {{v\_betas}}}_{in}$. This sequence of violations fills the entire interval, so it is then used to construct the proof $\mathrel {\mathcal {S}_{}}^{-}_\infty (5,[ \wedge ^{-}_{R} ( ap^- (1,c)), \wedge ^{-}_{R} ( ap^- (2,c)), \wedge ^{-}_{R} ( ap^- (3,c)), \wedge ^{-}_{R} ( ap^- (4,c))])$. The $\mathrel {\mathcal {S}_{}}^{-}$ proof corresponds precisely to the proof tree presented in Example 1, and the proof object $P_1$ in Example 2, whereas the $\mathrel {\mathcal {S}_{}}^{-}_{\infty }$ proof corresponds to the proof object $P_2$. Lastly, the size of these two proofs is computed, and the algorithm selects the $\mathrel {\mathcal {S}_{}}^{-}$ proof, since it is smaller (i.e., it includes fewer constructors).$\blacksquare$

4.3 Correctness

We now formally describe the invariant we maintain for $\mathord { saux }$. We write $\mathord {\mathsf {{ts}}}(p)$ for the time-stamp associated with a proof, i.e., the time-stamp $\tau _{\mathord {\mathsf {{tp}}}(p)}$ of the associated time-point $\mathord {\mathsf {{tp}}}(p)$. We also use functional programming notations like $\lambda$-abstractions and the list $\mathord {\mathsf {{map}}}$ function. We define the predicate $\mathord {\mathsf {{sorted}}}(seq)\;{:}{=}\bigl (\forall \left( \tau _i, p_i\right) ,\left( \tau _j, p_j\right) \in \mathord { seq }.\; \left( i< j\right) \wedge \left( j < \mathord {\mathsf {{length}}}\left( \mathord { seq }\right) \right) \mathrel \rightarrow \tau _i\le \tau _j\wedge |p_i| \le |p_j|\bigr )$ over a sequence of pairs of time-stamps and proofs and assume that every sequence below is monotone with respect to time-stamps ($i < j$ implies $\tau _i \le \tau _j$). The fields $\mathord {\mathsf {{ts}}}_{zero}$, $\mathord {\mathsf {{ts\_tp}}}_{in}$ and $\mathord {\mathsf {{ts\_tp}}}_{out}$ are characterized as follows:

The desired properties of the objects stored in other fields are given in Figure 6.

Fig. 6.

The algorithm’s invariant (soundness)

We describe each of the invariant’s statements. In (1) a proof in $\mathord {\mathsf {{s\_beta\_alphas}}}_{in}$ (which must be sorted) must have form $\mathrel {\mathcal {S}_{}}^{+} (p,\overline{q})$ and be a valid proof of $\alpha \mathrel {\mathcal {S}_{I}} \beta$ at the current time-point, with time-stamp $\mathord {\mathsf {{ts}}}\left( p\right)$. Next, (2) requires proofs to have the same form but instead be valid for a modified formula without the interval I. In this case, we can relax the timing constraint because these proofs will only be valid at a later time-point, namely once $\mathord {\mathsf {{ts}}}(p)$ moves inside the interval. The statement (3) is precisely the same as (1), but for $\mathrel {\mathcal {S}_{}}^{-}$ proofs. In (4), each proof p in $\mathord {\mathsf {{v\_alphas}}}_{out}$ (which must too be sorted) must be a valid subproof of a $\mathrel {\mathcal {S}_{}}^{-}$ proof at the current time-point with time-stamp $\mathord {\mathsf {{ts}}}(p)$. In (5), each subproof corresponding to the violation of $\beta$ must be inside the interval with time-stamp $\mathord {\mathsf {{ts}}}(p)$. The statement (6) specifies that outside the interval there is either a subproof of a violation of $\alpha$ or $\beta$ or there are no such proofs. These statements formalize what must hold for the things stored in $\mathord { saux }$, which yields soundness. We briefly consider completeness, by answering the question of what must be stored, on the example of $\mathord {\mathsf {{s\_beta\_alphas}}}_{in}$:

$$\begin{aligned}&\forall p\;\bar{q}\;\tau .\; \mathrel {\mathcal {S}_{}}^{+} (p,\overline{q}) \vdash \alpha S_I \beta \wedge \mathord {\mathsf {{tp}}}\left( S^+\left( p, \bar{q}\right) \right) = cur \wedge \tau = \mathord {\mathsf {{ts}}}\left( p\right) \mathrel \rightarrow \\&\qquad \bigl (\exists p'\;\bar{q}'\;\tau '.\; | \mathrel {\mathcal {S}_{}}^{+} (p',\overline{q}')| \le | \mathrel {\mathcal {S}_{}}^{+} (p,\overline{q})| \wedge \mathrel {\mathcal {S}_{}}^{+} (p',\overline{q}') \vdash \alpha \mathrel {\mathcal {S}_{I}}\beta \wedge \tau ' = \mathord {\mathsf {{ts}}}\left( p'\right) \wedge \\&\qquad \tau ' \ge \tau \wedge \mathord {\mathsf {{tp}}}\left( \mathrel {\mathcal {S}_{}}^{+} (p',\overline{q}')\right) = \mathord {\mathsf {{tp}}}\left( \mathrel {\mathcal {S}_{}}^{+} (p,\overline{q})\right) \wedge \left( \tau ', \mathrel {\mathcal {S}_{}}^{+} (p',\overline{q}')\right) \in \mathord {\mathsf {{s\_beta\_alphas}}}_{in}\bigr ) \end{aligned}$$

In words: for any valid $\mathrel {\mathcal {S}_{}}^{+}$ proof for $\varphi = \alpha \mathrel {\mathcal {S}_{I}} \beta$ at time-point cur, we must store in $\mathord {\mathsf {{s\_beta\_alphas}}}_{in}$ another proof at most as large and old, that is also valid for $\varphi$ at cur. Other fields of $\mathord { saux }$ have similar completeness statements and so have other state components.

Together, soundness and completeness ensure that given a formula, a trace, and a time-point i, our online monitoring algorithm will eventually output a valid minimal proof at i.

5 Implementation

We implement our algorithm in a new tool called Explanator2 [22]. The implementation amounts to around 4 000 lines of OCaml. In addition, a 6 900 lines long OCaml program is extracted from our Isabelle formalization consisting of 19 000 lines of definitions and proofs. The extracted program contains the proof object validity checker in the form of a function $\textsf {is\_valid} : \textit{trace} \rightarrow \textit{formula} \rightarrow \textit{proof} \rightarrow \textit{bool}$, which effectively implements what we denote by $p \vdash \varphi$. Moreover, it also contains the minimality checker $\textsf {is\_minimal} : \textit{trace} \rightarrow \textit{formula} \rightarrow \textit{proof} \rightarrow \textit{bool}$ that given a trace $\rho$, a formula $\varphi$, and a proof p computes a proof q for $\varphi$ on $\rho$ at time-point $\mathord {\mathsf {{tp}}}(p)$ with a minimal size using a verified dynamic programming algorithm and then checks that $|{p}| \le |{q}|$. Note that q may differ from p because minimal proof objects are not unique. Herasimau [16] provides more details on the formalization and the dynamic programming algorithm. We used the verified validity and minimality checkers to thoroughly test our unverified algorithm. Our tool includes a command line option to enable the verified certification of its output, which slows down computation as the verified algorithm is rather inefficient but increases trustworthiness.

Fig. 7.

Visualization of Example 1

Explanator2 also includes a JavaScript web front end. To this end, we transpile the compiled OCaml bytecode to JavaScript using Js_of_ocaml [36]. The resulting JavaScript library runs in any web browser. We augment the library with an interactive visualization using React [17]. Figure 7 shows the visualization of our Example 1. On the left, the visualization shows the trace (from top to bottom) consisting of the atomic propositions (columns a, b, and c), the time-stamps (column TS) and associated time-points (column TP). The following columns show either the topmost operator of the different subformulas or the atomic propositions of our monitored MTL formula $\varphi = a \mathrel {\mathcal {S}_{[1,2]}} (b \wedge c)$. In particular, the column labeled with $\varphi$’s topmost operator, namely $\mathrel {\mathcal {S}_{[1,2]}}$, shows the Boolean verdicts that a traditional monitor would output. Users of Explanator2 can further inspect the Boolean verdicts by clicking on them. Figure 7 shows the visualization’s state after clicking on $\varphi$’s violation at time-point 5. The visualization highlights the time interval and the Boolean verdicts for subformulas that justify the verdict associated with the inspected formula and time-point. Furthermore, it shows the relevant violations of $\varphi$’s subformulas a and $b\wedge c$: the subformula a is violated at time-point 3 and $b\wedge c$ is violated at time-points 3 and 4, which corresponds to a valid $\mathrel {\mathcal {S}_{}}^{-}$ proof. The user could continue the exploration by further clicking on the two $b\wedge c$ violations to find out that the tool used b violations to justify both. The visualization uses black circles to denote combinations of subformula and time-point that are relevant for at least one of $\varphi$’s verdicts. The Boolean value for these relevant subformula verdicts is only revealed upon exploration.

6 Examples

We demonstrate how the minimal proofs produced by our monitor can be useful when trying to comprehend a satisfaction or violation of an MTL formula. To this end, we consider Timescales [34], a benchmark generator for MTL monitors. Timescales uses predefined MTL formulas that represent temporal patterns that commonly occur in real system designs [20]. It generates traces, in which the time-stamps are equal to their corresponding time-points. We selected the two most complex properties and generated their corresponding traces. At the end of both traces there is a violation of the pattern, and we use our approach to explain these violations. In addition to the operators presented in Figure 2, we extended our proof system and algorithm with the following operators: $\top$ (truth), $\bot$ (falsity), $\rightarrow$ (implies), $\leftrightarrow$ (iff), $\blacksquare _{I}$ (historically), $\square _{I}$ (always), $\blacklozenge _{I}$ (once), and $\lozenge _{I}$ (eventually).

Fig. 8.

Proof of $\varphi _1$’s violation at time-point 61

Fig. 9.

Visualization of $\varphi _1$’s violation at time-point 61

Bounded Recurrence Between q and r. The bounded recurrence property specifies the following pattern: between events q and r there is at least one occurrence of event p every u time units. In MTL, this pattern is captured by the formula $\varphi _1 = \left( r \wedge \lnot q \wedge \blacklozenge _{} q\right) \rightarrow \left( (\blacklozenge _{[0,\,u]}\left( p \vee q\right) ) \mathrel {\mathcal {S}_{}} q\right)$. We set the bound $u = 3$, and we consider the trace $\langle \dots , (\{q\}, 56),(\{\cdot \}, 57),(\{\cdot \}, 58),(\{\cdot \}, 59), (\{\cdot \}, 60),(\{r\}, 61)\rangle$, which is the portion pertinent to the proof. The formula $\varphi _1$ is violated at time-point 61 and the proof is shown in Figure 8.

To prove the violation of the implication (the formula’s topmost operator) the subformula on the left (assumption) must be satisfied and the subformula on the right (conclusion) must be violated. For this reason, two subproofs are constructed. In the left subproof, we can see that the subformula on the left is violated because both conjuncts $r \wedge \lnot q$ and $\blacklozenge _{} q$ are satisfied at time-point 61. This part of the formula enforces that: (i) r is satisfied (and q is not satisfied) at the current time-point; and (ii) q is satisfied at some point in the past. Note that (ii) corresponds exactly to $\blacklozenge _{} q$. In the left subproof, we have $61 \vdash ^+r \wedge \lnot q$ because r is satisfied and q is violated at time-point 61. Moreover, the proof $61 \vdash ^+\blacklozenge _{} q$ uses the fact that q is satisfied at time-point 56, which is when the last q had arrived. Moving to the subproof $61 \vdash ^-(\blacklozenge _{[0,\,3]}\left( p \vee q\right) ) \mathrel {\mathcal {S}_{}} q$, the violation occurs because both subformulas are violated at time-point 61. The subproof $61 \vdash ^-\blacklozenge _{[0,3]} \left( p \vee q\right)$ uses the violations of p and q in the last 3 time units ($58,\dots ,61$), whereas the proof $61 \vdash ^-q$ indicates that q is not satisfied at the current time-point. This is sufficient to show that since the last q has arrived (at time-point 56), it is neither the case that a new sequence started (with a new occurrence of q) or that a sequence finished (with an occurrence of p) within 3 time units in the past.

Figure 9 shows our visualization of the above proof. Starting from $\rightarrow$, the columns show the topmost operators of $\varphi _1$’s subformulas (including atomic propositions). For example, $\varphi _1$ is violated because the left subformula is satisfied (the first $\wedge$ column) and the right subformula is violated (column $\mathrel {\mathcal {S}_{[0, \infty )}}$). All subformulas have a corresponding column and the order of the columns is such that immediate subformulas of a subformula appear further to the right. The same atomic proposition may occur in different subformulas, in which case there will be multiple columns showing the same proposition (but potentially different time-points of interest). Continuing our example, the right subproof from Figure 8 starts in column $\mathrel {\mathcal {S}_{[0, \infty )}}$ in Figure 9. The formula $(\blacklozenge _{[0,\,3]}\left( p \vee q\right) ) \mathrel {\mathcal {S}_{}} q$ is violated at time-point 61 because both subformulas are violated. In the visualization, we focus (by clicking) on the subformula $\blacklozenge _{[0,\,3]}\left( p \vee q\right)$ (displayed when hovering over the corresponding cell) and observe that it is violated because $p \vee q$ is violated at time-points $58, \dots , 61$ (highlighted cells in the $\vee$ column). Also, the context of this subproof, i.e., all parent nodes in the proof tree, is highlighted. In this case, these are $\rightarrow$ and $\mathrel {\mathcal {S}_{[0, \infty )}}$ at time-point 61. Even though it presents the exact same information as the proof tree, our interactive visualization makes the proofs easier to navigate, explore, and digest.

Bounded Response Between q and r. Closely related to the bounded recurrence, the bounded response property specifies the following pattern: between events q and r, event s must respond to event p within the interval [l, u]. In MTL, this pattern is specified by the formula $\varphi _2 = \left( \left( r \wedge \lnot q\right) \wedge \blacklozenge _{} q\right) \rightarrow \left( \left( \left( s \rightarrow \blacklozenge _{[l,u]} p\right) \wedge \lnot \left( \lnot s \mathrel {\mathcal {S}_{[u,\infty )}} p\right) \right) \mathrel {\mathcal {S}_{}} q\right)$. We consider the trace $\langle \dots , (\{q\}, 58),(\{p\}, 59),(\{\cdot \}, 60),(\{\cdot \}, 61), (\{\cdot \}, 62),(\{\cdot \}, 63),(\{r\},64)\rangle$ and set $l=0$ and $u=3$. Figure 10 shows a violation proof for $\varphi _2$ at time-point 64.

The implication’s assumption in $\varphi _2$ is the same as the assumption in $\varphi _1$ (the bounded recurrence formula). We omit the corresponding subproof P from Figure 11 as it has the same structure as the subproof of the bounded recurrence example. (Yet, there are differences in the time-points.) The conclusion of $\varphi _2$ has the form $\alpha \mathrel {\mathcal {S}_{}} q$. It is violated at time-point 64 because $\alpha$ is violated at time-point 62, and from this point onward until the current time-point 64, q is always violated. According to our proof system, we only need to consider violations of q starting at time-point 62, because $\alpha$ is violated at that point. The formula $\alpha = \left( s \rightarrow \blacklozenge _{[0,3]} p\right) \wedge \lnot \left( \lnot s \mathrel {\mathcal {S}_{[3,\infty )}} p\right)$ captures two properties: (i) if there is a response s then there must be a recent challenge p (i.e., p must be satisfied within the last 3 time units); (ii) there are no challenges p more than 3 time units in the past without a response s. In our proof, the violation of $\alpha$ is constructed using the violation of (ii). After applying the negation rule, the proof $62 \vdash ^+\lnot s \mathrel {\mathcal {S}_{[3,\infty )}} p$ uses the fact that p is satisfied at time-point 59 and that s is violated at time-points 60, 61 and 62. In other words, there was no response s to the challenge p within the required time constraint. Figure 11 shows the visualization of this subproof. While the static image already helps with the intuition, we invite the reader to explore this and the previous example in our interactive visualization.

Fig. 10.

Proof of $\varphi _2$’s violation at time-point 64

Fig. 11.

Visualization of $\varphi _2$’s violation at time-point 64

7 Performance

Fig. 12.

Evaluation results

We empirically evaluate our tool by answering the following research question: How does Explanator2 scale with respect to the formula size when compared to other state-of-the-art monitoring tools? To this end, we reuse the evaluation setup of the MTL monitor Hydra [26]. We consider two different settings: (i) past-only MTL formulas; and (ii) MTL formulas (mixing past and future operators). For each setting we pseudo-randomly generate a trace with $100\,000$ events and collections of five different formulas for each size $s\in \{6, 17, \dots , 50\}$ . We measure the time and space usage of the Explanator2, Hydra and Vydra [27], Aerial [3] MonPoly [5], and VeriMon [29]. Our verified dynamic programming algorithm is not included because it times out (with a time-out of 200 seconds) even for the smallest formulas of size 6. The experiments were conducted on a computer with an AMD Ryzen 5 5600X CPU and 16GB of RAM. The results are presented in Figure 12. Each filled shape is an average of the measurements for the corresponding formula size. (Unfilled shapes show the individual runs, but are sometimes invisible.) The axes showing time and space usage measurements are of logarithmic scale.

Time-wise, Explanator2 outperforms MonPoly and VeriMon (first-order monitors), and is on par with most of its competitors in the past-only setting. When we include future operators, Explanator2 performs worse than its competitors, although only by a narrow margin. However, we must consider that in contrast to the others our tool has a clear disadvantage: it produces checkable and understandable output instead of Boolean verdicts. Thus, these results reassure us that we do not compromise too much by providing this feature, and that our algorithm is indeed efficient. In terms of space usage, Explanator2 performs worse than other monitoring tools in both settings. This is hardly surprising, given that proofs can be huge (e.g., they may contain the entire trace).

8 Conclusion

We have developed an online MTL monitor that outputs detailed verdicts in the form of proof trees, which serve as both understandable explanations and checkable certificates. Our monitor incorporates a formally verified checker and an interactive visualization. Our empirical evaluation demonstrates the reasonable performance of our monitor, even though it provides a strictly more informative output than its competitors. Overall, we believe that our approach significantly improves the user experience when using an MTL monitor. In particular, the generated explanations provide insight into root causes of violations and can help with specification debugging. Another plausible application of explanations is teaching temporal logics to students and engineers.

As future work, we will lift our approach to the more expressive metric first-order temporal logic. The main challenge here is to incorporate parametric events and quantification. Moreover, we are interested in optimizing other aspects of the proofs than their size.

Data Availability Statement  Explanator2 is available under the GNU Lesser General Public License v3.0 [22] and its interactive visualization is hosted on GitHub. Our artifact [23] contains the snapshot of the tool’s source code at paper submission time along with instructions on how to run our test suite and to reproduce our evaluation.