Monitorability for the Modal Mu-Calculus over Systems with Data: From Practice to Theory

In formal methods, data words and trees constitute popular formalisms to model respectively the traces and possible executions of systems [51]. Since we consider linear-time properties, we model execution traces as data $\omega$-words. They consist in infinite words whose elements are pairs of a letter from a finite alphabet and of a data value from an infinite domain. The finite alphabet plays no role here and can be simulated, so we omit it for simplicity [49]. A data word is thus an infinite sequence of values from an infinite domain.

For the rest of the paper, we fix a countably infinite data domain $𝔻$, whose only predicate is “$=$” and is decidable. An action is modelled as a data value $d\in 𝔻$. An infinite (respectively, finite) trace is a data word, i.e., an infinite (resp., finite) sequence $t\in {𝔻}^{\omega }$ (resp., $w\in {𝔻}^n$ for some $n\in \mathbb{N}$); the set of all infinite traces is denoted $\text{Trc}={𝔻}^{\omega }$ (resp., $\text{FTrc}={𝔻}^{\ast }$ for finite traces). For $w=w_0\mathrm{\dots }{w}_n\in \text{FTrc}$ and $u=u_0{u}_1\mathrm{\cdots }\in \text{FTrc}\cup \text{Trc}$, the concatenation of $w$ and $u$ is $w\cdot u=w_0\mathrm{\dots }{w}_n{u}_0\mathrm{\dots }$ (we may omit the $\cdot$). When $u=y\cdot v$, $y$ is a prefix of $u$, and $v$ is a suffix of $u$. The set of suffixes of $u$ is denoted $\mathrm{𝚜𝚞𝚏𝚏𝚒𝚡}(u)$.

We define an extension of $\mu$HML, called $\mu {\text{HML}}^d$. Its syntax and semantics are described in Fig. 1 on page 1. Formulae are built from a countable set of formula variables, $X,Y\in \text{FVar}$, and data variables, $x,y\in \text{DVar}$, ranging over an infinite domain of data values, $d\in 𝔻$. In addition to the standard Boolean constructs, $\mu {\text{HML}}^d$ can express recursive properties as least ($\mathrm{𝗆𝗂𝗇}X.(\phi )$) and greatest ($\mathrm{𝗆𝖺𝗑}X.(\phi )$) fixed-point formulae that bind the free occurrences of $X$ in $\phi$. The logic includes the possibility ($⟨b⟩\phi$) and necessity ($[b]\phi$) modal constructs. To reason on the data carried by process actions, modalities are augmented with decidable, quantifier-free Boolean constraint expressions, $b,c\in \text{BExp}$, defined over $𝔻$ and $\text{DVar}\cup \{\star \}$, where $\star \notin \text{DVar}$ is a placeholder variable for the current action $d\in 𝔻$. The free data variables $x\in \text{DVar}$ that appear in $b$ are bound by existential and universal quantification constructs $\exists 𝒙.\phi$ and $\forall 𝒙.\phi$.

In what follows, the standard notions of open and closed expressions, free and bound variables, and formula equivalence up to alpha-conversion are used. We assume wlog that every occurrence of each fixed-point variable is within the scope of a modal operator in its defining fixed-point formula. This is the case e.g. of $\mathrm{𝗆𝖺𝗑}X.([b]X)$, but not of $\mathrm{𝗆𝖺𝗑}X.(X\wedge [b]X)$.

We define the domains $\text{DEnv}=\text{DVar}\rightharpoonup 𝔻$ of data environments, $\text{DInt}=\text{DEnv}\rightharpoonup 2^{\text{Trc}}$ of data interpretations, and $\text{TEnv}=\text{FVar}\rightharpoonup \text{DInt}$ of trace environments (where $A\rightharpoonup B$ denotes the set of partial functions from set $A$ to set $B$). A data environment, $\delta \in \text{DEnv}$, is a partial function with a finite domain mapping data variables to values from $𝔻$; analogously, a trace environment, $\rho \in \text{TEnv}$, maps formula variables to data interpretations $F,G\in \text{DInt}$, that given $\delta$, return a set of traces, whose intended meaning is the interpretation of the formula variable in the data environment $\delta$.

The linear-time semantics of $\mu {\text{HML}}^d$ is given by the denotational semantic function, $⟦-⟧$, defined inductively in Fig. 1. In $⟦-⟧$, formulae are interpreted w.r.t. a trace environment $\rho$ that gives meaning to formula variables, and a data environment $\delta$ that assigns values to data variables in Boolean constraint expressions. Expressions are of the form:

