figure a
figure b

1 Introduction

Runtime monitoring is concerned with the analysis of events produced by a system during its execution. An online monitor searches for given complex patterns in event streams, processing the stream incrementally, i.e., one event at a time. If it finds a pattern match, the monitor outputs a verdict to its user. The nature of a verdict depends on both the monitor and its pattern specification language. For propositional specification languages, such as metric temporal logic (MTL) [6, 21], typical verdicts are streams of Booleans [8, 28, 31], where each Boolean signifies the presence or the absence of a pattern match, i.e., the satisfaction or violation of the MTL formula at every position in the input stream.

Users might find Boolean outputs difficult to interpret, especially when complex patterns like nesting temporal operators are involved. In particular, Boolean verdicts give no insight into how monitors produce them—we have to trust their correctness. Even when assuming infallible monitors, verdict justifications can help us to ensure that we expressed correctly our intentions in the specification and, e.g., that it is not vacuously true [23].

Lima et al. [25] propose the use of richer verdicts in an MTL monitor. Specifically, they use proof trees in a dedicated proof system resembling MTL’s semantics to explain why a formula is satisfied or violated. They develop the Explanator2 monitor, which outputs a stream of size-minimal proof trees, and design an interactive graphical user interface for exploring and understanding these informative verdicts. In addition, they formally verify, in the Isabelle/HOL proof assistant, a proof tree checker certifying that their proof system rules were correctly applied. Thus proof tree verdicts serve a two-fold purpose: as machine-checkable certificates and human-readable explanations.

In this work, we significantly widen the scope of the “proof tree verdicts” approach. We provide certifiable and explainable monitoring verdicts for metric first-order temporal logic (MFOTL) [14] with bounded future operators and without equality between variables. MFOTL extends MTL with data parameters and first-order quantification and is an expressive formalism with many practical applications [7, 10,11,12,13]. We extend Lima et al.’s MTL proof system to MFOTL with the expected rules for quantifiers (Section 2): e.g., the universally quantified formula \(\forall x.\;\alpha \) is satisfied if \(\alpha \) with x replaced by d is satisfied for all domain values d. The key challenge here is that the domain is typically infinite, which results in the above proof rule for \(\forall \) to be infinitely branching. This is problematic because it is unclear how to validate a correct application of the \(\forall \) rule in a proof tree checker.

A crucial observation is that without equality between variables, proof trees cannot distinguish values outside of the active domain, i.e., the finite set of data values from the monitored event stream prefix and from the formula’s constants. Thus, the active domain’s size plus one bounds the number of choices for d requiring different proof trees, and we can reuse them–with the extra “plus one” representing values outside the active domain. Thus, to represent the \(\forall \) rule it suffices to store a finite partition of the domain and one subproof for each part. We obtain finite proof objects, develop a checker for them, and formally verify the checker’s correctness in Isabelle/HOL (Section 3).

The proof system explains how to deal with closed MFOTL formulas. A Boolean verdict for a formula with free variables only makes sense relative to a variable assignment. Hence, traditional MFOTL monitors compute sets of satisfying variable assignments [15, 30] instead of Boolean verdicts. In our setting, an explanation for a formula with free variables must provide a proof tree for any variable assignment (satisfying or violating). For infinite domains, there are infinitely many assignments, but the same idea that worked for quantifiers comes to our rescue: it suffices to consider a finite partition of the domain for each variable. Inspired by binary decision diagrams (BDDs) [16], we organize the partitions for different variables hierarchically in partitioned decision trees (PDTs). PDTs are trees where each leaf stores a generic data item and each node (representing a variable) branches on a finite partition of the domain (Section 4). The partitions may change from one node to the other. PDTs can be compacted (or reduced in BDD terminology).

We thus have arrived at our notion of explainable verdicts for MFOTL formulas: PDTs whose leaves are proof objects. We extend our verified checker from proof objects to such verdicts and Lima et al.’s algorithm for MTL [25] to MFOTL (Section 5). Our algorithm extension is modular in the sense that it merely adds a layer of PDTs, but keeps Lima et al.’s algorithms for temporal operators unchanged. We implement the extended algorithm in a new monitor and also extend Lima et al.’s interactive visualization of proof objects. We demonstrate the effectiveness of our new tool on MFOTL policies from the literature (Section 6). In summary, we make the following contributions:

  • We develop a proof system for MFOTL satisfaction and violation at a time-point for a given event stream and verify its soundness and completeness in Isabelle/HOL.

  • We finitely represent our proof system’s proof trees and formally verify a checker for them. The key idea is that finite partitions of infinite domains are sufficient.

  • We design partitioned decision trees (PDTs) to represent functions from variable assignments to generic data items in a way that enables sharing and compression.

  • We develop an algorithm computing explanations: PDTs with proof objects as leaves. We implement the algorithm in a new monitor, along with an interactive visualization of explanations and integrated with the verified proof tree checker for certification.

Our tool, called WhyMon, is publicly available [2].

Fig. 1.
figure 1

Semantics of MFOTL for a fixed stream \(\sigma = \left\langle \tau _i,\varGamma _i\right\rangle _{i\in \mathbb {N}}\).

Full size image

Further Related Work Lima et al.’s work [25], which we extend, is based on the work by Basin et al. [9] that employed proof trees as explanations in the context of understanding counterexamples of LTL model checkers. We refer to these works for a discussion of related proof systems for propositional temporal logics and regular expressions.

In the first-order monitoring setting, we are on unexplored territory with verdicts that go beyond satisfying assignments. Nonetheless our work incorporates ideas from existing first-order monitors. Most closely related is Havelund et al’s DejaVu monitor [18], which uses BDDs to represent sets of satisfying assignments. Our work generalizes BDDs to branching over partitions of the domain and storing generic data (e.g., proof objects) instead of Booleans in the leaves. In addition, the DejaVu authors make use of the fact that without equality between variables the formula’s satisfaction cannot be influenced by different values outside the active domain. We generalize this observation so that not only the satisfaction but rather entire proof trees can be reused when exchanging values outside the active domain. Finally, DejaVu only supports past temporal operators and closed formulas, whereas our algorithm supports both past and future operators and free variables.

Havelund et al.’s key observation fails for equalities between variables. For example, the formula \(x \approx y \rightarrow \textsf{p}(x, y)\) is satisfied for any pair of distinct values \(c \ne d\) outside of the predicate \(\textsf{p}\)’s interpretation, but it is violated if we pick the same value c for both x and y. A classic result by Ailamazyan et al. [5, 19] shows that for the relational calculus (MFOTL without temporal operators) it suffices to distinguish a finite number of equivalence classes of values outside of the active domain. While it is conceivable that this result generalizes to MFOTL with equality, we leave this generalization as future work.

The MFOTL monitor MonPoly [14, 15] and its formally verified counterpart VeriMon [30] output streams of satisfying assignments for formulas in the so-called monitorable fragment. The fragment ensures that all subformulas always evaluate to finite sets of satisfying assignments. Our monitor does not suffer from this limitation; even more it returns all satisfying and violating assignments (labeled and explained as such).

Outside of first-order monitoring, our visualization takes some inspiration from the stream runtime verification tool TeSSLa [24], which can provide output for all intermediate streams. Similarly, we provide output for all subformulas, but our proof trees allow us to focus on the relevant dependencies between a formula and its subformulas.

