A Theory of Monitors

Abstract

We develop a behavioural theory for monitors — software entities that passively analyse the runtime behaviour of systems so as to infer properties about them. First, we extend the monitor language and instrumentation relation of [17] to handle piCalculus process monitoring. We then identify contextual behavioural preorders that allow us to relate monitors according to criteria defined over monitored executions of piCalculus processes. Subsequently, we develop alternative monitor preorders that are more tractable, and prove full-abstraction for the latter alternative preorders with respect to the contextual preorders.

The research was supported by the UoM research fund CPSRP05-04 and the research grant COST-STSM-ECOST-STSM-IC1201-170214-038253.

These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

1 Introduction

Monitors (execution montors [32]) are software entities that are instrumented to execute along side a program so as determine properties about it, inferred from the runtime analysis of the exhibited (program) execution; this basic monitor form is occasionally termed (sequence) recognisers [28]. In other settings, monitors go further and either adapt aspects of the monitored program [7, 11, 22] or enforce predefined properties by modifying the observable behaviour [4, 15, 28]. Monitors are central to software engineering techniques such as monitor-oriented programming [16] and fail-fast design patterns [8] used in fault-tolerant systems [19, 34]; they are also used exten sively in runtime verification [27], a lightweight verification technique that attempts to mitigate state explosion problems associated with full-blown verification methods such as model checking.

Monitoring setups typically consist of three components: apart from the program being monitored, P, there is the monitor itself, M, and the instrumentation, the mechanism composing the monitor with the program, $P \triangleleft \, M$. The latter gives rise to a software composition relation that has seldom been studied in its own right. This paper investigates compositional reasoning techniques for monitors performing detections (recognisers), composed using the instrumentation relation employed in [17], for programs expressed as piCalculus processes [29, 31], a well-studied concurrency model. We set out to develop monitor preorders

$$\begin{aligned} M_1 \sqsubseteq M_2 \end{aligned}$$

(1)

stating that, when instrumented in the context of an arbitrary process P, if $P \triangleleft \, M_1$ exhibits certain properties, then $P \triangleleft \, M_2$ exhibits them as well. Within this setup, we formalise the possible instrumentation properties one may require from an instrumented (monitored) process, and show how these give rise to different monitoring preorders.

Example 1

Consider the monitors $M_1$ and $M_2$ below. $M_1$ monitors for output actions on channel a with a payload that is not in the set C. Apart from detecting the same outputs on channel a, $M_2$ also detects outputs with payload b on channels that are not in D (the $+$ construct acts as an external choice [23]).

$$\begin{aligned} M_1&=\textsf {match}\, a ! x .\textsf {if}\; x\not \in C \,\textsf {then}\, \checkmark \\ M_2&=(\textsf {match}\, a ! x .\textsf {if}\; x\not \in C \,\textsf {then}\, \checkmark )\,+(\,\textsf {match}\, y ! b .\textsf {if}\; y \not \in D \,\textsf {then}\, \checkmark ) \end{aligned}$$

One can argue that $M_2$ is related to $M_1$, i.e., $M_1 \sqsubseteq M_2$, since all the detections raised by $M_1$ are also raised by $M_2$. However, under different criteria, the two monitors would not be related. Consider the case where $a \in D$ (or $b\in C$): for a process P exhibiting action $a ! b$, monitor $M_2$ may non-deterministically fail to detect this behaviour; by contrast, $M_1$ always detects the behaviour $a ! b$ and, in this sense, $M_2$ does not preserve all the properties of $M_1$. Monitors are also expected to interfere minimally with the execution of the analysed process, giving rise to other criteria for relating monitors, as we will see in the sequel. $\blacksquare$

There are various reasons why such preorders are useful. For a start, they act as notions of refinement: they allow us to formally specify properties that are expected of a monitor M by expressing them in terms of a monitor description, $\textsf {Spec}_M$, and then requiring that $\textsf {Spec}_M \sqsubseteq M$ holds. Moreover, our preorders provide a formal understanding for when it is valid to substitute one monitor implementation for another while preserving elected monitoring properties. We consider a general model that allows monitors to behave non-deterministically; this permits us to study the cases where non-determinism is either tolerated or considered erroneous. Indeed, there are settings where determinism is unattainable (e.g., distributed monitoring [18, 33]). Occasionally, non-determinism is also used to expresses under-specification in program refinement.

Although formal and intuitive, the preorders alluded to in (1) turn out to be hard to establish. One of the principal obstacles is the universal quantification over all possible processes for which the monitoring properties should hold. We therefore develop alternative characterisations for these preorders, $M_1 \le M_2$, that do not rely on this universal quantification over process instrumentation. We show that such relations are sound wrt. the former monitor preorders, which serves as a semantic justification for the alternative monitor preorders. More importantly, however, it also allows us to use the more tractable alternative relations as a proof technique for establishing inequalities in the original preorders. We also show that these characterisations are complete, thereby obtaining full-abstraction for these alternative preorders.

The rest of the paper is structured as follows. Section 2 briefly overviews our process model whereas Sect. 3 introduces our monitor language together with the instrumentation relation. In Sect. 4 we formalise our monitor preorder relations wrt. this instrumentation. We develop our alternative preorders in Sect. 5, where we also establish the correspondence with the other preorders. Section 6 concludes.

Fig. 1.

piCalculus syntax and semantics

2 The Language

Figure 1 presents our process language, a standard version of the piCalculus. It has the usual constructs and assumes separate denumerable sets for channel names $c,d,a,b \in \textsc {Chans}$, variables $x, y, z\in \textsc {Vars}$ and process variables, $X, Y\in \textsc {PVars}$, and lets identifiers $u,\,v$ range over the sets, $\textsc {Chans} \cup \textsc {Vars}$. The input construct, $c \textsf {?} x . P$, the recursion construct, $\textsf {rec}\,X.P$, and the scoping construct, $\textsf {new}\,c. P$, are binders where the free occurrences of the variable x, the process variable $X$, and the channel c resp., are bound in the guarded body P. We write $\mathbf{fv }(P), \mathbf{fV }(P),\mathbf{fn }(P), \mathbf{bV }(P),\mathbf{bv }(P)$ and $\mathbf{bn }(P)$ for the resp. free/bound variables, process variables and names in P. We use standard syntactic conventions e.g., we identify processes up to renaming of bound names and variables (alpha conversion). For arbitrary syntactic objects $o, o'$, we write $o \,\sharp \,o'$ when the free names in o and $o'$ are disjoint e.g., $P \,\sharp \,Q$ means $\mathbf{fn }(P) \cap \mathbf{fn }(Q) = \emptyset$.