where $e,f\in \text{DVar}\bigsqcup \{\star \}$. An expression $b$ defines a set of external system actions. An action $d$ is in this set when the data value it carries satisfies $b$ with regards to the data environment $\delta$, i.e., $b\delta [\star \mapsto d]\Downarrow \mathrm{𝗍𝗋𝗎𝖾}$, where, for any function $f:A\to B$, any $a$ (not necessarily in $A$) and any $b\in B$, $f[a\mapsto b]$ denotes the function that maps $a$ to $b$ and agrees with $f$ over $A\backslash \{a\}$. Satisfaction of an expression is then defined as:

Possibility formulae $⟨b⟩\phi$ denote all the traces $t=du$ that begin with an action $d$ that is in the action set described by $b\delta$ and whose tail $u$ satisfies the continuation formula $\phi$. Dually, necessity formulae $[b]\phi$ describe all the traces that, whenever they begin with such an action $d$, continue with a trace that satisfies $\phi$. Note that in the linear-time setting, necessity can be expressed as possibility: $[b]\phi \equiv ⟨\neg b⟩\mathrm{𝗍𝗍}\vee ⟨b⟩\phi$, and dually $⟨b⟩\phi =[\neg b]\mathrm{𝖿𝖿}\wedge [b]\phi$. The existential quantifier $\exists 𝒙.\phi$ is interpreted as the set of traces that satisfy $\phi$ by assigning some $d\in 𝔻$ to $x$; the universal quantifier $\forall 𝒙.\phi$ is the set of traces satisfying $\phi$ under all such assignments. Formulae are only interpreted with regards to data environments whose domain includes the set of free data variables occurring in them. Note that existential quantification cannot be expressed using universal quantification, except using negation, which is not allowed in the syntax outside modalities.

Since the logic does not have an explicit negation operator, for all $\phi$ the semantic function $⟦\phi ,\rho ,\delta ⟧$ is monotonic in $\rho$ over the complete lattice $(\text{DInt},⊑)$, where the partial order $⊑$ corresponds to graph inclusion. Formally, it is defined, for all $F,G\in \text{DInt}$, as $F⊑G$ whenever $\forall \delta \in \text{DEnv}.F(\delta )\subseteq G(\delta )$. As is standard in the modal $\mu$-calculus, recursion is interpreted through fixed points: by the Knaster-Tarski theorem [53], $\mathrm{𝗆𝗂𝗇}X.(\phi )$ and $\mathrm{𝗆𝖺𝗑}X.(\phi )$ respectively correspond to the least and greatest fixed point of the operator that maps a data interpretation $F:\text{DEnv}\to 2^{\text{Trc}}$ to the data interpretation $\delta \mapsto ⟦\phi ,\rho [X\mapsto F],\delta ⟧$. This is the analogue of the operator used to define the semantics of the modal $\mu$-calculus over traces, lifted to the case of infinite alphabets by parameterising the interpretation by a data environment, in the spirit of [41]. To obtain the sought interpretation for $\mathrm{𝗆𝗂𝗇}X.(\phi )$ and $\mathrm{𝗆𝖺𝗑}X.(\phi )$, one then applies the least (resp., greatest) fixed point of this operator (which is a function from data environments to sets of traces) to the current data environment $\delta$.

By construction, they both satisfy the following fixed-point equations where, for all formulae $\phi ,\psi \in \mu {\text{HML}}^d$ and all recursion variables $X\in \text{FVar}$, we write $\phi [\psi /X]$ for the formula that results by the standard capture-avoiding substitution of all free occurrences of $X$ in $\phi$ with $\psi$:

When a formula is closed with regards to recursion variables (respectively, data variables), its interpretation does not depend on the trace environment $\rho$ (resp., the data environment $\delta$) and we write $⟦\phi ,\delta ⟧$ (resp., $⟦\phi ,\rho ⟧$) in lieu of $⟦\phi ,\rho ,\delta ⟧$. For closed formulae, we drop both and write $⟦\phi ⟧$ in lieu of $⟦\phi ,\rho ,\delta ⟧$ for clarity. We say that a trace $t$ satisfies a closed formula $\phi$ if $t\in ⟦\phi ⟧$, and violates $\phi$ if $t\notin ⟦\phi ⟧$. In the following, in all closed formulae $\phi$ we assume that each recursion variable $X$ appears in a unique fixed-point formula ${\mathrm{𝚏𝚡}}_{\phi }(X)$, which is either of the form $\mathrm{𝗆𝗂𝗇}X.({\phi }_X)$ or $\mathrm{𝗆𝖺𝗑}X.({\phi }_X)$. If $\mathrm{𝚏𝚡}(X)$ is $\mathrm{𝗆𝗂𝗇}X.({\phi }_X)$, then $X$ is called an lfp variable; otherwise, $X$ is called a gfp variable. We write $X\le Y$ when ${\phi }_X$ is a subformula of ${\phi }_Y$, when moreover $X\ne Y$, and denote by $\mathrm{𝚜𝚞𝚋}(\phi )$ the set of subformulae of $\phi$.