Metric first-order temporal logic (MFOTL) We recall MFOTL’s syntax and semantics. We fix an infinite domain \(\mathbb {D}\) (e.g., containing integers and strings). Terms \(t\in \mathbb {T}\) are either variables \(x, y, z \in \mathbb {V}\) or constants \(c, d \in \mathbb {D}\). Overlines indicate lists (finite sequences), e.g., if t is a term, then \(\overline{t}\) is a list of terms. The grammar below specifies MFOTL’s syntax, where \(\textsf{p} \in \mathbb {E}\) is a predicate name (e.g., a string) and \(I \in \mathbb {I} \subseteq 2^\mathbb {N}\) is a non-empty interval.

$$\begin{aligned} \alpha \ {:}{:}=& tt \mid ff \mid \textsf{p}(\overline{t})\mid x \approx c \mid \lnot \, \alpha \mid \alpha \wedge \alpha \mid \alpha \vee \alpha \mid \alpha \rightarrow \alpha \mid \exists x.\ \alpha \mid \forall x.\ \alpha \mid \\ &\CIRCLE _{I}\alpha \mid \Circle _{I}\alpha \mid \blacklozenge _{I}\alpha \mid \lozenge _{I}\alpha \mid \blacksquare _{I}\alpha \mid \square _{I}\alpha \mid \alpha \mathrel {\mathcal {S}_{I}}\alpha \mid \alpha \mathrel {\mathcal {U}_{I}}\alpha \end{aligned}$$

Besides the first-order logic operators, the syntax includes the past \(\CIRCLE _{}\) (previous), \(\blacklozenge _{}\) (once), \(\blacksquare _{}\) (historically), \(\mathrel {\mathcal {S}_{}}\) (since) and future \(\Circle _{}\) (next), \(\lozenge _{}\) (eventually), \(\square _{}\) (always), \(\mathrel {\mathcal {U}_{}}\) (until) temporal operators. We use \(\bigwedge \) for universal and \(\bigvee \) for existential quantification at the metalanguage level to avoid confusion with MFOTL formulas. We also use common interval notation \([a,b)=\{n\mid a\le n< b\}\) or \([a,c]=\{n\mid a\le n\le c\}\), for \(a,c\in \mathbb {N}\) and \(b \in \mathbb {N} \cup \{\infty \}\), and omit intervals when \(I=[0,\infty )=\mathbb {N}\). Whenever we write [a, c], we exclusively denote the range \([a, \dots , c]\) (rather than the two element sequence [a, c]). Furthermore, we assume that the future operators (\(\lozenge _{}\), \(\square _{}\), and \(\mathrel {\mathcal {U}_{}}\)) intervals are finite (also called bounded). We write \(a+I\) for \(\{a+x\mid x\in I\}\) and \(a\,\mathcal {R}\,I\) for \(\bigwedge x\in I.\; a\,\mathcal {R}\,x\) (where \(\mathcal {R} \in \{ <, \le , >, \ge \}\)). We interpret formulas over streams \(\sigma \): infinite sequences of time-stamped sets of events \(\sigma = \left\langle \tau _i,\varGamma _i\right\rangle _{i\in \mathbb {N}}\). We call the indices \(i\in \mathbb {N}\) time-points, so that \(\varGamma _i\) is the set of events and \(\tau _i \in \mathbb {N}\) is the time-stamp at time-point i. The time-stamps \(\tau _i\) must be monotone (\(\bigwedge i j.\;i \le j \longrightarrow \tau _{i} \le \tau _j\)) and eventually increasing (\(\bigwedge \tau .\;\bigvee i.\;\tau _{i} > \tau \)). Each event has the form \(\textsf{p}(d_1,\ldots , d_n)\) where \(\textsf{p}\) is the event name and \(d_i \in \mathbb {D}\). Given a total assignment v mapping variables to values in \(\mathbb {D}\), we define \(\llbracket \, x \,\rrbracket _{v}=v(x)\) and \(\llbracket \, c \,\rrbracket _{v}=c\). The notation \(\llbracket \, \overline{t} \,\rrbracket _{v}=\overline{c}\) lifts this operation to lists of terms. We define the satisfaction relation \(v,i \vDash _\sigma \alpha \) in the usual way (Figure 1). Finally, the earliest time-point \(\textsf{ETP}_\sigma (\tau )\) of \(\tau \in \mathbb {N}\) on \(\sigma \) is the smallest time-point i such that \(\tau _i\ge \tau \). Analogously, the latest time-point \(\textsf{LTP}_\sigma (\tau )\) of \(\tau \ge \tau _0\) on \(\sigma \) is the largest i such that \(\tau _i\le \tau \). We omit the stream \(\sigma \) (e.g., \(\vDash \), \(\textsf{ETP}\left( \tau \right) \) and \(\textsf{LTP}\left( \tau \right) \)) if it is clear from the context.

2 Proof System

We introduce a local proof system for MFOTL (Figure 2). “Local" means here that the proof system does not talk about satisfiability in general, but rather about the formula’s satisfaction or violation for a fixed stream, assignment, and time-point.

Our proof system consists of two mutually dependent judgments, \(\vdash ^+_\sigma \) and \(\vdash ^-_\sigma \) (again \(\sigma \) is omitted when clear), that characterize a formula’s satisfaction \(v,i\vdash ^+_\sigma \alpha \) and violation \(v,i\vdash ^-_\sigma \alpha \) relations for assignment v, stream \(\sigma \), and time-point i. The rules of our proof system closely follow the MFOTL semantics (Figure 1) and extend the proof system used by Lima et al. [25] with assignments (that are mostly passed around without modification) and the rules for quantifiers (which modify the assignments). The rules for atomic predicates and Boolean constants and operators are self-explanatory: e.g., predicates are satisfied if a matching event is present in the trace; a conjunction is satisfied if both conjuncts are satisfied; a conjunction is violated if either of the conjuncts is violated.

Fig. 2.
figure 2

Local proof system for MFOTL on a fixed stream \(\sigma = \left\langle \tau _i,\varGamma _i\right\rangle _{i\in \mathbb {N}}\).

Full size image

The rule \( \exists {}^{+} \) states that for v to satisfy \(\exists x.\ \alpha \) at i, it suffices to provide a domain value d such that the updated assignment \(v[x\mapsto d]\) setting x to d satisfies \(\alpha \) at i. Conversely, \( \exists {}^{-} \) asserts that the violation of \(\exists x.\ \alpha \) under v at i requires showing that all domain values make \(v[x\mapsto d]\) violate \(\alpha \) at i. Since the universal quantifier is dual to the existential one, the rules \( \forall {}^{-} \) and \( \forall {}^{+} \) exchange the relations \(\vdash ^+_\sigma \) and \(\vdash ^-_\sigma \) compared to \( \exists {}^{+} \) and \( \exists {}^{-} \).