The operational semantics of the language is defined by the Labelled Transition System (LTS) shown in Fig. 1. LTS judgements are of the form

$$\begin{aligned}&I \triangleright P \xrightarrow {\;\mu \;} P' \end{aligned}$$

where $I\subseteq \textsc {Chans}$ denotes an interface of names known (or shared) by both the process and an implicit observer (with which interactions occur), P is a closed term, and $\mathbf{fn }(P) \subseteq I$. We write $I,c$ as a shorthand for $I\cup \left\{ c\right\}$ where $c \not \in I$, and generally assume a version of the Barendregt convention whereby $\mathbf{bn }(P) \,\sharp \,I$.¹ For arbitrary names c, d, actions $\mu \in \textsc {Act} _\tau$ range over input actions, $c ? d$, output actions, $c ! d$, and a distinguished silent action, $\tau$ ($\alpha \in \textsc {Act}$ ranges over external actions, that exclude $\tau$). The rules in Fig. 1 are fairly standard, using $I$ for book-keeping purposes relating to free/bound names (we elide symmetric rules for pPar, pCom and pCls); implicitly, $c,d \in I$ in rule pOut and $c \in I$ in rule pIn (but d is not necessarily in $I$). We use $s,t \in \textsc {Act} ^*$ to denote traces of external actions. Although actions do not include explicit information relating to extruded names, this may be retrieved using $I$ as shown in Definition 1; the absence of action name binding (as in [24, 31]) simplifies subsequent handling of traces. The evolution of $I$ after a transition is determined exclusively by the resp. action of the transition, defined as $\mathbf{aftr }(I,\mu )$ in Definition 1; note that both the process (through outputs) and the implicit observer (through inputs) may extend $I$.

Definition 1

(Extruded Names and Interface Evolution)

$$\begin{aligned} \mathbf{ext }(I, \tau )&\mathop {=}\limits ^\mathbf{\tiny def }\emptyset&\mathbf{ext }(I,c ! d )&\mathop {=}\limits ^\mathbf{\tiny def }\left\{ d\right\} \!\setminus \! I&\mathbf{ext }(I, c ? d )&\mathop {=}\limits ^\mathbf{\tiny def }\emptyset \\ \mathbf{aftr }(I,\tau )&\mathop {=}\limits ^\mathbf{\tiny def }I&\mathbf{aftr }(I,c ! d )&\mathop {=}\limits ^\mathbf{\tiny def }I\cup \left\{ d\right\}&\mathbf{aftr }(I,c ? d )&\mathop {=}\limits ^\mathbf{\tiny def }I\cup \left\{ d\right\} \end{aligned}$$

We lift the functions in Definition 1 to traces, e.g., $\mathbf{aftr }(I,s)$, in the obvious way and denote successive transitions $I \triangleright P \xrightarrow {\;\mu _1\;} P_1$ and $\mathbf{aftr }(I,\mu _1) \triangleright P_1\xrightarrow {\;\mu _2\;} P_2$ as $I \triangleright P \xrightarrow {\;\mu _1\;} \mathbf{aftr }(I,\mu _1) \triangleright P_1 \xrightarrow {\;\mu _2\;} P_2$. We write $I \triangleright P\not \!\xrightarrow {\;\mu \;}$ to denote $\not \!\exists P' \cdot I \triangleright P\xrightarrow {\;\mu \;} P'$ and to denote $I_0 \triangleright P_0 \xrightarrow {\;\mu _1\;} I_1 \triangleright P_1 \xrightarrow {\;\mu _2\;} I_2 \triangleright P_2 \ldots \xrightarrow {\;\mu _n\;} P_n$ where $P_0 = P$, $P_n=Q$, $I_0=I$, $I_i = \mathbf{aftr }(I_{i-1},\mu _i)$ for $i\in 1..n$, and $s$ is equal to $\mu _1\ldots \mu _n$ after filtering $\tau$ labels.

Example 2

Consider $P_\text {sv}= \textsf {rec}\,X.c \textsf {?} x . \textsf {new}\,d. x \textsf {!} d . X$, modelling the idiomatic server that repeatedly waits for requests on c and answers back on the inputted channel with a fresh channel. We can derive the following behaviour wrt. $I= \left\{ c\right\}$:

Above, bound outputs/inputs [31] are manifested as interface extensions. $\blacksquare$

Fig. 2.

Monitor syntax, semantics and Instrumentation Semantics

3 Monitor Instrumentation

Monitors, $M,N \in \textsc {Mon}$, are syntactically defined by the grammar of Fig. 2. They may reach either of two verdicts, namely detection, $\checkmark$, or termination, $\textsf {end}$, denoting an inconclusive verdict. Our setting is a mild generalisation to that in [17] since monitors need to reason about communicated names so as to adequately monitor for piCalculus processes. They are thus equipped with a pattern matching construct (used to observe external actions) and a name-comparison branching construct. The remaining constructs, i.e., external branching and recursion, are standard. Note that, whereas the syntax allows for monitors with free occurrences of monitor variables, monitors are always closed wrt. (value) variables, whereby the outermost occurrence of a variable acts as a binder. E.g., in the monitor ($x ? c .x ! y .\textsf {if}\; y \!=\! d\,\textsf {then}\, \textsf {end}\;\textsf {else}\; \checkmark$) pattern $x ? c$ binds variable x in the continuation whereas pattern $x ! y$ binds variable y.

The monitor semantics is defined in terms of an LTS (Fig. 2), modeling the analysis of the visible runtime execution of a process. Following [15, 17, 30], in rule mVer verdicts are able to analyse any external action but transition to the same verdict, i.e., verdicts are irrevocable. By contrast, pattern-guarded monitors only transition when the action matches the pattern, binding pattern variables to the resp. action names, $\textsf {match}(p,\alpha ) =\sigma$, and substituting them in the continuation, $M\sigma$; see rule mPat. The remaining transitions are unremarkable.