Over data words, the infinity of the domain implies that compromises have to be made between expressiveness, closure properties and decidability [17, 27]. By adapting the classical encoding [25, Section 12], one can observe that $\mu {\text{HML}}^d$ is strictly more expressive than LTL with freeze [30]. Thus, in our setting, decidability fails: the satisfiability and validity problems of $\mu {\text{HML}}^d$ are undecidable, in contrast with the finite alphabet case ($\mu$HML) [54]. By adapting the reduction of [49, Theorem 18], we can sharpen the undecidability result:

The decidability picture for $\mu {\text{HML}}^d$ is quite grim, but fortunately, as we will see in Sec. 3, this does not prevent us from delineating monitorable fragments of that logic.

We introduce an alternative semantics for formulae in $\mu {\text{HML}}^d$, to better argue about the monitorability of a formula. Annotations are analogous to choice functions [52, Section 4] (see also [24, Theorem 2.1]), and consist in (possibly infinite) witnesses that a formula holds.

Note that all conditions are local, except for lfp-consistency that allows us to distinguish between least and greatest fixed-points by forbidding least fixed-points to be unfolded infinitely often without encountering larger recursion variables.

The following result states that annotations do yield an alternative semantics for $\mu {\text{HML}}^d$:

The goal of this paper is to determine which properties can be verified at runtime. Informally, runtime verification is conducted as follows: along its execution, the system under scrutiny produces a trace, whose elements carry information about its operations; it can be thought of as a dynamically produced log file. We do not assume that the system terminates, so the trace is infinite, but termination can obviously be modelled e.g. by a termination symbol.

In parallel with the execution of the system, a program, called monitor, passively reads each element of the execution trace in an on-line manner. At any time, the monitor can emit a yes (respectively, a no) verdict, meaning that it considers that the system under scrutiny satisfies (resp., violates) a given specification. We then say that the monitor accepts (respectively, rejects) the trace. Note, however, that a monitor may never emit a verdict on reading an execution trace, e.g. if it does not have enough information to conclude. In this paper, we focus on irrevocable verdicts, meaning that once a verdict is emitted, the monitor cannot change its mind. Thus, for now, we can define a monitor through its acceptance and rejectance predicates (which will later on be defined through an operational model). Our definitions are inspired from [4, 6], although similar ideas already appeared earlier in the literature [50].

Note that the irrevocability criterion implies that monitors only recognise suffix-closed languages, in the sense that both the sets of accepted and rejected traces of a monitor are suffix-closed. We can now relate monitors and properties:

In plain words, a property is completely monitorable if there exists a monitor that detects all its satisfactions and violations. Monitorability is thus defined relative to a monitor model, since it depends on the computational power of the monitoring program. As a first step, we consider monitors with arbitrary power; we do not even assume that they are computable. This very strong definition is to be thought of as an overapproximation. However, as witnessed by Theorem 14, a quite weak monitor model suffices, since completely monitorable properties turn out to be very simple. This motivates the study of satisfaction-completeness in Secs. 3.3 and 4, as well as that of optimal monitors (Sec. 3.1 below) in Sec. 3.4.

For now, a monitor is to be conceived simply as a machine (possibly with access to arbitrary oracles) $m$ which processes a trace and possibly eventually raises a yes or a no verdict. When monitoring for some formula $\phi \in \mu {\text{HML}}^d$, if $m$ emits yes upon reading a finite trace $w\in \text{FTrc}$, it means that any continuation $wt\in {𝔻}^{\omega }$ belongs to $⟦\phi ⟧$. Conversely, if it emits a no, it means that $w{𝔻}^{\omega }\cap ⟦\phi ⟧=\mathrm{\varnothing }$. Thus, as long as we are not concerned with the way it executes, a monitor $m$ is fully described by the set of prefixes for which it emits a verdict. Observe that $T$ is completely monitorable iff there exist two sets $G,B\subseteq \text{FTrc}$ such that $T=G{𝔻}^{\omega }=\text{Trc}\backslash (B{𝔻}^{\omega })$, i.e., it is characterised by its good and bad prefixes.