The rules \( \blacklozenge _{}^{+} \) and \( \lozenge _{}^{+} \) are mere restatements of the MFOTL semantics. Since the operators \(\blacksquare _{I}\) and \(\square _{I}\) are respectively dual to \(\blacklozenge _{I}\) and \(\lozenge _{I}\), their violation rules \( \blacksquare _{}^{-} \) and \( \square _{}^{-} \) once again exchange \(\vdash ^+_\sigma \) and \(\vdash ^-_\sigma \) compared to \( \blacklozenge _{}^{+} \) and \( \lozenge _{}^{+} \). The rule \( \blacksquare _{<l}^{+} \) accounts for the vacuous truth of the operator \(\blacksquare _{I}\) near the start of the stream (when no time-points fall within the interval I). Dually, the rule \( \blacklozenge _{<l}^{-} \) asserts the violation of \(\blacklozenge _{I}\) near the start of the stream. The remaining rules \( \blacklozenge _{}^{-} \), \( \lozenge _{}^{-} \), \( \blacksquare _{}^{+} \), and \( \square _{}^{+} \) use notation \(\textsf{E}_{i}^{\text {p}}(I)\), \(\textsf{L}_{i}^{\text {p}}(I)\), \(\textsf{E}_{i}^{\text {f}}(I)\), and \(\textsf{L}_{i}^{\text {f}}(I)\) to refer to time-points of particular interest relative to the current time-point i. Specifically, for a future formula \(\varphi =\mathop {\mathcal {F}_I}\alpha \) with \(\mathcal {F}\in \{\Circle _{},\lozenge _{},\square _{}\}\) and interval \(I=[a,b]\) or \(I=[a,b)\) such that \(b\ne \infty \), the formula’s semantics at time-point i may need to refer to any time-point with time-stamp in \([\tau _i+a,\ldots ,\tau _i+b]\). The latest such time-point is \(\textsf{L}_{i}^{\text {f}}(I)=\textsf{LTP}(\tau _i+b)\) while the earliest one is \(\textsf{E}_{i}^{\text {f}}(I) = \max (i, \textsf{ETP}(\tau _i+a))\). For past operators \(\mathcal {P} \in \{\CIRCLE _{},\blacklozenge _{},\blacksquare _{}\}\), the relevant time-stamp interval is \([\tau _i-b,\ldots ,\tau _i-a]\) and the interval’s earliest time-point is \(\textsf{E}_{i}^{\text {p}}(I) = \textsf{ETP}(\tau _i-b)\) and its latest time-point is \(\textsf{L}_{i}^{\text {p}}(I) = \min (i,\textsf{LTP}(\tau _i-a))\).

Proof trees emerging from repeated application of the rules in our proof system contain all the necessary information to explain why a formula is satisfied or violated. In other words, our proof system is sound and complete, i.e., the following result holds.

Theorem 1

Let \(\alpha \) be a formula, v a variable assignment, \(i\in \mathbb {N}\) a time-point, and \(\sigma = \left\langle \tau _i,\varGamma _i\right\rangle _{i\in \mathbb {N}}\) a trace. Then \(v,i\vdash ^+_\sigma \alpha \longleftrightarrow v,i\vDash _\sigma \alpha \) and \(v,i\vdash ^-_\sigma \alpha \longleftrightarrow v,i\nvDash _\sigma \alpha \).

We have formalized and verified this result in Isabelle/HOL.

Example 1

Consider the standard publish–approve example [14] requiring that any file f published by an author a, must first be approved by a manager m of a within the previous seven days. The formalization of this policy as a closed MFOTL formula is:

$$ \varphi = \forall a.\; \forall f. \; \textsf{publish}(a,f) \rightarrow \left( \blacklozenge _{[0,7]} \exists m.\ \left( \lnot \mathsf {mgr_F}(m,a)\mathrel {\mathcal {S}_{}} \mathsf {mgr_S}(m,a)\right) \wedge \textsf{approve}(m,f)\right) \text {.} $$

Here, the events \(\mathsf {mgr_S}(m,a)\) and \(\mathsf {mgr_F}(m,a)\) mark m starting and finishing being a’s manager. Formally, m is currently a manager of a if m started being a’s manager in the past and has not finished being a’s manager since. Thus, the manager relation changes over time. Consider the stream \(\left\langle \tau _i,\varGamma _i\right\rangle _{i\in \mathbb {N}}\), where \(\tau _0=\tau _1=0\), \(\tau _2=4\), \(\tau _3=10\), and

$$ \begin{aligned} \varGamma _0 = & \{\mathsf {mgr_S}(\texttt {Mallory},\texttt {Alice}), \mathsf {mgr_S}(\texttt {Merlin},\texttt {Bob}), \mathsf {mgr_S}(\texttt {Merlin},\texttt {Charlie})\},\text { and }\\ \varGamma _1 = &\{\textsf{approve}(\texttt {Mallory},\texttt {152})\},\text { and }\\ \varGamma _2 = &\{\textsf{approve}(\texttt {Merlin}, \texttt {163}), \textsf{publish}(\texttt {Alice},\texttt {160}), \mathsf {mgr_F}(\texttt {Merlin},\texttt {Charlie})\},\text { and }\\ \varGamma _3 = &\{\textsf{approve}(\texttt {Merlin},\texttt {187}), \textsf{publish}(\texttt {Bob},\texttt {163}), \textsf{publish}(\texttt {Alice},\texttt {163}), \\ &\textsf{publish}(\texttt {Charlie},\texttt {163}),\textsf{publish}(\texttt {Charlie},\texttt {152})\}. \end{aligned} $$