A monitored system, $P \triangleleft \, M$, consists of a process, P, instrumented with a monitor, M, analysing its (external) behaviour. Figure 2 defines the instrumentation semantics for configurations, $I \triangleright P \triangleleft \, M$, i.e., systems augmented with an interface $I$, where again we assume P is closed and $\mathbf{fn }(P) \subseteq I$. The LTS semantics follows [7, 17] and relies on the resp. process and monitor semantics of Figs. 1 and 2. In rule iMon, if the process exhibits the external action $\alpha$ wrt. $I$, and the monitor can analyse this action, they transition in lock-step in the instrumented system while exhibiting same action. If, however, a process exhibits an action that the monitor cannot analyse, the action is manifested at system level while the monitor is terminated; see rule iTer. Finally, iAsyP and iAsyM allow monitors and processes to transition independently wrt. internal moves, i.e., our instrumentation forces process-monitor synchronisation for external actions only, which constitute our monitorable actions. We note that, as is expected of recognisers, the process drives the behaviour of a monitored system: if the process cannot $\alpha$-transition, the monitored system cannot $\alpha$-transition either.

Example 3

Recall $P_\text {sv}$ from Example 2. Using the semantics of Fig. 2, one can derive the monitored execution leading to a detection below, when composed with the monitor $M_1 = \bigl (c ? y .y ! z .\textsf {if}\; z \!=\! c\,\textsf {then}\, \textsf {end}\;\textsf {else}\; \checkmark \bigr )$, subject to $I' = \left\{ c,a\right\}$:

Contrastingly, for the same $I'$, monitoring with $M_2 = (y ! z .\textsf {if}\; y \!=\! a\,\textsf {then}\, \textsf {end}\;\textsf {else}\; \checkmark )$ does not lead to a detection for the same trace, because the first action, $c ? a$ (an input) cannot pattern match with the output pattern, $y ! z$. In fact, rule iTer terminates the monitor after transition $c ? a$, so as to avoid erroneous detections.

(2)

For illustrative purposes, consider $N=c ? y .\textsf {if}\; y \!=\! c\,\textsf {then}\, \textsf {end}\;\textsf {else}\; y ! z .c ? z .\checkmark$, another monitor. We have the following (dissected) transition sequence for $I=\left\{ c\right\}$:

$$\begin{aligned} \!\!\!\! I \triangleright P_\text {sv} \triangleleft \, \!N\! \quad&\xrightarrow {\tau }\cdot \xrightarrow {c ? a }&I,a \triangleright \big (\!\textsf {new}\,d. a \textsf {!} d . P_\text {sv}\!\big ) \triangleleft \, \textsf {if}\; a \!=\! c\,\textsf {then}\, \textsf {end}\;\textsf {else}\; a ! z .c ? z .\checkmark \end{aligned}$$

(3)

$$\begin{aligned}&\xrightarrow {\;\tau \;}&I,a \triangleright \big (\textsf {new}\,d. a \textsf {!} d . P_\text {sv}\big ) \triangleleft \, a ! z .c ? z .\checkmark \end{aligned}$$

(4)

$$\begin{aligned}&\xrightarrow {\;a ! d \;}&(I,a,d) \triangleright P_\text {sv} \triangleleft \, c ? d .\checkmark \end{aligned}$$

(5)

$$\begin{aligned}&\xrightarrow {\tau }\cdot \xrightarrow {c ? b }&(I,a,d,b) \triangleright \textsf {new}\,d'. b \textsf {!} d' . P_\text {sv} \triangleleft \, \textsf {end} \end{aligned}$$

(6)

$$\begin{aligned}&\xrightarrow {\;b ! d' \;}&(I,a,d,b,d') \triangleright P_\text {sv} \triangleleft \, \textsf {end} \end{aligned}$$

(7)

In (3) the server (asynchronously) unfolds (pRec and iAsyP) and inputs on c the fresh name a (pIn); the monitor can analyse $c ? a$ (mPat where $\textsf {match}(c ? y ,c ? a ) = \left\{ y\mapsto a\right\}$), transitioning accordingly (iMon) while learning the fresh name a for future monitoring. At this stage, the instrumentation temporarily stalls the process, even though it can produce the (scope extruding) output $a ! d$. More precisely, although the monitor cannot presently analyse $a ! d$, the rule iTer — which terminates the monitor execution — cannot be applied, since the monitor can silently transition and potentially become capable of analysing the action. This is indeed the case, (4) using mEls, resulting in the second monitoring transition, (5) using iMon, where the monitor learns the second fresh name d, this time originating from the monitored process. After another unfolding, the process is ready to input on c again. However, the monitor cannot match $c ? b$ ($\textsf {match}(c ? d ,c ? b )$ is undefined) and since the monitor cannot silently transition either, it is terminated (iTer) while still allowing the process to proceed, (6). In (7), verdicts allow monitored processes to execute without any hindrance. $\blacksquare$

Example 3 highlights two conflicting instrumentation requirements. On the one hand, monitors should interfere minimally with the execution of a monitored process where, observationally, a monitored process should behave like the original one. On the other hand, instrumentation must also ensure bona fide detections, e.g., in (2) and (6), terminating monitoring when the observed process behaviour does not correspond, (through rule iTer). But in order to do this while avoiding premature termination, instrumentation needs to allow for monitor internal computation, e.g., (4). Unfortunately, the premise caveat $M \not \!\xrightarrow {\;\tau \;}$ in rule iTer — necessary to prevent premature terminations — allows monitors to affect (indirectly) process behaviour. For instance the monitor $\varOmega$ below:

$$\begin{aligned} \varOmega&= \textsf {rec}\,X.(\textsf {if}\; c \!=\! c\,\textsf {then}\, X\;\textsf {else}\; X )&\varOmega '&= \textsf {if}\; c \!=\! c\,\textsf {then}\, \varOmega \;\textsf {else}\; \varOmega \end{aligned}$$

(8)

is divergent, i.e., $\varOmega \xrightarrow {\tau } \varOmega ' \xrightarrow {\tau } \varOmega \xrightarrow {\tau } \ldots$, and unresponsive, i.e., $\forall \alpha \cdot \varOmega \not \!\xrightarrow {\;\alpha \;}$ and $\varOmega ' \not \!\xrightarrow {\;\alpha \;}$. As a result, it suppresses every process external behaviour when instrumented: for arbitrary $I \triangleright P$ we can show $I \triangleright P \triangleleft \, \varOmega \not \!\xrightarrow {\;\alpha \;}$ and $I \triangleright P \triangleleft \, \varOmega ' \not \!\xrightarrow {\;\alpha \;}$ for any $\alpha$, since rules iMon and iTer cannot be applied. We revisit this point in Sect. 4. We conclude with the property stating that verdicts are irrevocable.