In the finite alphabet case, all completely monitorable formulae can be expressed in the fragment HML, which consists in formulae of $\mu$HML without recursion [4, Theorem 4.8]. The proof of that result can be adapted to establish the following theorem, taming the infinity of the domain by quotienting finite traces by bijections over $𝔻$ (${\text{HML}}^d$ is defined in Fig. 1).

Having to detect all satisfactions and all violations prevents us from monitoring for behaviours that can happen after an unbounded number of steps in a system execution, restricting us to the tiny fragment ${\text{HML}}^d$, where properties cannot be recursive. In the following, we relax our notion of completeness and focus on detecting only one kind of verdict, i.e., single-verdict monitors. We also consider the richer setting of optimal monitors in Sec. 3.4, but most results are unfortunately negative. Without loss of generality, we consider satisfaction-completeness, the ability to detect all satisfactions of a property. In practice, as reflected in the literature, runtime verification is more focussed on detecting violations, which are often more critical. Since this adds one level of negation and hence of technicality, we work with satisfactions and results about violation-completeness are obtained by duality.

The main obstacle to complete monitorability is that of behaviours that happen in the limit, which obviously cannot be monitored for at runtime. For instance, no monitor can ever detect that there are only finitely many occurrences of a given data value. In the spirit of [5], we thus consider optimal monitors, that are only required to flag all violations or satisfactions that may be detected by some monitor.

First, ${\text{disj}\text{HML}}^d$ (as defined in Fig. 1) is equivalent to non-deterministic register automata. Their emptiness problem is decidable [45, Theorem 1], so we can build optimal monitors:

Yet, as soon as we add conjunctions to get ${\text{c}\text{HML}}^d$, this becomes impossible. Indeed, from a violation-optimal monitor one can build a semi-algorithm to decide unsatisfiability of ${\text{c}\text{HML}}^d$. Since we have a semi-algorithm for satisfiability of ${\text{c}\text{HML}}^d$ (Sec. 2.4), this would yield an algorithm to decide satisfiability of ${\text{c}\text{HML}}^d$, contradicting Theorem 4.