In the following we abbreviate the subformulas of \(\varphi \) as follows: \(\varphi _L = \textsf{publish}(a,f)\), \(\varphi _1 =\lnot \mathsf {mgr_F}(m,a)\mathrel {\mathcal {S}_{}} \mathsf {mgr_S}(m,a)\), \(\varphi _2 = \textsf{approve}(m,f)\), \(\varphi _\exists = \exists m.\ \varphi _1\wedge \varphi _2\), \(\varphi _R = \blacklozenge _{[0,7]}\,\varphi _\exists \), and \(\varphi ' = \varphi _L \rightarrow \varphi _R\). The following proof tree shows that \(\varphi \) is violated at time-point 3 for any v:

figure c

Given \(\varphi _R\)’s temporal constraint, we note that \(\tau _3\ge 0\) and need to check \(v,i\vdash ^-\varphi _\exists \) for the time-points \(i \in \{2,3\}\) (as \([\textsf{E}_{3}^{\text {p}}([0,7]),\textsf{L}_{3}^{\text {p}}([0,7])] = \{2,3\}\)). Both subproofs are identical, so we parameterize them over i. In addition, the \( \exists {}^{-} \) subproofs are valid for an arbitrary manager \(d \in \mathbb {D}\) (abbreviating infinite branching over all possible domain values).    \(\square \)

Fig. 3.
figure 3

Grammar for our proof objects.

Full size image

3 Proof Object Checker

This section introduces our proof objects and their checker: finite data-representations of our proof system’s trees, and an algorithm that certifies if a given proof object faithfully proves the satisfaction or violation of a formula under a given assignment and stream. We discuss the soundness, completeness, and executability of these constructions.

To algorithmically manipulate proof trees, we define an explicit representation of satisfactions \(\mathfrak {sp}\) and violations \(\mathfrak {vp}\) via the grammar in Figure 3, where each constructor corresponds to a proof rule of our proof system (Figure 2), and its arguments represent subproofs and parameters that are part of a rule. The disjoint union \(\mathfrak {p}= \mathfrak {sp}\uplus \mathfrak {vp}\) is our type of proof objects. The proof object \(\forall ^+\) requires information about satisfactions for all domain elements \(d\in \mathbb {D}\) which we finitely represent with our valued partitions \(P\in \biguplus _{\mathbb {D}}({\mathfrak {sp}})\). Recall that a partition P of a set A is a collection of non-empty, pair-wise disjoint subsets of A that cover A. That is, \(D_i \cap D_j = \varnothing \) for \(D_i,\,D_j\in P\) with \(D_i\ne D_j\) and \(\bigcup P=A\). Partitions enable us to finitely represent all elements of the domain using finitely many finite sets and the co-finite complement of their union. In valued partitions \(P\in \biguplus _{\mathbb {D}}({\mathfrak {sp}})\), each set in the partition is tagged with a satisfaction explaining why its elements satisfy the argument of a universally quantified formula. Formally, our valued partitions \(P\in \biguplus _{\mathbb {D}}({Z})\) are lists of pairs of a set \(D_i\) and a value \(z\in Z\) from a given set Z such that the sets \(D_i\) form a partition of \(\mathbb {D}\). Similarly, \(\exists ^-\) stores a valued partition \(P\in \biguplus _{\mathbb {D}}({\mathfrak {vp}})\) of violations.

Our proof objects \(p\in \mathfrak {p}\) represent satisfactions or violations at a certain time-point. We define a function \(\textsf{tp}(p)\) (omitted) to compute this time-point. Either this information can be obtained recursively (e.g., \(\textsf{tp}( \Circle _{}^{+} (p))=\textsf{tp}(p)-1\)) or, in cases where it cannot, it is stored directly in the proof objects (e.g., \(\textsf{tp}( tt ^+(i))=i\)). We lift \(\textsf{tp}\) to sequences (yielding sequences of time-points) and valued partitions as \(\textsf{tp}(P) = \textsf{tp}(p_1)\), where \((D_1, p_1)\) is the partition P’s first entry. To characterize valid proof objects, we define the relation \(\vdash _\sigma \) ( Figure 4) that checks that proof objects constitute correct applications of our proof system’s rules. Here, \(\vdash \) is not an executable algorithm yet since the proof objects \(\forall ^+\) and \(\exists ^-\) require a recursive call for each element of each set in the partition, and at least one of such sets is infinite for infinite domains. We will improve on this aspect after an example.

Example 2

The following violation proof object p at time-point 3 (i.e., \(\textsf{tp}(p) = 3\)) is valid for formula \(\varphi \) on stream \(\sigma \) from Example 1 (i.e., \(v, p \vdash _\sigma \varphi \) for any assignment v):

$$\begin{array}{@{}lcl@{}} p &{}=&{} \forall ^- (a,\texttt {Charlie}, \forall ^- (f,\texttt {152},p_\rightarrow ^-)),\ \text {where}\\ p_\rightarrow ^- &{}=&{} \rightarrow ^- (p_L^+,p_{\blacklozenge _{}}^-),\ p_L^+ = p^+ (3,\textsf{publish},[a,f]),\\ p_{\blacklozenge _{}}^- &{}=&{} \blacklozenge _{}^{-} (3,[ \exists ^- (x,[\left( \mathbb {D},p^-_{2}\right) ]), \exists ^- (x,[\left( \mathbb {D},p^-_{3}\right) ])]),\, \text {and}\\ p^-_{i} &{}=&{} \wedge ^{-}_{R} ( p^- (i,\textsf{approve},[m,f]))\ \text {for}\ i\in \{2,3\}. \end{array}$$
Fig. 4.
figure 4

Proof checker for a fixed stream \(\sigma = \left\langle \tau _i,\varGamma _i\right\rangle _{i\in \mathbb {N}}\).

Full size image

Indeed, we use the definition in Figure 4 to certify that \(v,p \vdash _\sigma \varphi \):

$$\begin{array}{@{}lcl@{}} v,p\vdash \varphi \ {} &{}\text {iff}&{} v[a\mapsto \texttt {Charlie}], \forall ^- (f,\texttt {152},p_\rightarrow ^-)\vdash \forall f.\ \varphi _L\rightarrow \varphi _R\\ &{}\text {iff}&{}v[a\mapsto \texttt {Charlie}, f\mapsto \texttt {152}],p_\rightarrow ^-\vdash \varphi _L\rightarrow \varphi _R\\ &{}\text {iff}&{}v[a\mapsto \texttt {Charlie}, f\mapsto \texttt {152}],p_L^+\vdash \varphi _L \text { and }\textsf{tp}(p_L^+)=3=\textsf{tp}(p_{\blacklozenge _{}}^-)\text { and }\\ &{}&{}v[a\mapsto \texttt {Charlie}, f\mapsto \texttt {152}],p_{\blacklozenge _{}}^-\vdash \varphi _R\\ &{}\text {iff}&{} v[a\mapsto \texttt {Charlie}, f\mapsto \texttt {152}], \exists ^- (x,[\left( \mathbb {D},p^-_{i}\right) ])\vdash \varphi _\exists \ \texttt {for}\ i\in \{2,3\}\\ &{}\text {iff}&{} v[a\mapsto \texttt {Charlie}, f\mapsto \texttt {152}, x\mapsto d],p^-_{i}\vdash \varphi _1\wedge \varphi _2\ \text {for all}\ d\in \mathbb {D},\,i\in \{2,3\}\\ &{}\text {iff}&{} \textsf{approve}(\texttt {d},\texttt {152})\notin \varGamma _i\ \text {for all}\ d\in \mathbb {D},\,i\in \{2,3\},\text { which is true}. \end{array}$$
Fig. 5.
figure 5

The formula’s latest relevant time-point at i for a fixed stream \(\sigma = \left\langle \tau _i,\varGamma _i\right\rangle _{i\in \mathbb {N}}\).

Full size image

We implicitly use in the above the true statements \(\textsf{publish}(\texttt {Charlie},\texttt {152})\in \varGamma _3\), \(0\le \tau _3\), and \(\textsf{tp}( [ \exists ^- (x,[\left( \mathbb {D},p^-_{2}\right) ]), \exists ^- (x,[\left( \mathbb {D},p^-_{3}\right) ])])=[2,3]=[\textsf{E}_{i}^{\text {p}}(I),\textsf{L}_{i}^{\text {p}}(I)]\).    \(\square \)

Theorem 2

Fix a stream \(\sigma \). The relation \(\vdash \) is sound and complete in the sense that \(v,i\vDash \alpha \) iff there is a satisfaction \( sp \) such that \(v, sp \vdash \alpha \) and \(\textsf{tp}( sp )=i\). Similarly \(v,i\nvDash \alpha \) iff there is a violation \( vp \) such that \(v, vp \vdash \alpha \) and \(\textsf{tp}( vp )=i\).

We have established the above result in Isabelle. Below we sketch our overall approach and highlight the main challenge. We show both soundness and completeness by relating proof object validity (\(\vdash \)) to the proof system (\(\vdash ^+\) and \(\vdash ^-\)), which we already know to be sound and complete, i.e., related to the semantics \(\vDash \). Soundness is easy as the proof object directly provides the recipe for correctly applying the proof system rules. Formally, if \(v, sp \vdash \alpha \) then \(v,\textsf{tp}( sp ) \vdash ^+\alpha \), and if \(v, vp \vdash \alpha \), then \(v,\textsf{tp}( vp )\vdash ^-\alpha \). The proof follows immediately by mutual induction on the proof object structure.

Completeness of \(\vdash \) requires us to provide a valid proof object just from knowing \(v, i \vdash ^+ \alpha \) or \(v, i \vdash ^- \alpha \). We proceed by mutual induction on the derivations of \(\vdash ^+\) and \(\vdash ^-\). Only two of the quantifier cases are challenging. For the satisfaction of the universal quantifier (and similarly for the violation of \(\exists \)), we must construct a valued partition with finitely many subproofs. However, the induction hypothesis yields a separate proof object for every element of the domain \(\mathbb {D}\), and all these proof objects may a priori be different. The crucial observation is that for all values that do not occur in the stream (or at least are not in reach of \(\alpha \) with respect to a time-point i) we can reuse the same proof object. To formalize this observation, we first define a formula’s active domain at i, written \(\textsf{AD}_i(\alpha )\), which formalizes the in “reach” intuition. To this end, we first define the latest relevant time point (\(\textsf{LRTP}\; i\; \alpha \)) of \(\alpha \) at i (Figure 5). Intuitively, \(\textsf{LRTP}\; i\; \alpha \) marks the largest time-point that may influence \(\alpha \)’s satisfiability at i. It exists, because we assume that future temporal operators have bounded intervals. Based on this, we define:

$$\begin{aligned} \textsf{AD}_i(\alpha ) = \mathbb {D}(\alpha ) \cup \bigcup \nolimits _{k\le \textsf{LRTP}\; i\; \alpha }\{d\mid d\text { appears in some }\textsf{p}(d_1,\dots ,d_n)\in \varGamma _k\}. \end{aligned}$$

Here we write \(\mathbb {D}(\alpha )\) for the set of constants \(d \in \mathbb {D}\) occurring in subformulas of the form \(x \approx d\) in \(\alpha \). (In contrast to constants occurring in atomic predicates, constants occurring in equalities may appear in \(\alpha \)’s satisfying assignments even if they are not part of the trace.) Note that \(\textsf{AD}_i(\alpha )\) is finite. The active domain lets us formalize the key observation:

Lemma 1

Fix a stream \(\sigma \), a formula \(\alpha \), a proof p, and two assignments v and \(v'\). Let \(i = \textsf{tp}(p)\), \(\textsf{AD}= \textsf{AD}_i(\alpha )\), and V be the set of \(\alpha \)’s free variables. Assume that v and \(v'\) may only disagree on V for values outside of the active domain at i, i.e.,

$$\begin{aligned} \forall x \in V.\;v(x) = v'(x) \vee (v(x) \notin \textsf{AD}\wedge v'(x) \notin \textsf{AD})\text {.} \end{aligned}$$