Theorem 1

(Definite Verdicts).

4 Monitor Preorders

We can use the formal setting presented in Sect. 3 to develop the monitor preorders discussed in the Introduction. We start by defining the monitoring predicates we expect to be preserved by the preorder; a number of these predicates rely on computations and detected computations, defined below.

Definition 2

(Detected Computations). The transition sequence

is called an $s$ -computation if it is maximal (i.e., either it is infinite or it is finite and cannot be extended further using $\tau$-transitions). An $s$-computation is called detected (or a detected computation along $s$) iff $\exists n\in \mathbb {N}\cdot M_n = \checkmark$. $\blacksquare$

One criteria for comparing monitors considers the verdicts reached after observing a specific execution trace produced by the process under scrutiny. The semantics of Sect. 3 assigns a passive role to monitors, prohibiting them from influencing the branching execution of the monitored process. Definition 2 thus differentiates between detected computations, identifying them by the visible trace that is dictated by the process (over which the monitor should not have any control).

Example 4

Consider $P=\textsf {new}\,d. (d \textsf {!} \!\parallel \!d \textsf {?} . c \textsf {!} a \!\parallel \!d \textsf {?} . c \textsf {!} b )$, $I= \left\{ c,b,a\right\}$ and monitors:

$$\begin{aligned} M_1&= c ! a .\checkmark +c ! b .\checkmark \quad&M_2&= c ! a .\checkmark +c ! b .\textsf {end} \qquad M_3 = c ! a .\checkmark \\ M_4&= c ! a .\checkmark +c ! b .\checkmark +c ! b .\textsf {end} \quad&M_5&= c ! a .\checkmark +c ! b .\checkmark +c ! a .\textsf {end}+c ! b .\textsf {end} \end{aligned}$$

Configurations $I \triangleright M_i \triangleleft \, P$ for $i\in 1..5$ exhibit detecting computations along $s =c ! a .\epsilon$. For trace $t =c ! b .\epsilon$, configurations $I \triangleright M_j \triangleleft \, P$ for $j\in \left\{ 1,4,5\right\}$ detect $t$-computations as well, whereas the resp. configurations with $M_2$ and $M_3$ do not. Although the configuration with $M_1$ always detects along $t$, those with $M_4$ and $M_5$ may fail to detect it along such a trace. Similarly, configuration with $M_1$ and $M_4$ deterministically detect along trace $s$, but $I \triangleright M_5 \triangleleft \, P$ does not. $\blacksquare$

Example 4 suggests two types of computation detections that a monitor may exhibit.

Definition 3

(Potential and Deterministic Detection). M potentially detects for $I \triangleright P$ along trace $s$, denoted as $\textsf {pd}(M,I,P,s)$, iff there exists a detecting $s$-computation from $I \triangleright P \triangleleft \, M$. M deterministically detects for $I \triangleright P$ along trace $s$, denoted as $\textsf {dd}(M,I,P,s)$, iff all $s$-computation from $I \triangleright P \triangleleft \, M$ are detecting.$\blacksquare$

Remark 1

If a monitored process cannot produce trace $s$, i.e., , then $\textsf {pd}(M,I,P,s)$ is trivially false and $\textsf {dd}(M,I,P,s)$ is trivially true for any M. $\blacksquare$

The detection predicates of Definition 3 induce the following monitor preorders (and equivalences), based on the resp. detection capabilities.

Definition 4

(Potential and Deterministic Detection Preorders)

$$\begin{aligned} M \sqsubseteq _\textsf {pd} N&\quad \mathop {=}\limits ^\mathbf{\tiny def }\quad \forall I,P,s \cdot \;\textsf {pd}(M,I,P,s)\text { implies }\textsf {pd}(N,I,P,s) \\ M \sqsubseteq _\textsf {dd} N&\quad \mathop {=}\limits ^\mathbf{\tiny def }\quad \forall I,P,s \cdot \;\textsf {dd}(M,I,P,s)\text { implies }\textsf {dd}(N,I,P,s) \end{aligned}$$

$M \!\cong _\textsf {pd} \! N$ and $M\! \cong _\textsf {dd} \! N$ are the kernel equivalences induced by the resp. preorders, i.e., $M \!\cong _\textsf {pd} \! N \mathop {=}\limits ^\mathbf{\tiny def }(M \!\sqsubseteq _\textsf {pd} \! N \text { and }N\! \sqsubseteq _\textsf {pd} \! M)$, and similarly for $M \!\cong _\textsf {dd} \! N$. We write $M \!\sqsubset _\textsf {pd} \! N$ in lieu of $(M \!\sqsubseteq _\textsf {pd} \! N \text { and } N \not \sqsubseteq _\textsf {pd} M)$ and similarly for $M \!\sqsubset _\textsf {dd} \! N$. $\blacksquare$

Example 5

Recall the monitors defined in Example 4. It turns out that

$$\begin{aligned}&M_2&\cong _\textsf {pd} \quad M_3&\sqsubset _\textsf {pd} \quad M_5&\cong _\textsf {pd} \quad M_4&\cong _\textsf {pd} \quad M_1 \end{aligned}$$

(9)

$$\begin{aligned}&M_5&\sqsubset _\textsf {dd} \quad M_2&\cong _\textsf {dd} \quad M_3&\cong _\textsf {dd} \quad M_4&\sqsubset _\textsf {dd} \quad M_1 \end{aligned}$$

(10)

Note that, whereas $M_5$ can potentially detect more computations that $M_2$ and $M_3$, (9), it can deterministically detect less computations than these monitors (10); in fact, $M_5$ cannot deterministically detect any computation. $\blacksquare$

As opposed to prior work on monitors [2, 10, 15], the detection predicates in Definition 3 consider monitor behaviour within an instrumented system. Apart from acting as a continuation for the study in [17], this setup also enables us to formally justify subtle monitor orderings, Example 6, and analyse peculiarities brought about by the instrumentation relation, Example 7.

Example 6