In general, universally quantified formulae are not monitorable for satifactions, as they require checking infinitely many instantiations of the quantified variable. Consider, e.g., the formula $\forall 𝒙.\mathrm{𝗆𝗂𝗇}X.(⟨\star =x⟩\mathrm{𝗍𝗍}\vee ⟨\star \ne x⟩X)$ which states that all data values appear in the input. It is satisfiable, since we assumed that the data domain is countable. Yet, it is not monitorable for satisfactions: any finite prefix only contains finitely many data values and can be continued by, e.g., ${\mathrm{\#}}^{\omega }$, yielding an input which violates the formula.

Nevertheless, some formulae containing universal quantifiers are monitorable. Consider the property which states that the input is divided into blocks separated by dollar and sharp symbols, and that all data values that appear in the second block appear in the first block (formalised in Equation 8). It is monitorable for satisfactions: the monitor reads the first two blocks by waiting to see the $\$$ and then the $\mathrm{\#}$; if this never happens it means that the input violates the property. Otherwise, the monitor can check that all data values in the second block appear in the first one by processing them one by one, going back and forth.

The formula $\gamma (x)$ is called the guard, and sets a monitorable bound on the maximal position where a candidate $x$ violating the formula $\psi$ can be found. This way, once the bound is found, the monitor knows that the subsequent data values that appear need not be checked. Here, it expresses that the trace starts with two blocks – ended by $ and #, respectively – and that $x$ does not appear in the second block: first, look for a $\$$; once it is found, look for a $\mathrm{\#}$, and if in the meantime $x$ is encountered, the formula cannot recurse and therefore rejects.

The formula $\psi (x)$ is the universally quantified property, and since we are looking for satisfactions, its universal quantification has to be limited to finitely many values to ensure that it has a finite witness, hence the disjunction with the guard. Here, it expresses that $x$ appears in the first block. Summing up, the conjunct $\exists 𝒙.\gamma (x)$ ensures that a trace has the form $w_1\$w_2\mathrm{\#}u$ for some $w_1,w_2\in {𝔻}^{\ast }$ and $u\in \text{Trc}$, while the conjunct $\forall 𝒙.\left(\gamma (x)\vee \psi (x)\right)$ yields that every $d\in 𝔻$ occurring in $w_2$ also occurs in $w_1$.

The above property cannot however be expressed in ${\text{c}\text{HML}}^d$. Indeed, the length of $w_2$ is unbounded, and its elements have to be compared to elements that appear before in the input, so they cannot be manipulated only using existential quantifiers, even with fixed points. This is made formal by going through monitors: by Theorem 17, the synthesis procedure of Fig. 2 yields sound a satisfaction-complete monitors. Now, those monitors can only carry boundedly many data values accross the $\$$ sign. Thus, ${\text{c}\text{HML}}^d$ is not a maximally monitorable fragment.

We now proceed to characterise the collection of formulae without greatest fixed points that can be monitored in a sound and satisfaction-complete fashion. Given a formula $\gamma$, a data variable $x$, and a finite set $F\subset \text{DVar}$ of data variables, we use the following notations:

The formula $x\ne F$ describes that the value of $x$ is different from every value assigned to any element of $F$ (except for $x$ if $x\in F$), and $x\sim F$ conversely describes that the value of $x$ coincides with the value assigned to some other element of $F$.

The quantifier in $\forall 𝒙\mathbf{\le }𝜸\mathbf{+}𝑭.\phi$ intuitively bounds the quantification of $x$, as we only need to verify $\phi$ for all data values that are assigned to variables in $F\overline{x}$ and the ones for which $\gamma$ is not true. As such, we say that $\gamma$ is a guard or bound for $x$, or that $x$ is guarded. We need to keep track of the free and guarded variables. Hence, we parameterize the definition of our fragment with respect to two finite sets of data variables. For all finite $F\subset \text{DVar}$ and $V\subseteq F$, we define ${\text{min}\text{HML}}_{{\forall }_{g}V,F}^d$ as the set of formulae that are produced from ${\phi }_{V,F}$ in the following grammar whose grammar variables are parameterized with respect to $V$ and $F$:

We then define ${\text{min}\text{HML}}_{{\forall }_g}^d={\bigcup }_{V\subseteq F\subset \text{DVar}}{\text{min}\text{HML}}_{{\forall }_{g}V,F}^d$. If $\phi \in {\text{min}\text{HML}}_{{\forall }_g}^d$ has no free data variables, then $\phi \in {\text{min}\text{HML}}_{{\forall }_g\mathrm{\varnothing },\mathrm{\varnothing }}^d$. In the above grammar, the set $F$ keeps track of the free variables in $\phi$, and $V$ of the “guarded” free variables. Here, “$x$ is guarded” means that the value of $x$ is not encountered in the trace while we evaluate the formula (but this value is still assigned to some variable). This is ensured by the “$\star \ne V$” conjunct in the diamonds and by guaranteeing that, during the existential quantification of $y$, if the value of $y$ matches that of some $x$ in $V$, then $y$ is added to $V$. Hence ${\phi }_{Vx,F}(x)$ can only be true for values of $x$ that do not appear in some finite annotation of $\phi$.

The main characteristic of this fragment is that every universal quantification is guarded by a bound on the positions where a candidate $x$ violating the formula can be found. This is achieved by partitioning the potential values of $x$ into those that appear during the (finite) evaluation of the guard (and must be checked against $\phi$) and those that do not (and therefore satisfy the guard). Thus, when monitoring or evaluating $\forall 𝒙\mathbf{\le }{𝜸}_{𝑽𝒙\mathbf{,}𝑭𝒙}\mathbf{+}𝑭.{\phi }_{V\overline{x},Fx}$, we only need to consider a fixed number of cases for the value of $x$ when checking the subformula ${\gamma }_{Vx,Fx}$, and therefore, ${\gamma }_{Vx,Fx}$ is, in a sense, easier to monitor for, or evaluate, than ${\phi }_{V\overline{x},Fx}$. Then, the number of cases that we need to consider for the value of $x$ when checking the subformula ${\phi }_{V\overline{x},Fx}$ is finite and depends on how we evaluated ${\gamma }_{Vx,Fx}$.

In ${\phi }_{\forall \mathrm{\#}\exists \$}$, the evaluation of the guard $\gamma$ is complete at the end of the second block. Therefore, to evaluate $\forall x.(\gamma (x)\vee \psi (x))$, it suffices to check values of $x$ for $\psi$ that appear during the evaluation of $\gamma$ – specifically in the second block. More generally, the grammar of ${\text{min}\text{HML}}_{{\forall }_g}^d$ induces a recursive strategy to evaluate a formula while only remembering finitely many cases for the values assigned to its variables. As we see below, this allows us to find a finite witness for the satisfaction of a formula, using a guarded version of annotations, and, subsequently, to monitor for the satisfaction of all formulae in ${\text{min}\text{HML}}_{{\forall }_g}^d$.