Then, p’s validity status is the same for both assignments, i.e., \(v,p\vdash \alpha \) iff \(v',p\vdash \alpha \).

We now can finish the \( \forall {}^{+} \) case of the completeness proof. By the induction hypothesis, there is a satisfaction \(p(d)\in \mathfrak {sp}\) for each domain element \(d \in \mathbb {D}\). Moreover, \(\{\{d\}\mid d\in \textsf{AD}_i(\alpha )\}\cup \{\mathbb {D}\setminus \textsf{AD}_i(\alpha )\}\) is a finite partition of \(\mathbb {D}\). Hence, the list of pairings \((\{d\}, p(d))\) for each \(d\in \textsf{AD}_i(\alpha )\) and \((\mathbb {D}\setminus \textsf{AD}_i(\alpha ),p(z))\) for some \(z\in \mathbb {D}\setminus \textsf{AD}_i(\alpha )\) (which exists as \(\mathbb {D}\) is infinite) is a valued partition. Moreover, all subproofs are valid for all the values contained in the partition sets by combining the induction hypothesis with the above congruence Lemma 1 (for \(p = p(z)\)), and thus so is the overall \(\forall ^+\) proof object.

Lastly, we address the executability issue. The validity relation \(\vdash \) works with assignments v of values to variables. To avoid performing infinitely many recursive calls for the \(\forall ^+\) and \(\exists ^-\) proof objects we now will work with set assignments V of sets of values to variables. We define a validity relation \(V, p \vdash \alpha \) based on set assignments. The definition is the same as the one of \(v, p \vdash \alpha \) except for the predicate and the quantifier cases:

$$ \begin{array}{@{}lcl@{}} V,\, p^+ (i,\textsf{p},\overline{t}) \vdash \textsf{p}(\overline{t})&{}\text {iff}&{} \{\textsf{p}\}\times \llbracket \overline{t}\rrbracket _V\subseteq \varGamma _i\\ V,\, p^- (i,\textsf{p},\overline{t}) \vdash \textsf{p}(\overline{t})&{}\text {iff}&{} \{\textsf{p}\}\times \llbracket \overline{t}\rrbracket _V\subseteq \mathbb {D}\setminus \varGamma _i\\ V,\, \forall ^+ (x,P) \vdash \forall x.\ \alpha &{}\ \text {iff}&{}\ \bigwedge (D_k, sp _k)\in P.\; \textsf{tp}( sp _k){=}\textsf{tp}(P)\text { and }V[x\mapsto D_k],\, sp _k\vdash \alpha \\ V,\, \exists ^+ (x,d, sp ) \vdash \exists x.\ \alpha &{}\ \text {iff}&{} V[x\mapsto \{d\}],\, sp \vdash \alpha \end{array} $$

and dually for \(\exists ^-\) and \(\forall ^-\). Here, \(\llbracket \overline{t}\rrbracket _V\) represents a transformation of the list of values \(\llbracket \overline{t}\rrbracket _v\) to the set of all possible lists of values generated by V. Set assignments allow us to delay deciding values for quantifier subproofs to the predicate base case. Note that \(\{\textsf{p}\}\times \llbracket \overline{t}\rrbracket _V\subseteq \varGamma _i\) and \(\{\textsf{p}\}\times \llbracket \overline{t}\rrbracket _V\subseteq \mathbb {D}\setminus \varGamma _i\) are decidable because due to our partitions, we only encounter finite and co-finite sets. The set-assignment-based validity check is thus executable and thus provides the algorithm that we use as our formally verified proof object checker: \(v, p \vdash \alpha = (\lambda x. \{v(x)\}), p \vdash \alpha \) (proved by induction on \(\alpha \) using Lemma 1).

4 Partitioned Decision Trees

Our proof system is parameterized with an assignment, but in our monitoring approach we are interested in computing a proof object for every assignment. In this section, we introduce partitioned decision trees (PDTs), a specialized data structure for representing and efficiently manipulating variable assignments, inspired by the use of BDDs in runtime verification [17]. We want to represent functions of the form \(f:\mathbb {D}\times \ldots \times \mathbb {D}\rightarrow \mathfrak {p}\), i.e., mappings from tuples of domain elements to proof trees, where each tuple corresponds to a variable assignment to the formula’s free variables. As argued in the previous section, we are only interested in such functions with a finite range. Thus, we organize the domain into a finite number of subsets \(\mathbb {D}\times \ldots \times \mathbb {D}\) such that each tuple element is partitioned separately (using valued partitions over the domain). As before, we work with finite and co-finite sets in the partition. PDTs \(\mathbb {P}(A)\) are defined inductively as follows:

$$\mathbb {P}(A) = \textsf{Leaf}\;\,A \mid \textsf{Node}\;(\mathbb {V}, \biguplus \nolimits _\mathbb {D}(\mathbb {P}(A))) $$
Fig. 6.
figure 6

Resulting PDT for our running example at time-point 3.

Full size image

PDTs have leaves and nodes. Leaves store objects from the set A, while nodes store pairs of the form (x, P), where x is a variable and P, a valued partition of the domain storing PDTs. PDTs generalize binary decision trees along two dimensions. First, the branching of their nodes is not binary but follows a given partition of the infinite domain \(\mathbb {D}\). Second, their leaves do not store Boolean values. Instead, they store arbitrary objects, even though we will mostly use them with proof objects \(A = \mathfrak {p}\). PDTs provide a way to organize the infinitely many possible variable assignments in a structured manner, storing only finitely many different proof objects. In monitoring, partitions will arise naturally, guided by the values occurring in the stream and assembled via operations that combine them.

Fig. 7.
figure 7

Proof tree \(\blacktriangle ^+\).

Full size image

Example 3

We continue the publish–approve example from Example 1. We consider the same stream but drop the top-level quantifiers from the formula \(\varphi \): we only consider \(\varphi '\) with its free variables a and f. Figure 6 shows the PDT representing all assignments for \(\varphi '\) at time-point 3. The root node represents variable a, and the edges partition the values that a can take into the following domain subsets: \(\{\texttt {Alice}\}, \{\texttt {Bob}\}, \{\texttt {Charlie}\}\), and \(\mathbb {D}\setminus \{\texttt {Alice}, \texttt {Bob}, \texttt {Charlie}\}\). The second level is analogous for variable f. At every level of the PDT, the union of all choices cover the entire domain \(\mathbb {D}\) (by definition of partitions) and the partitions may differ at every node. The leaves of the PDT are different proof trees (formally, proof objects) which we represent by small black triangles. For example, \(\blacktriangle _3^-\) is the proof tree of \(\varphi '\)’s violation shown in Example 1. In contrast, \(\blacktriangle ^+\) (occurring in multiple leaves) is the proof tree shown in Figure 7 of \(\varphi '\)’s vacuous satisfaction: the left hand side of the implication (\(\textsf{publish}(a,f)\)) is violated for any assignment v updated by following the path from the PDT’s root to the respective leaf (e.g., taking \(a = \texttt {Alice}\) and \(f = \texttt {42} \in \mathbb {D}\setminus \{\texttt {163}\}\)).   \(\square \)

Since PDTs are a generalization of BDDs, we use similar functions to manipulate them. We list the most important ones, for partitions and PDTs in Figure 8, but we only show and discuss the implementation of \(\textsf{apply2}\), \(\textsf{merge2}\), and \(\textsf{hide}\). Most PDT-functions are parameterized by a variable list \(\mathord { vs } {:}{:} \overline{\mathbb {V}}\) fixing the variable order. The functions \(\mathsf {map\_part}\) and \(\textsf{apply1}\) lift unary functions on objects to partitions and PDTs respectively.

The functions \(\textsf{merge2}\) and \(\textsf{apply2}\) do the same for binary functions; \(\textsf{apply2}\) generalizes the well-known \(\textsf{apply}\) function on BDDs [16]. On leaves, \(\textsf{apply2}\) maps f to the objects. When operating on a leaf and a node, \(\textsf{apply2}\) pushes f partially applied to the leaf to the node’s leaves using \(\textsf{apply1}\). Finally, on pairs of nodes, it proceeds recursively depending which of \(\mathord { x }\), \(\mathord { y }\), and \(\mathord { z }\) are equal. The most interesting case, \(\mathord { x }=\mathord { y }=\mathord { z }\) occurs when both PDTs partition the domain values for \(\mathord { z }\) in different ways. Thus, we must combine both partitions. For this, we use \(\textsf{merge2}\) that takes two valued partitions \(P_1\) and \(P_2\), and iteratively “erodes” \(P_2\) by intersecting its elements with the sets in \(P_1\) while applying f. Since both \(P_1\) and \(P_2\) cover \(\mathbb {D}\), the resulting set of intersections is a valued partition. The function \(\textsf{apply3}\) analogously combines three PDTs into one.

Fig. 8.
figure 8

Selected functions on partitions and PDTs.

Full size image

The function \(\textsf{hide}\) traverses the PDT similarly to \(\textsf{apply1}\), while eliminating the last variable in the given variable list. It uses two higher-order arguments, in case the last layer is present (\(\mathord { node }\)) or absent (\(\mathord { leaf }\)). The function \(\mathsf {pdt\_of}\;\mathord { vs }\;\mathord { A }\;\mathord { B }\;\mathord { V }\) constructs a PDT from a finite set of partial assignments (\(V {:}{:} 2^{(\mathbb {V} \rightharpoonup \mathbb {D})}\)) using \(\mathord { A }\) for leaves reached by paths from the set, and \(\mathord { B }\) for the other leaves. Finally, the \(\mathsf {split\_*}\) functions transpose a PDT storing pairs (lists of equal length) into a pair (list) of PDTs.

5 Monitoring Algorithm

We follow the typical online monitoring algorithm structure consisting of an initialization and a step (evaluation) function [25, 30]. The initializer \(\textsf{init}\) (omitted as standard) computes our monitor’s initial state \(s\in \mathbb {S}\) from an MFOTL specification \(\alpha \). Figure 9 shows an excerpt of our monitor’s state, which recursively follows the formula structure and augments some operators with additional information, such as buffers storing verdicts from subformulas (\(\mathbb {B}_2\) for \(\wedge \) and \(\mathbb {B}_3\) for \(\mathrel {\mathcal {S}_{}}\)) or an operator-specific state (\(\mathbb {S}_ {saux} \) for \(\mathrel {\mathcal {S}_{}}\)).

Fig. 9.
figure 9

Involved types and selected cases of the monitor’s \(\textsf{eval}\) function

Full size image
Fig. 10.
figure 10

Functions \(\mathsf {do\_exists\_leaf}\) and \(\mathsf {do\_exists\_node}\).

Full size image

Our function \(\textsf{eval}\), partly shown in Figure 9, takes as inputs a new time-point i (along with its time-stamp \(\tau \) and database \(\varGamma \)) and a monitor state s and outputs the next state \(s'\) and a list of PDTs of proof objects as verdicts. (In addition, \(\textsf{eval}\) keeps track of the variable ordering used in PDTs via the parameter \(\mathord { vs }\).) Lists in the output are necessary because delays may occur for (bounded) future operators and a single time-point might trigger multiple outputs. Our algorithm extends Lima et al.’s algorithm [25] computing proof trees for MTL. We highlight our key additions to \(\textsf{eval}\) and the state Figure 9 in gray.

We focus on the predicate, conjunction, existential quantifier, and since cases. In the predicate case, we find all partial assignments \(\sigma \) mapping the predicate’s variables to the values \(\mathord { ds }\), so that \(\textsf{p}(\mathord { ds })\in \varGamma \). We reuse VeriMon’s \(\textsf{match}\) function [30] to compute such partial assignments. We convert this set of assignments to a PDT using \(\mathsf {pdt\_of}\). In the resulting PDT, matching assignments lead to leaves using the satisfaction proof \( p^+ (\mathord { i },\mathord { \textsf{p} },\mathord { ts })\), whereas the others lead to the corresponding violation proof \( p^- (\mathord { i },\mathord { \textsf{p} },\mathord { ts })\).

The conjunction case is taken almost without changes from Lima et al.’s [25] MTL algorithm. We reuse the buffering functions \(\mathsf {buf2\_add}\) and \(\mathsf {buf2\_take}\). The first adds partial results to the buffer, while the second combines these results and dequeues them once both subformulas have produced results for a time-point. The only difference is that our buffers store PDTs of proof objects, whereas the MTL algorithm works with propositional proof objects. Accordingly, we reuse the Lima et al.’s function \(\mathsf {do\_and} {:}{:} \mathfrak {p}\Rightarrow \mathfrak {p}\Rightarrow \mathfrak {p}\) to combine two proof objects conjunctively, but lift it to PDTs using \(\textsf{apply2}\).

The quantifier cases are a new addition of our work. As both cases proceed dually, we focus on \(\exists x.\,\alpha \) formulas. Considering that \(\alpha \) may have one more free variable than \(\exists x.\,\alpha \), the recursive call appends x to the variable list ordering. The recursive call’s output is processed using our function \(\textsf{hide}\) to eliminate the quantified variable. The interesting cases occur near the leaves of \(\alpha \)’s PDTs. If x is not present, \(\textsf{hide}\) will encounter a leaf, i.e., a proof object, and use the function \(\mathsf {do\_exists\_leaf}\) (Figure 10) to perform a case distinction: satisfactions result in a satisfaction (\(\mathfrak {sp}\)) of \(\exists x.\, \alpha \) with an arbitrary element d of the domain as the witness (we write \(x \leftarrow X\) to denote an arbitrarily chosen element x of a non-empty set X); violations result in a violation (\(\mathfrak {vp}\)) with the trivial partition. If x is present as the last decision node, then \(\textsf{hide}\) will use \(\mathsf {do\_exists\_node}\) (Figure 10) to construct the proof object for \(\exists x.\,\alpha \). It performs a case distinction whether a satisfaction proof is contained in the partition of this last node. If it is, \(\exists x.\, \alpha \) is satisfied and we compute the smallest (in proof size) such satisfaction proof, taking as our witness an arbitrary element of the respective partition set. Otherwise, all leaves are violations and we obtain a violation proof of \(\exists x.\,\alpha \).

To reuse Lima et al.’s [25] temporal operator evaluation, our state stores a PDT whose leaves are the auxiliary state of these algorithms (instead of proof objects). This allows us to keep the complex auxiliary state and its update unchanged. For example, we use \(\textsf{apply3}\) to lift Lima et al.’s [25] \(\mathsf {update\_since}\) function to two PDTs storing proof objects for subformulas and a third one storing the auxiliary state. The resulting PDT has type \(\mathbb {P}(\mathbb {S}_{\mathord { saux }} \times \overline{\mathfrak {p}})\), which we transpose into the desired \(\mathbb {P}(\mathbb {S}_{\mathord { saux }}) \times \overline{\mathbb {P}(\mathfrak {p})}\) using \(\mathsf {split\_prod}\) and \(\mathsf {split\_list}\).

6 Implementation and Case Study

We implement our algorithm in a new monitoring tool, called WhyMon [2]. Our implementation consists of \(4\,500\) lines of OCaml code and incorporates an optimization of collapsing partition sets with the same stored values both in proof objects and in PDTs. Our formally verified checker contributes additional \(1\,700\) lines of OCaml code generated from our Isabelle formalization, which itself comprises \(6\,400\) lines of definitions and proofs. The checker’s main function lifts the validity check of proof objects (\(\vdash \)) to PDTs, i.e., \(\textsf {check}: \textit{trace} \rightarrow \textit{formula} \rightarrow \textit{pdt} \rightarrow \textit{bool}\), and is used to certify WhyMon’s output. WhyMon includes a visualization [3] implemented in React [20] that consists of \(2\,400\) lines of JavaScript and invokes a JavaScript version of our monitor, generated by Js_of_ocaml [32]. Here, we consider the data race policy [18] that captures possible concurrency issues in multithreaded programs on a stream prefix generated by Raszyk [27, Section 4.3]. Furthermore, we consider Nokia’s Data-collection Campaign [4], which comes with a stream prefix of around 5 million time-points [1], for which we focus on the del-2-3 policy [12] controlling data propagation between databases. We describe a violation for each scenario highlighting the advantages of our approach.

Example 4

We first return to Example 3 in our visualization tool, depicted in Figure 11. The table includes TP (time-points), TS (time-stamps), and Values columns. The following columns show the topmost operator of \(\varphi '\)’s subformulas or its predicate names (and their variables). In the Values column, for each of the already evaluated time-points, there is an associated button enclosing a (for satisfactions), or a (for violations) or both. After clicking on this button, we are presented with a dropdown menu (as in  Figure 12) that corresponds to a partition. The listed values are the (potentially multiple) variable assignments of the resulting PDT for that specific time-point. The formula \(\varphi '\) contains two free variables, a and f, and to single out a verdict we must select one value for each. In particular, at time-point 3 we select \(a = \texttt {Charlie}\) and \(f = \texttt {152}\). Note that in the visualization we focus on readability and omit set parentheses. Moreover, Other denotes the complement of the listed values. After choosing the assignments, a Boolean verdict appears in the next column matching the topmost operator of \(\varphi '\), namely \(\rightarrow \). Clicking on this Boolean verdict reveals and highlights the Boolean verdicts associated with its justification. The subformulas’ columns of the current inspection are also highlighted. In this case, the implication is violated because the left side is satisfied, while the \(\blacklozenge _{[0,7]}\) subformula is violated. We can explore this verdict further: the violation is justified by those of its subformula at time-points 2 and 3 (the time-points inside the interval are also highlighted). For each time-point, there is another dropdown menu where we can select an assignment for m. Here, the only listed value is Any, which corresponds to \(\mathbb {D}\). Thus, the existential quantifier is violated because the subformula \(\textsf {approve}( m , \texttt {152})\) is violated for all values that m can be assigned to (\(\mathbb {D}\)), and all justifications are identical.

Data Race Detection Multithreaded programs are pervasive and hard to debug. In particular, they are prone to data races, which occur when two threads access (\(\textsf {read}\) or \(\textsf {write}\) to) a shared address concurrently and at least one of these accesses is a \(\textsf {write}\). Locking mechanisms that synchronize access to variables shared between threads are a plausible solution. We consider the following policy to detect data race potentials[18]:

$$ \begin{array}{@{}lcl@{}} \varphi _{dr} &{}=&{} \textsf {datarace}(t_1, t_2, x) \rightarrow \exists l. (\textsf {acqnrel}(t_1, x, l) \wedge \textsf {acqnrel}(t_2, x, l)),\text { with }\\ \textsf {datarace}(t_1, t_2, x) &{}=&{} \blacklozenge _{} \left( \textsf {read}\left( t_1, x\right) \vee \textsf {write}\left( t_1 x\right) \right) \wedge \blacklozenge _{} \textsf {write}\left( t_2, x\right) ,\text { and }\\ \textsf {acqnrel}(t, x, l) &{}=&{} \blacksquare _{} \left( \left( \textsf {read}\left( t, x\right) \vee \textsf {write}\left( t, x\right) \right) \rightarrow \left( \lnot \textsf {rel}\left( t, l\right) \mathrel {\mathcal {S}_{}} \textsf {acq}\left( t, l\right) \right) \right) \end{array} $$

where the predicates \(\textsf {read}(t, x)\) and \(\textsf {write}(t, x)\) specify read and write operations performed by thread t to shared address x, and \(\textsf {acq}(t, l)\) and \(\textsf {rel}(t, l)\) specify the acquisition and the release of lock l by thread t. Havelund et al. [18] consider a closed formula variant of this policy as their tool, DejaVu, only supports closed formulas. In contrast, WhyMon supports open formulas. We consider the stream prefix:

$$\begin{aligned} {} & {} \langle (0, \{\textsf {acq}(\texttt {9},\texttt {9})\}), (1, \{\textsf {read}(\texttt {9},\texttt {3})\}), (2, \{\textsf {acq}(\texttt {13},\texttt {19})\}), (3, \{\textsf {acq}(\texttt {15},\texttt {3})\}), \\ {} & {} \,\, (4, \{\textsf {acq}(\texttt {18}, \texttt {15})\}),(5, \{\textsf {read}(\texttt {13},\texttt {5})\}),(6, \{\textsf {write}(\texttt {15},\texttt {4})\}),(7, \{\textsf {write}(\texttt {15},\texttt {3})\}), \ldots \rangle \end{aligned}$$

At time-point 7, WhyMon outputs a PDT with non-trivial assignments. We focus on the single violation in this PDT, which corresponds to the assignment \((\{\texttt {9}\}, \{\texttt {15}\}, \{\texttt {3}\})\) for (\(t_1\), \(t_2\), x). This violation is shown in Figure 13. The topmost operator of \(\varphi _{dr}\) is an implication, and it is violated because the left side is satisfied (there was a data race), while the right side (the lock requirement) is violated. Specifically, the data race occurred because thread \(t_1 = 9\) read address 3 at time-point 1, satisfying the \(\blacklozenge _{[0, \infty )}\) subformula in the left conjunct, and thread \(t_2 = 15\) wrote to address 3 at the current time-point 7, satisfying the \(\blacklozenge _{[0, \infty )}\) subformula in the right conjunct. Moving to the right side of the implication, the violation of the existential indicates that its subformula is violated for every value of \(\mathbb {D}\). In particular, the subsets of the domain \(\{9\}\) and \(\{9\}^\textsf{C}\) are each associated with a different violation. Here, we focus on the violation where \(l = 9\). The subformula is a conjunction, and to be violated it suffices that one of the conjuncts is violated. This violation stems from the violation of the right conjunct \(\blacksquare _{[0, \infty )}\) (note that \(t_2 = 15\) is listed as the variable in the predicate columns). We omit the columns referring to the left conjunct, since all entries are empty. Once again, the implication is violated because the left side is satisfied, i.e., thread \(t_2 = 15\) wrote to address 3 at time-point 7, satisfying the disjunction, but \(\mathrel {\mathcal {S}_{[0,\infty )}}\) on the right side is violated, because thread \(t_2 = 15\) never acquired the lock \(l = 9\).

Fig. 11.
figure 11

Visualization of \(\varphi '\)’s violation at time-point 3 for \((\{\texttt {Charlie}\}, \{\texttt {152}\})\).

Full size image
Fig. 12.
figure 12

Assignment selection for \(\varphi '\) at time-point 3.

Full size image
Fig. 13.
figure 13

Visualization of \(\varphi _{dr}\)’s violation at time-point 7 for \((\{\texttt {9}\}, \{\texttt {15}\}, \{\texttt {3}\})\).

Full size image
Fig. 14.
figure 14

Visualization of \(\varphi _{del}\)’s violation at time-point 79 for \((\{\texttt {189810327}\}, \{\texttt {user2}\}, \{\texttt {[unknown]}\})\).

Full size image

Data Propagation Nokia’s Data-collection Campaign [4] used three databases \(\texttt {db}_1\), \(\texttt {db}_2\) and \(\texttt {db}_3\) in the collection of sensitive information from mobile phones of participants. We focus on the policy \(\varphi _{del}\) [12], which controls the data propagation between databases \(\texttt {db}_2\) and \(\texttt {db}_3\): if \( data \) is deleted from \(\texttt {db}_2\), then it must be deleted from \(\texttt {db}_3\) within 1 minute.

$$ \varphi _{del} = \textsf {delete}\left( x, \texttt {db}_2, y, data\right) \wedge data \not \approx \texttt {[unknown]} \rightarrow \lozenge _{[0,60]} \exists u, v.\; \textsf {delete}\left( u, \texttt {db}_3, v, data \right) $$

where \(\texttt {db}_2\), \(\texttt {db}_3\), and \(\texttt {[unknown]}\) are constants and \(\textsf {delete}(db_{user}, db , p_{id}, data )\) specifies the deletion of data from participant \(p_{id}\) from database db using database user \(db_{user}\). We used the replayer tool [22] to convert the stream prefix to WhyMon’s format. We executed WhyMon’s command line interface with the entire prefix and found two violations. The following experiments were conducted on a computer with an Apple M1 Chip (8 cores) and 16GB of RAM. WhyMon took 17m51s to process the entire prefix. We also executed MonPoly with a slightly modified yet equivalent policy (due to monitorability restrictions), and its running time amounted to 1m10s. MonPoly outperforms WhyMon, but we must acknowledge the different outputs both monitors produce. MonPoly only outputs variable assignments, whereas WhyMon outputs entire PDTs containing all assignments and a justification of the verdict in the form of a proof tree for each. We extract 100 time-points containing both violations and focus on the violation at time-point 79 for the assignment \((\{\texttt {189810327}\}, \{\texttt {user2}\}, \{\texttt {[unknown]}\})\) for (\( data \),x,y), depicted in Figure 14. Time-stamps are converted to actual dates (by enabling the option) and we omit time-points that do not contain relevant events for the violation. Let

$$\begin{aligned} \varGamma _{79} =& \{\textsf {delete}(\texttt {user2},\texttt {db2},\texttt {[unknown]},\texttt {189810327}),\\ \varGamma _{80} =& \{\textsf {delete}(\texttt {triggers},\texttt {db3},\texttt {[unknown]},\texttt {[unknown]})\},\\ \varGamma _{81} =& \{\textsf {delete}(\texttt {user2},\texttt {db2}, \texttt {[unknown]},\texttt {189810328})\},\text { and }\varGamma _{82} = \varGamma _{83} = \varGamma _{84} = \varnothing . \end{aligned} $$

The implication is violated because the left side is satisfied (there was a deletion at the current time-point 79), but \(\lozenge _{[0,59]}\) is violated. Note that [0, 60) was replaced with the equivalent interval [0, 59]. For each time-point of \([\textsf{E}_{79}^{\text {f}}([0,59]),\textsf{L}_{79}^{\text {f}}([0,59])]=\{79, \ldots , 84\}\), the subformula is violated. Regardless of the values we assign to u and v (all violations are identical), the subformula \(\textsf {delete}\left( u, \texttt {db}_3, v, \texttt {189810327}\right) \) is violated.

7 Conclusion

We describe an approach for MFOTL monitoring with verdicts in the form of proof objects for every free variable assignment. Such verdicts are useful for understandability and certification, which increases the monitor’s trustworthiness. We implement our approach in the tool WhyMon along with an interactive visualization for these verdicts, which we invite the reader to explore [3]. As future work, we plan to provide support for equality between variables and to improve our monitor’s performance by, e.g., stream slicing [29].