Using the shorthand $\tau .{M}$ for $\textsf {rec}\,X.M$ where $X\not \in \mathbf{fV }(M)$, we have:

$$\begin{aligned}&\checkmark \cong _\textsf {pd} \tau .{\checkmark }&\text {but}\qquad \qquad \qquad&\checkmark \sqsubset _\textsf {dd} \tau .{\checkmark } \end{aligned}$$

For process $P=\varOmega$, defined as in (8), predicate $\textsf {dd}(\checkmark ,I,P,\epsilon )$ holds trivially, but predicate $\textsf {dd}(\tau .{\checkmark },I,P,\epsilon )$ does not, due of the non-detecting $\epsilon$-computation ${I \triangleright \varOmega \triangleleft \, \tau .{\checkmark } \xrightarrow {\tau }\cdot \xrightarrow {\tau } \varOmega \triangleleft \, \tau .{\checkmark } \xrightarrow {\tau }\cdot \xrightarrow {\tau } \ldots }$, refuting the inequality $\checkmark \!\sqsubseteq _\textsf {dd} \! \tau .{\checkmark }$. $\blacksquare$

Example 7

Recalling the divergent monitor $\varOmega$ from (8), we have:

$$\begin{aligned}&\bigl (\textsf {end}\quad \cong _\textsf {dd} \quad c ! a .{\textsf {end}}\bigr ) \quad \sqsubset _\textsf {dd} \quad c ! a .{\checkmark } \quad \sqsubset _\textsf {dd} \quad \varOmega \quad \sqsubset _\textsf {dd} \quad \checkmark \end{aligned}$$

(11)

$$\begin{aligned}&\varOmega +\textsf {end} \quad \sqsubset _\textsf {dd} \quad \bigl (\varOmega \quad \cong _\textsf {dd} \quad \varOmega +\checkmark \quad \cong _\textsf {dd} \quad \textsf {rec}\,X.(\tau .{X}+\checkmark ) \bigr )\end{aligned}$$

(12)

$$\begin{aligned}&\varOmega +c ! a .{\checkmark } \quad \sqsubset _\textsf {pd} \quad \varOmega +\checkmark \qquad \text {but}\qquad \varOmega +c ! a .{\checkmark } \quad \cong _\textsf {dd} \quad \varOmega +\checkmark \end{aligned}$$

(13)

In (11), every computation starting with monitor $\checkmark$ is trivially detected. Monitor $\varOmega$ limits all computations to $\epsilon$-computations, i.e., irrespective of $I \triangleright P$, configuration $I \triangleright P \triangleleft \, \varOmega$ exhibits no $s$-computations for any $s$ where $|s | > 0$, rendering $\textsf {dd}(\varOmega ,I,P,s)$ for $|s | > 0$ vacuously true (see Remark 1). By contrast, $\textsf {dd}(c ! a .{\checkmark },I,P,s)$ holds only whenever $s = c ! a .t$ (for arbitrary $t$) and .

In (12), monitor $\varOmega +\textsf {end}$ does not deterministically detect any computation: when composed with an arbitrary $I \triangleright P$, it clearly can never reach a detection, but it can neither prohibit the process from producing visible actions, as in the case of $\varOmega$ (see rules mVer, mChR and iMon). Monitor $\varOmega +\checkmark$ can either behave like $\varOmega$ or transition to $\checkmark$ after one external action observed; in both cases, it deterministically detects all $s$-computation where $|s |>0$. The monitor $\textsf {rec}\,X.(\tau .{X}+\checkmark )$ first silently transitions to $(\tau .{\textsf {rec}\,X.(\tau .{X}+\checkmark )})+\checkmark$ and then either transitions back to the original state or else transitions to $\checkmark$ with an external action; in either case, when composed with any process $I \triangleright P$, it also deterministically detects all $s$-computation for $|s |>0$.

In (13), although monitor $\varOmega +c ! a .{\checkmark }$ potentially detects less computations than $\varOmega +\checkmark$ (e.g., for $I=\left\{ c,a,b\right\}$, $P=c \textsf {!} b . \textsf {nil}$ and $s =c ! b .\epsilon$, the predicate $\textsf {pd}(\varOmega +\checkmark , I, P, s)$ holds but $\textsf {pd}(\varOmega +c ! a .{\checkmark }, I, P, s)$ does not), both deterministically detect the same computations, i.e., all $s$-computation where $|s |>0$. Specifically, if a process being monitored, say $I \triangleright P$, can produce an action other than $c ! a$, the instrumentation with monitor $\varOmega +c ! a .{\checkmark }$ restrains such an action, since the monitor cannot transition with that external action (it can only transition with $c ! a$) but, at the same time, it can $\tau$-transition (see rules iMon and iTrm). $\blacksquare$

The preorders in Definition 4 are not as discriminating as one might expect.

Example 8

Consider the monitor $M_\text {any}= x ? y .{\checkmark }+x ! y .{\checkmark }$.

$$\begin{aligned} M_\text {any}\;\cong _\textsf {pd} \; M_\text {any}+\varOmega&\qquad \text {and}\qquad M_\text {any}\;\cong _\textsf {dd} \; M_\text {any}+\varOmega \end{aligned}$$

(14)

$$\begin{aligned} c ! a .{\textsf {end}} \;\cong _\textsf {pd} \; c ! a .{\textsf {end}}+c ! a .{\varOmega }&\qquad \text {and}\qquad c ! a .{\textsf {end}} \;\cong _\textsf {dd} \; c ! a .{\textsf {end}}+c ! a .{\varOmega } \end{aligned}$$

(15)

Intuitively, $M_\text {any}$ potentially and deterministically detects any $s$-computation when $|s |>0$. It turns out that $M_\text {any}+\varOmega$ produces the same potential and deterministic detections, yielding the resp. equalities in (14). In (15), neither monitor produces any potential or deterministic detections and they are thus equivalent according to the resp. kernel equivalences of Definition 4. $\blacksquare$

There are however settings where the equalities established in Example 8 are deemed too coarse. E.g., in (15), whereas monitor $c ! a .$ $\textsf {end}$ is innocuous when instrumented with a process, monitor $c ! a .{\textsf {end}}+c ! a .{\varOmega }$ may potentially change the observed behaviour of the process under scrutiny after the action $c ! a$ is emitted (by suppressing external actions, as explained in Example 7); a similar argument applies for the monitors in (14). We thus define a third monitor predicate called transparency [5, 15, 28], stating that whenever a monitored process cannot perform an external action, it must be because the (unmonitored) process is unable to perform that action (i.e., the monitoring does not prohibit that action).

Definition 5

(Transparency Preorder). M is transparent for $I \triangleright P$ wrt. trace $s$, denoted as $\textsf {tr}(M,P,I,s)$, iff implies . We define the induced preorder as expected:

$$\begin{aligned} M \sqsubseteq _\textsf {tr} N \quad \mathop {=}\limits ^\mathbf{\tiny def }\quad \forall I,P,s \cdot \;\textsf {tr}(M,I,P,s) \text { implies }\textsf {tr}(N,I,P,s) \end{aligned}$$

$\blacksquare$

Although the preorders in Definitions 4 and 5 are interesting in their own right, we define the following relation as the finest monitor preorder in this paper.

Definition 6

(Monitor Preorder)

$$\begin{aligned} M \sqsubseteq N&\quad \mathop {=}\limits ^\mathbf{\tiny def }\quad M\sqsubseteq _\textsf {pd} N \text { and } M \sqsubseteq _\textsf {dd} N \text { and } M \sqsubseteq _\textsf {tr} N \end{aligned}$$

$\blacksquare$

Example 9

We have $M_\text {any}\not \sqsubseteq M_\text {any}+\varOmega$ because $M_\text {any}\not \sqsubseteq _\textsf {tr} M_\text {any}+\varOmega$, since $\lnot \textsf {tr}(M_\text {any}+\varOmega ,I,P,s)$ for $I=\left\{ c,a\right\}$, $P=c \textsf {!} a . c \textsf {!} a . \textsf {nil}$ and $s =c ! a .\epsilon$. Similarly, we also have $c ! a .{\textsf {end}} \not \sqsubseteq c ! a .{\textsf {end}}+c ! a .{\varOmega }$. $\blacksquare$

Inequalities from the preorders of Definitions 4 and 5 are relatively easy to repudiate. For instance, we can use $P,I$ and $t$ from Example 4 as counter examples to show that $\textsf {pd}(M_5,I,P,t)$ and $\lnot \textsf {pd}(M_3,I,P,t)$, thus disproving $M_5 \sqsubseteq _\textsf {pd} M_3$. However, it is much harder to show that an inequality from these preorders holds because we need to consider monitor behaviour wrt. all possible processes, interfaces and traces. As shown in Examples 6, 7 and 8, this often requires intricate reasoning in terms of the three LTSs defined in Figs. 1 and 2.

5 Characterisation

We define alternative monitor preorders for which positive statements about their inequalities are easier to establish. The new preorders are defined exclusively in terms of the monitor operational semantics of Fig. 2, as opposed to how they are affected by arbitrary processes as in Definition 6 (which considers also the process and instrumentation LTSs). We show that the new preorders coincide with those in Sect. 4. Apart from equipping us with an easier mechanism for determining the inequalities of Sect. 4, the correspondence results provide further insight into the properties satisfied by the preorders of Definitions 4 and 5.

We start with the potential-detection preorder. We first define a restricted monitor LTS that disallows idempotent transitions from verdicts, $w \xrightarrow {\;\alpha \;} w$: these are redundant when considering the monitor operational semantics in isolation. Note, however, that we can still used rule mVer, e.g., to derive $\checkmark +M \xrightarrow {\;\alpha \;}_r \checkmark$.

Definition 7

(Restricted Monitor Semantics). A derived monitor transition, $M \xrightarrow {\;\mu \;}_r N$, is the least relation satisfying the conditions $M \xrightarrow {\;\mu \;} N$ and $M\ne w$. denotes a transition sequence in the restricted LTS. $\blacksquare$

We use the restricted LTS to limit the detecting transition sequences on the left of the implication of Definition 8. However, we permit these transitions to be matched by transition sequences in the original monitor LTS, so as to allow the monitor to the right of the inequality to match the sequence with a prefix of visible actions (which can then be padded by $\checkmark \xrightarrow {\;\alpha \;} \checkmark$ transitions as required).

Definition 8

(Alternative Potential Detection Preorder)

Theorem 2

(Potential-Detection Preorders).  $M \sqsubseteq _\textsf {pd} N \quad \text {iff}\quad M \preceq _\textsf {pd} N$

Example 10

By virtue of Theorem 2, to show that $\varOmega +c ! a .{\checkmark } \sqsubseteq _\textsf {pd} \varOmega +\checkmark$ from (13) of Example 7 holds, we only need to consider , which can be matched by . Similarly, to show $(x ! a .{\textsf {if}\; x \!=\! c\,\textsf {then}\, \checkmark \;\textsf {else}\; \textsf {end} }) \sqsubseteq _\textsf {pd} \checkmark$, we only need to consider , matched by $\checkmark \xrightarrow {\;c ! a \;} \checkmark$.$\blacksquare$

For the remaining characterisations, we require two divergence judgements.

Definition 9

(Divergence and Strong Divergence)

• $M \uparrow$ denotes that M diverges, meaning that it can produce an infinite transition sequence of $\tau$-actions $M\xrightarrow {\;\tau \;} M' \xrightarrow {\;\tau \;} M'' \xrightarrow {\;\tau \;} \ldots$

• $M \Uparrow$ denotes that M strongly diverges, meaning that it cannot produce finite transition sequence of $\tau$-actions $M\xrightarrow {\;\tau \;} M' \xrightarrow {\;\tau \;} \ldots M'' \not \!\xrightarrow {\;\tau \;}$. $\blacksquare$

Lemma 1

$M \xrightarrow {\;\tau \;}\quad \text {implies}\quad M\ne w$

The alternative preorder for deterministic detections, Definition 11 below, is based on three predicates describing the behaviour of a monitor M along a trace $s$. The predicate $\textsf {blk}(M,s)$ describes the potential for M to block before it can complete trace $s$. Predicate $\textsf {fl}(M,s)$ describes the potential for failing after monitoring trace $s$, i.e., an $s$-derivative of M reaches a non-detecting state from which no further $\tau$ actions are possible, or it diverges (implicitly, by Lemma 1, this also implies that the monitors along the diverging sequences are never detecting). Finally $\textsf {nd}(M,s)$ states the existence of a non-detecting $s$-derivative of M.

Definition 10

(Monitor Block, Fail and Non-Detecting)

Note that $\textsf {blk}(M,s)$ implicitly requires $|s | \ge 1$ for the predicate to hold. $\blacksquare$

Corollary 1

$\textsf {blk}(M,s) \quad \text {implies}\quad \forall t \cdot \textsf {blk}(M,s t)$

Definition 11

(Alternative Deterministic Detection Preorder)

$$\begin{aligned} M \preceq _\textsf {dd} N&\;\mathop {=}\limits ^\mathbf{\tiny def }\; \forall s \cdot {\left\{ \begin{array}{ll} \textsf {blk}(N,s) \quad \text {implies}\quad \textsf {blk}(M,s) \text { or } \textsf {fl}(M,s) \\ \textsf {fl}(N,s) \quad \text {implies}\quad \textsf {blk}(M,s) \text { or } \textsf {fl}(M,s) \\ \textsf {nd}(N,s) \quad \text {implies}\quad \textsf {nd}(M,s) \text { or } \textsf {blk}(M,s) \end{array}\right. } \end{aligned}$$

We write $M \simeq _\textsf {dd} N$ to denote the kernel equality ($M \preceq _\textsf {dd} N$ and $N \preceq _\textsf {dd} M$). $\blacksquare$

Theorem 3

(Deterministic-Detection Preorders). $M \sqsubseteq _\textsf {dd} N \;\text {iff}\; M \preceq _\textsf {dd} N$

Example 11

Consider $M=c ? a .{\textsf {end}}+x ! b .{\textsf {end}}$ and $N=c ? a .{\textsf {end}}$. By virtue of Theorem 3, to determine $M \sqsubseteq _\textsf {dd} N$ we prove $M \preceq _\textsf {dd} N$ as follows:

• 1. We have $\textsf {blk}(N,s)$ whenever $s =\alpha s '$ and $\alpha \ne c ? a$. We have two subcases:

  • If $\textsf {match}(x ! b ,\alpha )$ is undefined, we show $\textsf {blk}(M,\alpha s ')$ by first showing that $\textsf {blk}(M,\alpha \epsilon )$ and then generalising the result for arbitrary $s '$ using Corollary 1.

  • If $\exists \sigma \cdot \textsf {match}(x ! b ,\alpha )=\sigma$, we show $\textsf {fl}(M,\alpha s ')$ by first showing $\textsf {fl}(M,\alpha \epsilon )$ and then generalising the result for arbitrary $s '$ using Theorem 1.

• 2. For any $s$, we have $\textsf {fl}(N,c ? a .s)$: we can show $\textsf {fl}(M,c ? a .s)$, again using Theorem 1 to alleviate the proof burden.

• 3. For any $s$, we have $\textsf {nd}(N,c ? a .s)$: the required proof is analogous to the previous case. $\blacksquare$

Example 12

Due to full abstraction (i.e., completeness), we can alternatively disprove $\checkmark \sqsubseteq _\textsf {dd} \tau .{\checkmark }$ from Example 6 by showing that $\checkmark \not \preceq _\textsf {dd} \tau .{\checkmark }$: we can readily argue that whereas $\textsf {nd}(\tau .{\checkmark },\epsilon )$, we cannot show either $\textsf {nd}(\checkmark ,\epsilon )$ or $\textsf {blk}(\checkmark ,\epsilon )$. $\blacksquare$

Example 13

Recall the equalities $\varOmega \cong _\textsf {dd} \varOmega +\checkmark \cong _\textsf {dd} \textsf {rec}\,X.(\tau .{X}+\checkmark )$ claimed in (12) of Example 7. It is arguably easier to determine these equalities by considering only the monitor LTSs to show that $\varOmega \simeq _\textsf {dd} \varOmega +\checkmark \simeq _\textsf {dd} \textsf {rec}\,X.(\tau .{X}+\checkmark )$ since:

• 1. For any $s \ne \epsilon$ we have $\lnot \textsf {blk}(\varOmega ,s)$, $\lnot \textsf {blk}(\varOmega +\checkmark ,s)$ and $\lnot \textsf {blk}(\textsf {rec}\,X.(\tau .{X}+\checkmark ),s)$.

• 2. We only have $\textsf {fl}(\varOmega ,\epsilon )$, $\textsf {fl}(\varOmega +\checkmark ,\epsilon )$ and $\textsf {fl}(\textsf {rec}\,X.(\tau .{X}+\checkmark ),\epsilon )$.

• 3. Similarly, we only have $\textsf {nd}(\varOmega ,\epsilon )$, $\textsf {nd}(\varOmega +\checkmark ,\epsilon )$ and $\textsf {nd}(\textsf {rec}\,X.(\tau .{X}+\checkmark ),\epsilon )$. $\blacksquare$

Remark 2

The alternative preorder in Definition 11 can be optimised further using refined versions of the predicates $\textsf {fl}(M,s)$ and $\textsf {nd}(M,s)$ that are defined in terms of the restricted monitor transitions of Definition 7, as in the case of Definition 3. $\blacksquare$

The alternative transparency preorder, Definition 13 below, is defined in terms of divergence refusals which, in turn, rely on strong divergences from Definition 9. Intuitively, divergence refusals are the set of actions that cannot be performed whenever a monitor reaches a strongly divergent state following the analysis of trace $s$. These actions turn out to be those that are suppressed on a process when instrumented with the resp. monitor.

Definition 12

(Divergence Refusals)

Definition 13

(Alternative Transparency Preorder)

$$\begin{aligned} M \preceq _\textsf {tr} N \,\mathop {=}\limits ^\mathbf{\tiny def }\, \forall s \cdot \textsf {dref}(N,s) \subseteq \textsf {dref}(M,s) \end{aligned}$$

Theorem 4

(Transparency Preorders). $M \sqsubseteq _\textsf {tr} N \quad \text {iff}\quad M \preceq _\textsf {tr} N$

Example 14

Recall monitors $c ! a .$ $\textsf {end}$ and $c ! a .{\textsf {end}}+c ! a .{\varOmega }$ from (15) of Example 8. The inequality $c ! a .{\textsf {end}}+c ! a .{\varOmega } \sqsubseteq _\textsf {tr} c ! a .{\textsf {end}}$ follows trivially from Theorem 4, since $\forall s \cdot \textsf {dref}(c ! a .{\textsf {end}},s)=\emptyset$. The symmetric case, $c ! a .{\textsf {end}} \sqsubseteq _\textsf {tr} c ! a .{\textsf {end}}+c ! a .{\varOmega }$, can also be readily repudiated by plying Theorem 4. Since $\textsf {dref}((c ! a .{\textsf {end}}+c ! a .{\varOmega }), c ! a .\epsilon )=\textsc {Act}$ (and $\textsf {dref}(c ! a .{\textsf {end}},c ! a .\epsilon )=\emptyset$) we trivially obtain a violation of the set inclusion requirements of Definition 13. $\blacksquare$

Example 15

Recall again $\varOmega +\checkmark$ and $\textsf {rec}\,X.(\tau .{X}+\checkmark )$ from (12). We can differentiate between these monitors from a transparency perspective, and Theorem 4 permits us to do this with relative ease. In fact, whereas $\textsf {dref}((\varOmega +\checkmark ),\epsilon )=\textsc {Act}$ (since $\varOmega +\checkmark \xrightarrow {\;\tau \;} \varOmega$ and $\textsf {dref}(\varOmega ,\epsilon ) = \textsc {Act}$) we have $\textsf {dref}((\textsf {rec}\,X.(\tau .{X}+\checkmark )),\epsilon )=\emptyset$; for all other traces $|s | \ge 1$ we obtain empty divergence refusal sets for both monitors. We thus can positively conclude that $\varOmega +\checkmark \sqsubseteq _\textsf {tr} \textsf {rec}\,X.(\tau .{X}+\checkmark )$ while refuting $\textsf {rec}\,X.(\tau .{X}+\checkmark ) \sqsubseteq _\textsf {tr} \varOmega +\checkmark$. $\blacksquare$

Definition 14

(Alternative Monitor Preorder)

$$\begin{aligned} M \preceq N&\quad \mathop {=}\limits ^\mathbf{\tiny def }\quad M\preceq _\textsf {pd} N \text { and } M \preceq _\textsf {dd} N \text { and } M \preceq _\textsf {tr} N \end{aligned}$$

$\blacksquare$

Theorem 5

(Full Abstraction). $M \sqsubseteq N \quad \text {iff}\quad M \preceq N$

6 Conclusion

We have presented a theory for (recogniser) monitors that allows us to substitute a monitor $M_1$ in a monitored process $P \triangleleft \, M_1$ by another monitor $M_2$ while guaranteeing the preservation of a number of monitoring properties relating to (behaviour) detection and monitor interference. The theory is compositional, since it enables us to ensure the preservation of properties by analysing the resp. monitors $M_1$ and $M_2$ in isolation, without needing to consider the process being monitored, P (which may be arbitrarily complex). To the best of our knowledge, it is the first monitor theory of its kind and could be used to alleviate efforts for proving monitors correct e.g., [26]. The concrete contributions are:

• 1. The definition of three monitor preorders, each requiring the preservation of different monitoring properties: Definitions 3, 4 and 5.

• 2. The characterisation of these preorders in terms of alternative preorders that are more tractable, Theorems 2, 3 and 4.

Related and Future Work. The instrumentation relation we consider is adopted from [17] and embodies synchronous instrumentation (where the external actions constituted the monitorable actions). Synchronous instrumentation is the most prevalent method used in monitoring tools (e.g., [1, 9, 14, 25]) because it carries benefits such as timely detections. There are however variants such as asynchronous instrumentation (e.g., [12, 20]) as well as hybrid variations (e.g., [6, 7, 9, 30]). Our theory should be applicable, at least in part, to these variants.

In runtime verification, three-verdict monitors [2, 10, 15, 17] are often considered, where detections are partitioned into acceptances and rejections. The monitors studied here express generic detections only; they are nevertheless maximally expressive for branching-time properties [17]. They also facilitate comparisons with other linear-time preorders (see below). We also expect our theory to extend smoothly to settings with acceptances and rejections.

Our potential and deterministic detection preorders are reminiscent of the classical may and must preorders of [13, 23] and, more recently (for the deterministic detection preorder), of the subcontract relations in [3, 21]. However, these relations differ from ours in a number of respects. For starters, the monitor instrumentation relation of Fig. 2 assigns monitors a passive role whereas the parallel composition relation composing processes (servers in [3, 21]) with tests (clients in [3, 21]) invites tests to interact with the process being probed. Another important difference is that testing preorders typically relate processes, whereas our preorders are defined over the adjudicating entities i.e., the monitors. The closest work in this regard is that of [3], where the authors develop a must theory for clients. Still, there are significant discrepancies between this must theory and our deterministic detection preorder (further to the differencies between the detected (monitored) computations of Definition 2 and the successful computations under tests of [3, 13, 23] as outlined above — success in the compliance relation of [21] is even more disparate). Concretely, in our setting we have equalities such as $c ! a .\checkmark \cong _\textsf {dd} c ! a .\checkmark +c ! b .\textsf {end}$ (see (10) of Example 6), which would not hold in the setting of [3] since their client preorder is sensitive to external choices ($\sqsubseteq _\textsf {dd}$ is not because monitored executions are distinguished by their visible trace). The two relations are in fact incomparable, since divergent processes are bottom elements in the client must preorder of [3], but they are not in $\sqsubseteq _\textsf {dd}$. In fact, we have $\varOmega \not \sqsubseteq _\textsf {dd} \varOmega +\textsf {end}$ in (12) of Example 7 or, more clearly, $\varOmega \not \sqsubseteq _\textsf {dd} \varOmega +\alpha .\textsf {end}$; at an intuitive level, this is because the instrumentation relation of Fig. 2 prioritises silent actions over external actions that cannot be matched by the monitor.

Transparency is usually a concern for enforcement monitors whereby the visible behaviour of a monitored process should not be modified unless it violates some specified property [5, 15, 28]. We adapted this concept to recognisers, whereby the process behaviour should never be suppressed by the monitor.

To our knowledge, the only body of work that studies monitoring for the piCalculus is [5, 11, 22], and focusses on synthesising adaptation/enforcement monitors from session types. The closest to our work is [5]: their definitions of monitor correctness are however distinctly different (e.g., they are based on branching-time equivalences) and their decomposition methods for decoupling the monitor analysis from that of processes rely on static type-checking.