An Operational Guide to Monitorability

TL;DR

This paper introduces a hierarchical framework for monitorability in runtime verification, explicitly linking properties to monitor guarantees, and unifies existing definitions to improve understanding and design of verification tools.

Contribution

It proposes a monitorability hierarchy with operational and syntactic characterizations, unifying various existing definitions into a rigorous, explicit framework.

Findings

Mapped existing monitorability definitions into the hierarchy

Provided operational and syntactic characterizations for hierarchy levels

Established a unified framework for runtime verification monitorability

Abstract

Monitorability delineates what properties can be verified at runtime. Although many monitorability definitions exist, few are defined explicitly in terms of the guarantees provided by monitors, i.e., the computational entities carrying out the verification. We view monitorability as a spectrum: the fewer monitor guarantees that are required, the more properties become monitorable. We present a monitorability hierarchy and provide operational and syntactic characterisations for its levels. Existing monitorability definitions are mapped into our hierarchy, providing a unified framework that makes the operational assumptions and guarantees of each definition explicit. This provides a rigorous foundation that can inform design choices and correctness claims for runtime verification tools.

Equations

$$\phi ,\psi \in \text{textsc}recHML$$

$$\mid ⟨a⟩\phi$$

$$\begin{array}[]{rlrl}\llbracket\mathsf{tt},\sigma\rrbracket&\,\overset{\leavevmode\resizebox{6.0pt}{}{\,{def}}\,}{=}\,{\textsc{Act}^{\infty}}&\llbracket\mathsf{ff},\sigma\rrbracket&\,\overset{\leavevmode\resizebox{6.0pt}{}{\,{def}}\,}{=}\,\emptyset\\ \llbracket\varphi_{1}\mathbf{\vee}\varphi_{2},\sigma\rrbracket&\,\overset{\leavevmode\resizebox{6.0pt}{}{\,{def}}\,}{=}\,\llbracket\varphi_{1},\sigma\rrbracket\cup\llbracket\varphi_{2},\sigma\rrbracket&\llbracket\varphi_{1}\mathbf{\wedge}\varphi_{2},\sigma\rrbracket&\,\overset{\leavevmode\resizebox{6.0pt}{}{\,{def}}\,}{=}\,\llbracket\varphi_{1},\sigma\rrbracket\cap\llbracket\varphi_{2},\sigma\rrbracket\\ \llbracket\mathbf{[}a\mathbf{]}\varphi,\sigma\rrbracket&\,\overset{\leavevmode\resizebox{6.0pt}{}{\,{def}}\,}{=}\,\left\{f\;|\;f=ag\;\text{ implies }\;g\in\llbracket\varphi,\sigma\rrbracket\right\}&\llbracket\mathbf{\langle}a\mathbf{\rangle}\varphi,\sigma\rrbracket&\,\overset{\leavevmode\resizebox{6.0pt}{}{\,{def}}\,}{=}\,\left\{af\;|\;f\in\llbracket\varphi,\sigma\rrbracket\right\}\\ \llbracket\mathsf{min}\,\!X.\varphi,\sigma\rrbracket&\,\overset{\leavevmode\resizebox{6.0pt}{}{\,{def}}\,}{=}\,\bigcap\left\{\textsl{F}\;|\;\llbracket\varphi,\sigma[X\mapsto\textsl{F}]\rrbracket\subseteq\textsl{F}\ \right\}\par\\ \llbracket\mathsf{max}\,\!X.\varphi,\sigma\rrbracket&\,\overset{\leavevmode\resizebox{6.0pt}{}{\,{def}}\,}{=}\,\bigcup\left\{\textsl{F}\;|\;\textsl{F}\subseteq\llbracket\varphi,\sigma[X\mapsto\textsl{F}]\rrbracket\ \right\}&\llbracket X,\sigma\rrbracket&\,\overset{\leavevmode\resizebox{6.0pt}{}{\,{def}}\,}{=}\,\sigma(X)\\ \\ \end{array}$$

$$\begin{array}[]{rlrlrlr}\textsf{X}\,\varphi&{\,\overset{\leavevmode\resizebox{6.0pt}{}{\,{def}}\,}{=}\,}\bigvee_{a\in\textsc{Act}}\mathbf{\langle}a\mathbf{\rangle}\varphi&\varphi\,\textsf{U}\,\psi&{\,\overset{\leavevmode\resizebox{6.0pt}{}{\,{def}}\,}{=}\,}\mathsf{min}\,Y.\bigl{(}\psi\,\mathbf{\vee}\,(\,\varphi\,\mathbf{\wedge}\,\textsf{X}\ Y)\bigr{)}&\textsf{F}\,\varphi&{\,\overset{\leavevmode\resizebox{6.0pt}{}{\,{def}}\,}{=}\,}\mathsf{tt}\,\textsf{U}\,\varphi\\ \varphi\,\textsf{R}\,\psi&\lx@intercol{\,\overset{\leavevmode\resizebox{6.0pt}{}{\,{def}}\,}{=}\,}\mathsf{max}\,Y.\bigl{(}(\,\psi\,\mathbf{\wedge}\,\varphi\,)\,\mathbf{\vee}\,(\,\psi\,\mathbf{\wedge}\,\textsf{X}\ Y)\bigr{)}\hfil\lx@intercol&\textsf{G}\,\varphi&{\,\overset{\leavevmode\resizebox{6.0pt}{}{\,{def}}\,}{=}\,}\mathsf{ff}\,\textsf{R}\,\varphi\end{array}$$

$$\displaystyle m,n\in\textsc{Mon}\$$

$$v,u\in \text{textsc}Verd$$

$$\phi ,\psi \in \text{textsc}sHML$$

$$\phi ,\psi \in \text{textsc}cHML$$

$$\begin{array}[]{rlrlrl}\textsf{m}(\mathsf{ff})&\,\overset{\leavevmode\resizebox{6.0pt}{}{\,{def}}\,}{=}\,\textsf{no}&\textsf{m}(\varphi_{1}\mathbf{\wedge}\varphi_{2})&\,\overset{\leavevmode\resizebox{6.0pt}{}{\,{def}}\,}{=}\,\textsf{m}(\varphi_{1}){\otimes}\textsf{m}(\varphi_{2})&\textsf{m}(\mathsf{max}\,X.\varphi)&\,\overset{\leavevmode\resizebox{6.0pt}{}{\,{def}}\,}{=}\,\textsf{rec}\,x.\textsf{m}(\varphi)\\ \textsf{m}(\mathsf{tt})&\,\overset{\leavevmode\resizebox{6.0pt}{}{\,{def}}\,}{=}\,\textsf{yes}&\textsf{m}(\varphi_{1}\mathbf{\vee}\varphi_{2})&\,\overset{\leavevmode\resizebox{6.0pt}{}{\,{def}}\,}{=}\,\textsf{m}(\varphi_{1}){\oplus}\textsf{m}(\varphi_{2})&\textsf{m}(\mathsf{min}\,X.\varphi)&\,\overset{\leavevmode\resizebox{6.0pt}{}{\,{def}}\,}{=}\,\textsf{rec}\,x.\textsf{m}(\varphi)\\ \textsf{m}(\mathbf{[}a\mathbf{]}\varphi)&\lx@intercol\textstyle\,\overset{\leavevmode\resizebox{6.0pt}{}{\,{def}}\,}{=}\,a.{\textsf{m}(\varphi)}+\sum_{b\in\textsc{Act}\setminus\left\{a\right\}}b.{\textsf{yes}}\hfil\lx@intercol&\textsf{m}(X)&\,\overset{\leavevmode\resizebox{6.0pt}{}{\,{def}}\,}{=}\,x\\ \textsf{m}(\mathbf{\langle}a\mathbf{\rangle}\varphi)&\lx@intercol\textstyle\,\overset{\leavevmode\resizebox{6.0pt}{}{\,{def}}\,}{=}\,a.{\textsf{m}(\varphi)}+\sum_{b\in\textsc{Act}\setminus\left\{a\right\}}b.{\textsf{no}}\hfil\lx@intercol\end{array}$$

$$=\{{\phi }_1\wedge {\phi }_2\in \text{textsc}recHML\mid {\phi }_1\in \text{textsc}sHML\text{ and }\mathsf{ff}\text{ appears in }{\phi }_1\},$$

$$=\{{\phi }_1\vee {\phi }_2\in \text{textsc}recHML\mid {\phi }_1\in \text{textsc}cHML\text{ and }\mathsf{tt}\text{ appears in }{\phi }_1\}$$

$$\phi \in \text{textsc}eHML$$

$$\mid \phi \vee \psi$$

$$\displaystyle=\left\{\varphi_{1}\land\varphi_{2}\in\textsc{recHML}\Bigm{|}\begin{tabular}[]{l}$\varphi_{1}\in\textsc{sHML}\cap\textsc{eHML}$ and every\\ subformula of $\varphi_{1}$ can refute\end{tabular}\right\}$$

$$\displaystyle=\left\{\varphi_{1}\lor\varphi_{2}\in\textsc{recHML}\Bigm{|}\begin{tabular}[]{l}$\varphi_{1}\in\textsc{cHML}\cap\textsc{eHML}$ and every\\ subformula of $\varphi_{1}$ can verify\end{tabular}\right\}$$

$$\text{f}(\text{no})$$

$$\text{f}(m+n)$$

$$\min S=\{s\in S\mid \forall r\in S.(r\text{ is a prefix of }s\Rightarrow s=r)\}.$$

$$d_B\left(\underset{\gamma \in \text{textsc}Act}{\bigwedge }[\gamma ]{\phi }_{\gamma }\right)$$

$$d_B(X)$$

$$d_B({\phi }_1\wedge {\phi }_2)$$

$$d_B(\max X.{\phi }^{\prime })$$

$$m::=\text{end}\mid \text{no}\mid x\mid \sum _{\alpha \in Act}\alpha .m_{\alpha }\mid \text{rec}x.m.$$

Full text

1 Introduction

Any sufficiently expressive specification language contains properties that cannot be monitored at runtime [33, 35, 23, 21, 27, 2, 5]. For instance, the satisfaction of a safety property (“bad things never happen”) cannot, in general, be determined by observing the (finite) behaviour of a program up to the current execution point; its violation, however, can. Monitorability [13] concerns itself with the delineation between properties that are monitorable and those that are not. Monitorability is paramount for a slew of Runtime Verification (RV) tools, such as those described in [19, 22, 36, 10, 34] (to name but a few), that synthesise monitors from specifications expressed in a variety of logics. These monitors are then executed with the system under scrutiny to produce verdicts concerning the satisfaction or violation of the specifications from which they were synthesised.

Monitorability is crucial for a principled approach because it disciplines the construction of RV tools. It defines, either explicitly or implicitly, a notion of monitor correctness, which guides the automated synthesis. It also delimits the monitorable fragment of the specification logic on which the synthesis is defined: monitors need not be synthesised for non-monitorable specifications. In some settings, a syntactic characterisation of monitorable properties can be identified [27, 1, 5], and used as a core calculus for studying optimisations of the synthesis algorithm. More broadly, monitorability boundaries may guide the design of hybrid verification strategies, which combine RV with other verification techniques (see the work in [2] for an example of this approach).

In spite of its importance, there is no generally accepted notion of monitorability to date. The literature contains a number of definitions, such as the ones proposed in [24, 35, 15, 27, 5]. These differ in aspects such as the adopted specification formalism, e.g., LTL, Street automata, recHML etc., the operational model, e.g., testers, automata, process calculi etc., and the semantic domain, e.g., infinite traces, finite and infinite (finfinite) traces or labelled transition systems. Even after these differences are normalised, many of these definitions are not in agreement: there are properties that are monitorable according to some definitions but not monitorable according to others. More alarmingly, as we will show, frequently cited definitions of monitorability contain serious errors.

This discrepancy between definitions raises the question of which one to adopt to inform one’s implementation of an RV tool, and what effect this choice has on the behaviour of the resulting tool. A difficulty in informing this choice is that few of those definitions make explicit the relationship between the operational model, i.e., the behaviour of a monitor, and the monitored properties. In other words, it is not clear what the guarantees provided by the various monitors mentioned in the literature are, and how they differ from each other.

Example 1.

Consider the runtime verification of a system exhibiting (only) three events over finfinite traces: failure (f), success (s) and recovery (r). One property we may require is that “failure never occurs and eventually success is reached”, otherwise expressed in LTL fashion as $(\textsf{G}\,\neg\textsf{f})\wedge(\textsf{F}\,\textsf{s})$. According to the definition of monitorability attributed to Pnueli and Zaks [35] (discussed in Sec. 7), this property is monitorable. However, it is not monitorable according to others, including Schneider [38], Viswanathan and Kim [39], and Aceto et al. [5], whose definition of monitorability coincides with some subset of safety properties. $\hfill\blacksquare$

Contributions.

To our mind, this state of the art is unsatisfactory for tool construction. An RV tool broadly relies on the following ingredients: $(i)$ the input of the tool in terms of the formalism used to describe the specification properties; $(ii)$ the executable description of monitors that are the tool’s output and $(iii)$ the mapping between the inputs and outputs, i.e., the synthesis function of monitors from specifications. Any account on monitorability should, in our view, shed light on those three aspects, particularly on what it means for the synthesis function and the monitors it produces to be correct. In addition, if this account is flexible enough to incorporate a variety of relationships between specification properties and the expected behaviour of monitors, it can then be used by the tool implementors as a principled foundation to guide their design decisions.

For these reasons, we take the view that monitorability comes on a spectrum. There is a trade-off between the guarantees provided by monitors and the properties that can be monitored with those guarantees. We argue that considering different requirements gives rise to a hierarchy of monitorability—depicted in Fig. 1 (middle)—which classifies properties according to what types of guarantees RV can give for them. At one extreme, anything can be monitored if the only requirement is for monitors to be sound i.e., they should not contradict the monitored specification. However, monitors that are just sound give no guarantees of ever giving a verdict. More usefully, informatively monitorable properties enjoy monitors that reach a verdict for some finite execution; arguably, this is the minimum requirement for making monitoring potentially worthwhile. More stringent requirements can demand this capability to be invariant over monitor executions, i.e., a monitor never reaches a state where it cannot provide a verdict; then we speak of persistently informative monitors. Adding completeness requirements of different strengths, such as the requirement that a monitor should be able to identify all failures and/or satisfactions, yields stronger definitions of monitorability: partial, satisfaction or violation complete, and complete.

In order not to favour a specific operational model, the hierarchy in Fig. 1 (middle) is cast in terms of abstract behavioural requirements for monitors. We then provide an instantiation that concretise those requirements into an operational hierarchy, establishing operational counterparts for each type of monitorability. To this end, we use the operational framework developed in [5]. We show this framework to be, in a suitable technical sense, maximally general (Thm. 4.1). This shows that our work is equally applicable to other operational models.

In order for a tool to synthesise monitors from specifications, it is useful to have syntactic characterisations of the properties that are monitorable with the required guarantees: synthesis can then directly operate on the syntactic fragment. We offer monitorability characterisations as fragments of recHML [32, 6] (a variant of the modal $\mu$-calculus [29]) interpreted over finfinite traces—see Fig. 1 (right). The logic is expressive enough to capture all regular properties—the focus of nearly all existing definitions of monitorability—and subsumes more user-friendly specification logics such as LTL. Partial and complete monitorability already enjoy monitor synthesis functions and neat syntactic characterisations in recHML [5]; related synthesis functions based on syntactic characterisations for a branching-time setting [26, 27] have already been implemented in a tool [10, 9]. Here, we provide the missing syntactic characterisation for informative monitorability, and for a fragment of persistently informative monitorability.

Finally, we show that the proposed hierarchy accounts for existing notions of monitorability. See Fig. 1 (left). Safety, co-safety and their union correspond to partial monitorability and its two components, satisfaction- and violation-monitorability; Pnueli and Zaks’s definition of monitorability can be interpretated in two ways, of which one ($\exists$pz) maps to informative monitorability, and the other ($\forall$pz) to persistently informative monitorability. We also show that the definitions of monitorability proposed by Falcone et al. [24], contrary to their claim, do not coincide with safety and co-safety properties. To summarise, our principal contributions are:

A unified operational perspective on existing notions of monitorability, clarifying what operational guarantees each provides, see Thms. 3.1, 6.1 and 7.1; 2. 2.

An extension to the syntactic characterisations of monitorable classes from [5], mapping all but one of these classes to fragments in recHML, which can be viewed as a target byte-code for higher-level logics, see Thms. 5.2 and 5.3.

Proofs omitted from the body of this paper can be found in Appendix 0.C.

2 Preliminaries

Traces. We assume a finite set of actions, $a,b,\ldots{\in}\textsc{Act}$. The metavariables $t,u{\in}\textsc{Act}^{\omega}$ range over infinite sequences of actions. Finite traces, denoted as $s,r\in\textsc{Act}^{\ast}$, represent finite prefixes of system runs. Collectively, finite and infinite traces ${\textsc{Act}^{\infty}}=\textsc{Act}^{\omega}{\cup}\textsc{Act}^{\ast}$ are called finfinite traces. We use $f,g\in{\textsc{Act}^{\infty}}$ (resp., $\textsl{F}\subseteq{\textsc{Act}^{\infty}}$) to range over finfinite traces (resp., sets of finfinite traces). A (finfinite) trace with action $a$ at its head is denoted as $af$. Similarly, a (finfinite) trace with a prefix $s$ and continuation $f$  is denoted as $sf$. We write $s\preceq f$ to denote that the finite trace $s$ is a prefix of $f$, i.e., $\exists g\cdot f=sg$.

Properties. A property over finfinite (resp., infinite) traces is a subset of ${\textsc{Act}^{\infty}}$ (resp., of $\textsc{Act}^{\omega}$). Simply property refers to a finfinite property, unless stated otherwise. We say that a finite trace $s$ positively (resp., negatively) determines a property $P\subseteq{\textsc{Act}^{\infty}}$ when $sf\in P$ (resp., $sf\notin P$), for every $f\in{\textsc{Act}^{\infty}}$. The same terms apply similarly when $P\subseteq\textsc{Act}^{\omega}$. We call a property regular if it is the union of a regular finite property $P_{f}{\in}\textsc{Act}^{*}$ and an $\omega$-regular infinite property $P_{i}{\in}\textsc{Act}^{\omega}$.

3 A Monitor-Oriented Hierarchy

From a tool-construction perspective, it is important to give concrete, implementable definitions of monitors; we do so in Sec. 4. To understand the guarantees that these monitors will provide, we first discuss the general notion of monitor and monitoring system. Already in this general setting, we are able to identify the various requirements that give rise to the hierarchy of monitorability, depicted in the middle part of Fig. 1. Sec. 4 will then provide operational semantics to this hierarchy, in the setting of regular properties.

We consider a monitor to be an entity that analyses finite traces and (at the very least) identifies a set of finfinite traces that it accepts and a set of finfinite traces that it rejects. We consider two postulates. Firstly, an acceptance or rejection verdict has to be based on a finite prefix of a trace, Def. 1.1; secondly, verdicts must be irrevocable, Def. 1.2. These postulates make explicit two features shared by most monitorability definitions in the literature.

Definition 1.

A monitoring system is a triple $(M,\textbf{acc},\textbf{rej})$, where $M$ is a nonempty set of monitors, $\textbf{acc},\textbf{rej}\subseteq M{\times}{\textsc{Act}^{\infty}}$, and for every $m\in M$:

\bigl{(}\,\textbf{acc}(m,f)\text{ implies }\exists s\cdot\bigl{(}s\preceq f\text{ and }\textbf{acc}(m,s)\bigr{)}\,\bigr{)} and \bigl{(}\,\textbf{rej}(m,f)\text{ implies }\exists s\cdot\bigl{(}s\preceq f\text{ and }\textbf{rej}(m,s)\bigr{)}\,\bigr{)}; 2. 2.

\bigl{(}\textbf{acc}(m,s)\text{ implies }\forall f{\cdot}\textbf{acc}(m,sf)\bigr{)} and \bigl{(}\textbf{rej}(m,s)\text{ implies }\forall f{\cdot}\textbf{rej}(m,sf)\bigr{)}. $\hfill\blacksquare$

Remark 1.

Finite automata do not satisfy the requirements of Def. 1 since their judgement can be revoked. Standard Büchi automata are not good candidates either, since they need to read the entire infinite trace to accept or reject. $\hfill\blacksquare$

We define a notion of maximal monitoring system for a collection of properties; for each property $P$ in that set, such a system must contain a monitor that reaches a verdict for all traces that have some prefix that determines $P$.

Definition 2.

A monitoring system $(M,\textbf{acc},\textbf{rej})$ is maximal for a collection of properties $C\subseteq 2^{{\textsc{Act}^{\infty}}}$ if for every $P\in C$ there is a monitor $m_{P}\in M$ such that $(i)$ $\textbf{acc}(m_{P},f)$ iff trace $f$ has a prefix that positively determines $P$; $(ii)$ $\textbf{rej}(m_{P},f)$ iff trace $f$ has a prefix that negatively determines $P$. $\hfill\blacksquare$

In Sec. 4, we present an instance of such a maximal monitoring system for regular properties. This shows that, for regular properties at least, the maximality of a monitoring system is a reasonable requirement. Unless otherwise stated, we assume a fixed maximal monitoring system $(M,\textbf{acc},\textbf{rej})$ throughout the rest of the paper. For $m{\in}M$ to monitor for a property $P$, it needs to satisfy some requirements. The most important such requirement is soundness.

Definition 3 (Soundness).

Monitor $m$ is sound for property $P$ when $\textbf{acc}(m,f)$ implies $f\in P$, and $\textbf{rej}(m,f)$ implies $f\notin P$. $\hfill\blacksquare$

Lemma 1.

If $m$ is sound for $P$ and $\textbf{acc}(m,s)$ (resp., $\textbf{rej}(m,s)$), then $s$ positively (resp., negatively) determines $P$.

Lemma 2.

For every $P\subseteq{\textsc{Act}^{\infty}}$: $(i)$ $m_{P}$ is sound for $P$; and $(ii)$ if $m$ is a sound monitor for $P$ and $\textbf{acc}(m,f)$ (resp., $\textbf{rej}(m,f)$), then it is also the case that $\textbf{acc}(m_{P},f))$ (resp., $\textbf{rej}(m_{P},f))$).

The dual requirement to soundness, i.e., completeness, entails that the monitor detects all violating and satisfying traces. Unfortunately, this is only possible for trivial properties in the finfinite111In the infinite domain more properties are completely monitorable, see Sec. 8. domain—see Prop. 1. Instead, monitors may be required to accept all satisfying traces, or reject all violating traces.

Definition 4 (Completeness).

Monitor $m$ is satisfaction-complete for $P$ if $f{\in}P$ implies $\textbf{acc}(m,f)$ and violation-complete for $P$ if $f{\notin}P$ implies $\textbf{rej}(m,f)$. It is complete for $P$ if it is both satisfaction- and violation-complete for $P$ and partially-complete if it is either satisfaction- or violation-complete. $\hfill\blacksquare$

Proposition 1.

If $m$ is sound and complete for $P$ then $P{=}{\textsc{Act}^{\infty}}$ or $P{=}\emptyset$.

Proof.

If $\varepsilon\in P$, then $\textbf{acc}(m,\varepsilon)$, so from Def. 1, $\forall f\in{\textsc{Act}^{\infty}}.~{}\textbf{acc}(m,f)$. Due to the soundness of $m$, $P={\textsc{Act}^{\infty}}$. Similarly, $P=\emptyset$ when $\varepsilon\notin P$. ∎

We define monitorability in terms of the guarantees that the monitors are expected to give. Soundness is not negotiable. Given the consequences of requiring completeness, as evidenced by Prop. 1, we consider weaker forms of completeness. The weaker the completeness guarantee, the more properties can be monitored.

Definition 5 (Complete Monitorability).

Property $P$ is completely monitorable when there is a monitor that is sound and complete for $P$. It is monitorable for satisfactions (resp., violations) when there is a monitor $m$ that is sound and satisfaction- (resp., and violation-) complete for $P$. It is partially monitorable when it is monitorable for satisfactions or violations.

A class of properties $C\subseteq 2^{\textsc{Act}^{\infty}}$ is satisfaction-, violation-, partially, or completely monitorable, when every property $P{\in}C$ is, respectively, satisfaction-, violation, partially or completely monitorable. We denote the class of all satisfaction, violation, partially, and completely monitorable properties by maximal monitoring systems as SCmp, VCmp, PCmp, and Cmp, respectively. $\hfill\blacksquare$

Since even partial monitorability, the weakest form in Def. 5, renders a substantial number of properties unmonitorable [5], one may consider even weaker forms of completeness that only flag a subset of satisfying (or violating) traces. Sound denotes monitorability without completeness requirements. Arguably, however, the weakest guarantee for a sound monitor of a property $P$ to be of use is if it flags at least one trace. One may then further strengthen this requirement and demand that this guarantee is invariant throughout the analysis of a monitor.

Definition 6 (Informative Monitors222These are not related to the informative prefixes from [30] nor persistence from [37]).

Monitor $m$ is satisfaction- (resp., violation-) informative if $\exists f\cdot\textbf{acc}(m,f)$ (resp., $\textbf{rej}(m,f)$). It is satisfaction- (resp., violation-) persistently informative if $\forall s\exists f\cdot\textbf{acc}(m,sf)$ (resp., $\textbf{rej}(m,sf)$). We simply say that $m$ is informative (resp., persistently informative) when we do not distinguish between satisfactions or violations. $\hfill\blacksquare$

Definition 7 (Informative Monitorability).

Property $P$ is informatively (resp., persistently informatively) monitorable if there is an informative (resp., a persistently informative) monitor that is sound for $P$. A class of properties $C{\subseteq}2^{\textsc{Act}^{\infty}}$ is informatively (resp., persistently informatively) monitorable, when all its properties are informatively (resp., persistently informatively) monitorable. The class of all informatively (resp., persistently informatively) monitorable properties by maximal monitoring systems is denoted as ICmp (resp., PICmp). A property $P$ is persistently informatively monitorable for satisfaction (resp., for violation) if there is a satisfaction- (resp., violation-) persistently informative monitor that is sound for $P$. We revisit this definition in Sec. 4. $\hfill\blacksquare$

Example 2.

The property “f never occurs and eventually s is reached” (Example 1) is not partially monitorable but is persistently informatively monitorable.

The property requiring that “r only appears a finite number of times” is not informatively monitorable. For if it were, the respective sound informative monitor $m$ should at least accept or reject one trace. If it accepts a trace $f$, by Def. 1, it must accept some prefix $s\preceq f$. Again, by Def. 1, all continuations, including $s\textsf{r}^{\omega}$, must be accepted by $m$. This makes it unsound, which is a contradiction. Similarly, if $m$ rejects some $f$, it must reject some finite $s\preceq f$ that necessarily contains a finite number of r actions, making it unsound. $\hfill\blacksquare$

Theorem 3.1 (Monitorability Hierarchy).

The monitorability classes given in Defs. 5 and 7 form the inclusion hierarchy depicted in Fig. 1.

Proof.

The hardest inclusion to show is $\textsf{PCmp}=\textsf{SCmp}{\cup}\textsf{VCmp}\subseteq\textsf{PICmp}$. Pick a property $P\in\textsf{VCmp}$. Let $s\in\textsc{Act}^{*}$. If $\exists f\cdot sf\notin P$ then by Def. 4 we have $\textbf{rej}(m_{P},sf)$. Otherwise, $\forall f\cdot sf\in P$, meaning that $s$ positively determines $P$, and by Def. 2 we have $\textbf{acc}(m_{P},sf)$. By Def. 6, we deduce that $m_{P}$ is persistently informative since $\forall s\exists f\cdot\textbf{acc}(m_{P},sf)\text{ or }\textbf{rej}(m_{P},sf))$. Thus, by Def. 7, it follows that $P\in\textsf{PICmp}$. The case for $P\in\textsf{SCmp}$ is dual. ∎

4 An Instantiation for Regular Properties

We provide a concrete maximal monitoring system for regular properties . This monitoring system that gives an operational interpretation to the levels of the monitorability hierarchy, and enables us to find syntactic characterisations for them in recHML [32, 5]. Since this logic is a reformulation of the modal $\mu$-calculus [29], it is expressive enough to describe all regular properties and to embed specification formalisms such as LTL, ($\omega$-)regular expressions, Büchi automata, and Street automata, used in the state of the art on monitorability.

The Logic.

The syntax or recHML is defined by the grammar in Fig. 2, which assumes a countable set of logical variables $X,Y\in\textsc{LVar}$. Apart from the standard constructs for truth, falsehood, conjunction and disjunction, the logic is equipped with existential ($\mathbf{\langle}a\mathbf{\rangle}\varphi$) and universal ($\mathbf{[}a\mathbf{]}\varphi$) modal operators, and two recursion operators expressing least and greatest fixpoints (resp., $\mathsf{min}\,X.\varphi$ and $\mathsf{max}\,X.\varphi$). The semantics is given by the function $\llbracket-\rrbracket$ defined in Fig. 2. It maps a (possibly open) formula to a set of (finfinite) traces [5] by induction on the formula structure, using valuations that map logical variables to sets of traces, $\sigma:\textsc{LVar}\to\mathcal{P}({\textsc{Act}^{\infty}})$, where $\sigma(X)$ is the set of traces assumed to satisfy $X$. An existential modality $\mathbf{\langle}a\mathbf{\rangle}\varphi$ denotes all traces with a prefix action $a$ and a continuation that satisfies $\varphi$ whereas a universal modality $\mathbf{[}a\mathbf{]}\varphi$ denotes all traces that are either not prefixed by $a$ or have a continuation $g$ satisfying $\varphi$. The sets of traces satisfying the least and greatest fixpoint formulae, $\mathsf{min}\,X.\varphi$ and $\mathsf{max}\,X.\varphi$, are the least and the greatest fixpoints, respectively, of the function induced by the formula $\varphi$. For closed formulae, we use $\llbracket\varphi\rrbracket$ in lieu of $\llbracket\varphi,\sigma\rrbracket$ (for some $\sigma$). Formulae are generally assumed to be closed and guarded [31]. In the discussions we occasionally treat formulae, $\varphi$, as the properties they denote, $\llbracket\varphi\rrbracket$.

Example 3.

The characteristic LTL operators can be encoded in recHML as:

[TABLE]

In examples, atomic propositions $a$ and $\neg a$ resp., denote $\mathbf{\langle}a\mathbf{\rangle}\mathsf{tt}$ and $\mathbf{[}a\mathbf{]}\mathsf{ff}$. $\hfill\blacksquare$

For better readability, examples use LTL. Since we operate in the finfinite domain, X should be read as a strong next operator, in line with Example 3.

The Monitors.

We consider the operational monitoring system of [27, 5], summarised in Fig. 3 (symmetric rules for binary operators are omitted). The full system is given in Appendix 0.B. Monitors are states of a transition system where $m+n$ denotes an (external) choice and $m{\odot}n$ denotes a composite monitor where ${\odot}\in\left\{{\oplus},{\otimes}\right\}$. There are three distinct verdict states, yes, no, and end, although only the first two are relevant to monitorability. This semantics gives an operational account of how a monitor in state $m$ incrementally analyses a sequence of actions $s=a_{1}\ldots a_{k}$ to reach a new state $n$; the monitor $m$ accepts (resp., rejects) a trace $f$, $\textbf{acc}(m,f)$ (resp., $\textbf{rej}(m,f)$), when it can transition to the verdict state yes (resp., no) while analysing a prefix $s\preceq f$. Since verdicts are irrevocable (rule mVer in Fig. 3), it is not hard to see that this operational framework satisfies the conditions for a monitoring system of Def. 1. The monitoring system of Fig. 3 is also maximal for regular properties, according to Def. 2. This concrete instance thus demonstrates the realisability of the abstract definitions in Sec. 3.

Theorem 4.1.

For all $\varphi{\in}\textsc{recHML}$, there is a monitor $m{\in}\textsc{Mon}$ that is sound for $\varphi$ and accepts all finite traces that positively determine $\varphi$ and rejects all finite traces that negatively determine $\varphi$.

As a corollary of Thm. 4.1, from Lem. 1 we deduce that for any arbitrary monitoring system $(M,\textbf{acc},\textbf{rej})$, if $m\in M$ is sound for some $\varphi\in\textsc{recHML}$, then there is a monitor $n\in\textsc{Mon}$ from Fig. 3 that accepts (resp., rejects) all traces $f$ that $m$ accepts (resp., rejects). In the sequel, we thus assume that the fixed monitoring system is $(\textsc{Mon},\textbf{acc},\textbf{rej})$ of Fig. 3, as it subsumes all others.

5 A Syntactic Characterisation of Monitorability

We present syntactic characterizations for the various monitorability classes as fragments of recHML.

Partial Monitorability, syntactically.

In [5] Aceto et al. identify a maximal partially monitorable syntactic fragment of recHML.

Theorem 5.1 (Partial Monitorability [5]).

Consider the fragments:

[TABLE]

The fragment sHML is monitorable for violation whereas cHML is monitorable for satisfaction. Furthermore, if $\varphi\in\textsc{recHML}$ is monitorable for satisfaction (resp., for violation) by some $m{\in}\textsc{Mon}$, then it is expressible in cHML(resp., sHML) , i.e., $\exists\psi{\in}\textsc{cHML}$ (resp., $\psi{\in}\textsc{sHML}$), such that $\llbracket\varphi\rrbracket{=}\llbracket\psi\rrbracket$.

As a corollary of Thm. 5.1, any $\varphi\in\textsc{recHML}$ that is monitorable for satisfaction (resp., for violation) can also be expressed as some $\psi\in\textsc{cHML}$ (resp., $\psi\in\textsc{sHML}$) where $\llbracket\varphi\rrbracket=\llbracket\psi\rrbracket$. For this fragment, the following automated synthesis function, which is readily implementable, is given in [5].

[TABLE]

Informative Monitorability, syntactically.

We proceed to identify syntactic fragments of recHML that correspond to informative monitorability.

Definition 8.

The informative fragment is $\textsc{iHML}=\textsc{siHML}\cup\textsc{ciHML}$ where

[TABLE]

Theorem 5.2.

For $\varphi\in\textsc{recHML}$, $\varphi$ is informatively monitorable if and only if there is some $\psi\in\textsc{iHML}$, such that $\llbracket\psi\rrbracket=\llbracket\varphi\rrbracket$.

Example 4.

$\textsf{G}\,\neg\textsf{f}\land\textsf{F}\,\textsf{s}$ from Example 2 (expressed here in LTL) is a siHML property, as $\textsf{G}\neg\textsf{f}$ can be written in sHML as $\mathsf{max}\,X.\mathbf{[}\textsf{f}\mathbf{]}\mathsf{ff}\mathbf{\wedge}\mathbf{[}\textsf{s}\mathbf{]}X\mathbf{\wedge}\mathbf{[}\textsf{r}\mathbf{]}X$. In contrast, $\textsf{F}\textsf{G}\neg\textsf{r}$ cannot be written in iHML, as it is not informatively monitorable. $\hfill\blacksquare$

Remark 2.

In siHML and ciHML, $\varphi_{1}$ describes an informative part of the formula, that is, a formula with at least one path to $\mathsf{tt}$ (or $\mathsf{ff}$), which indicates that the corresponding finite trace determines the property. Monitor synthesis from these fragments can use this part of the formula to synthesize a monitor that detects the finite traces that satisfy (violate) $\varphi_{1}$. The value of the synthesised monitor then depends on $\varphi_{1}$. It is therefore important to have techniques to extract some $\varphi_{1}$ that will retain as much monitoring information as possible. This extraction is outside the scope of this paper and left as future work. $\hfill\blacksquare$

Persistently Informative Monitorability, syntactically.

We also give a syntactic characterization of the recHML properties that are persistently informatively monitorable for satisfaction or violation. As the requirements for persistently informative monitors are more subtle than for informative monitors, the fragments we present are equally more involved than those for informative monitorability.

Definition 9.

We define eHML, the explicit fragment of recHML:

[TABLE]

Example 5.

Formula $\mathbf{[}\textsf{f}\mathbf{]}\mathbf{[}\textsf{s}\mathbf{]}\mathsf{ff}$ is not explicit, but it can be rewritten as the explicit formula $\mathbf{[}\textsf{f}\mathbf{]}(\mathbf{[}\textsf{s}\mathbf{]}\mathsf{ff}\land\mathbf{[}\textsf{f}\mathbf{]}\mathsf{tt}\land\mathbf{[}\textsf{r}\mathbf{]}\mathsf{tt})\land\mathbf{[}\textsf{s}\mathbf{]}\mathsf{tt}\land\mathbf{[}\textsf{r}\mathbf{]}\mathsf{tt}$. $\hfill\blacksquare$

Roughly, the following definition captures whether $\mathsf{tt}$ and $\mathsf{ff}$ are reacheable from subformulae (where the binding of a variable is reachable from the variable).

Definition 10.

Given a closed sHML (resp., cHML) formula $\varphi$, we define for a subformula $\psi$ that it can refute (resp., verify) in 0 unfoldings, when $\mathsf{ff}$ (resp., $\mathsf{tt}$) appears in $\psi$, and that it can refute (resp., verify) in $k+1$ unfoldings, when it can refute (resp., verify) in $k$ unfoldings, or $X$ appears in $\psi$ and $\psi$ is in the scope of a subformula $\max X.\psi^{\prime}$ (resp., $\min X.\psi^{\prime}$) that can refute (resp., verify) in $k$ unfoldings. We simply say that $\psi$ can refute (resp., verify) when it can refute (resp., verify) in $k$ unfoldings, for some $k\geq 0$. $\hfill\blacksquare$

Example 6.

For formula $\mathsf{max}\,X.\mathbf{[}\textsf{s}\mathbf{]}X\land\mathbf{[}\textsf{f}\mathbf{]}\mathsf{ff}\land\mathbf{[}\textsf{r}\mathbf{]}\mathsf{ff}$, subformula $\mathbf{[}\textsf{s}\mathbf{]}X\land\mathbf{[}\textsf{f}\mathbf{]}\mathsf{ff}\land\mathbf{[}\textsf{r}\mathbf{]}\mathsf{ff}$ can refute in [math] unfoldings. In contrast, $\mathbf{[}\textsf{s}\mathbf{]}X$ cannot refute in [math] unfoldings, but it can refute in 1, because $X$ appears in it and $\mathsf{max}\,X.\mathbf{[}\textsf{s}\mathbf{]}X\land\mathbf{[}\textsf{f}\mathbf{]}\mathsf{ff}\land\mathbf{[}\textsf{r}\mathbf{]}\mathsf{ff}$ can refute in [math] unfoldings. Therefore, all subformulae of $\mathsf{max}\,X.\mathbf{[}\textsf{s}\mathbf{]}X\land\mathbf{[}\textsf{f}\mathbf{]}\mathsf{ff}\land\mathbf{[}\textsf{r}\mathbf{]}\mathsf{ff}$ can refute. $\hfill\blacksquare$

We now define the fragments of recHML corresponding to recHML properties that are persistently informatively monitorable for satisfaction or violation.

Definition 11.

We define the fragment $\textsc{pHML}=\textsc{spHML}\cup\textsc{cpHML}$ where:

[TABLE]

Theorem 5.3.

For $\varphi\in\textsc{recHML}$, $\varphi$ is persistently informatively monitorable for violation (resp., for satisfaction) if and only if there is some $\psi\in\textsc{spHML}$ (resp., $\psi\in\textsc{cpHML}$), such that $\llbracket\psi\rrbracket=\llbracket\varphi\rrbracket$.

Remark 3.

To the best of our efforts, a syntactic characterisation of persistently informative monitorability would involve pairs of equivalent formulae with parts from sHML and cHML that together become, in some sense, explicit. We leave such a characterization as future work. $\hfill\blacksquare$

6 Safety and Co-safety

The classic (and perhaps the most intuitive) definition of monitorability consists of (some variation of) safety properties [7, 38, 39, 24, 5]. Nevertheless, there are subtleties associated with how exactly safety properties are defined—particularly over the finfinite domain—and how decidable they need to be to qualify as truly monitorable. For example, Kim and Viswanathan [39] argued that only recursively enumerable safety properties are monitorable (they restrict themselves to infinite, rather than finfinite traces). By and large, however, most works on monitorability restrict themselves to regular properties, as we do in Sec. 4.

We adopt the definition of safety that is intuitive for the context of RV: a property can be considered monitorable if its failures can be identified by a finite prefix. This is equivalent to Falcone et al.’s formal definition of safety properties[24, Def. 4] and work such as [7, 18] when restricted to infinite traces.

Definition 12 (Safety).

A property $P\subseteq{\textsc{Act}^{\infty}}$ is a safety property if every $f\notin P$ has a prefix, $s$ that determines $P$ negatively. The class of safety properties is denoted as Safe in Fig. 1. $\hfill\blacksquare$

Pnueli and Zaks, and Falcone et al. (among others) argue that it makes sense to monitor both for violation and satisfaction. Hence, if safety is monitorable for violations, then the dual class, co-safety (a.k.a. guarantee [24], reachability [17]), is monitorable for satisfaction. That is, every trace that satisfies a co-safety property can be positively determined by a finite prefix.

Definition 13 (Co-safety).

A property $P\subseteq{\textsc{Act}^{\infty}}$ is a co-safety property if every $f\in P$ has prefix, $s$, that determines $P$ positively. The class of safety properties is denoted as CoSafe, also represented in Fig. 1. $\hfill\blacksquare$

Example 7.

“Eventually s is reached”, i.e., F s, is a co-safety property whereas “f never occurs”, i.e., $\textsf{G}\,\neg\textsf{f}$, is a safety property. The property “s occurs infinitely often”, i.e., G F s, is neither safety nor co-safety. The property only holds over infinite traces so it cannot be positively determined by a finite trace. Dually, there is no finite trace that determines that there cannot be an infinite number of s occurrences in a continuation of the trace. $\hfill\blacksquare$

Safety and Co-safety, operationally.

It should come as no surprise that safety and co-safety coincide with an equally natural operational definition. Here, we establish the correspondence with the denotational definition of safety (co-safety), completing three correspondences amongst the monitorability classes of Fig. 1

Theorem 6.1.

$\textsf{VCmp}=\textsf{Safe}$* and $\textsf{SCmp}=\textsf{CoSafe}$.*

Proof.

We treat the case for safety, as the case for co-safety is similar. If $P$ is a safety property, then for every $f\in{\textsc{Act}^{\infty}}\setminus P$, there is some finite prefix $s$ of $f$ that negatively determines $P$. Therefore, $m_{P}$ is sound (Lem. 2) and violation-complete (Def. 2) for $P$. The other direction follows from Lem. 5. ∎

Aceto et al. [5] already show the correspondence between violation (dually, satisfaction) monitorability over finfinite traces and properties expressible in sHML (dually, cHML). As a corollary of Thm. 6.1, we obtain a syntactic characterisation for the Safe and CoSafe monitorability classes.

Remark 4.

Falcone et al. [24, Def. 17, Thm. 3] propose definitions of monitorability over finfinite traces that are claimed to coincide with the classes Safe, CoSafe and their union. However, this claim is incorrect. The properties, “the trace is finite” and G F s from Example 7 are neither safety nor co-safety properties. On the other hand, they are monitorable according to the alternative monitorability definition given in [24, Def. 17]. If the results claimed in [24, Thm. 3] held true, this would contradict the fact that those properties are neither safety nor co-safety properties. See Appendix 0.A for further details. $\hfill\blacksquare$

7 Pnueli and Zaks

The work on monitorability due to Pnueli and Zaks [35] is often cited by the RV community [13]. The often overlooked particularity of their definitions is that they only define monitorability of a property with respect to a (finite) sequence.

Definition 14 ([35]).

Property $P$ is $s$-monitorable, where $s\in\textsc{Act}^{*}$, if there is some $r\in\textsc{Act}^{*}$ such that $P$ is positively or negatively determined by $sr$. $\hfill\blacksquare$

Example 8.

The property \bigl{(}\textsf{f}\land\textsf{F}\,\textsf{r}\bigr{)}\vee\bigl{(}\textsf{F}\,\textsf{G}\,\textsf{s}\bigr{)} is $s$-monitorable for any finite trace that begins with f, i.e., $\textsf{f}s$, since it is determined by the extension $\textsf{f}s\textsf{r}$. It is not $s$-monitorable for finite traces that begin with an action other than f. $\hfill\blacksquare$

Monitorability over properties—rather than over property–sequence pairs—can then be defined by either quantifying universally or existentially over finite traces: a property is monitorable either if it is $s$-monitorable for all $s$, or for some $s$. We address both definitions, which we call $\forall$pz- and $\exists$pz-monitorability respectively. $\forall$pz-monitorability is the more standard interpretation: it appears for example in [24, 14] where it is attributed to Pnueli and Zaks. However, the original intent seems to align more with $\exists$pz-monitorability: in [35], Pnueli and Zaks refer to a property as non-monitorable if it is not monitorable for any sequence. This interpretation coincides with weak monitorability used in [20].

Definition 15 ($\forall$pz-monitorability).

A property $P$ is (universally Pnueli–Zaks) $\forall$pz-monitorable if it is $s$-monitorable for all finite traces $s$. The class of all $\forall$pz-monitorable properties is denoted $\forall$PZ. $\hfill\blacksquare$

Definition 16 ($\exists$pz-monitorability).

A property is (existentially Pnueli–Zaks) $\exists$pz-monitorable if it is $s$-monitorable for some finite trace $s$, i.e., if it is $\varepsilon$-monitorable. The class of $\exists$pz-monitorable properties is written $\exists$PZ. $\hfill\blacksquare$

The apparently innocuous choice between existential and universal quantification leads to different monitorability classes $\forall$PZ and $\exists$PZ.

Example 9.

Consider the property “Either s occurs before f, or r happens infinitely often”, expressed in LTL fashion as \bigl{(}(\neg\textsf{f})\,\textsf{U}\,\textsf{s}\bigr{)}\vee\bigl{(}\textsf{G}\,\textsf{F}\,\textsf{r}\bigr{)}. This property is $\exists$pz-monitorable because every finite trace $s\textsf{f}$ positively determines the property. However, it is not $\forall$pz-monitorable because no extension of the trace f positively or negatively determines that property. Indeed, all extensions of f violate the first disjunct and, as we argued in Example 7, there is no finite trace that determines the second conjunct positively or negatively. $\hfill\blacksquare$

From Defs. 15 and 16, it follows immediately that \textsf{\forallPZ}\subset\textsf{\existsPZ}.

Proposition 2.

All properties in $\textsf{Safe}\cup\textsf{CoSafe}$ are $\forall$pz-monitorable.

Proof.

Let $P\in\textsf{Safe}$ and pick a finite trace $s$. If there is an $f$ such that $sf\notin P$ then, by Def. 12, there exists $r\preceq sf$ that negatively determines $P$, meaning that $s$ has an extension that negatively determines $P$. Alternatively, if there is no $f$ such that $sf\notin P$, $s$ itself positively determines $P$. Hence $P$ is $s$-monitorable, for every $s$, according to Def. 14. The case for $P\in\textsf{CoSafe}$ is dual. ∎

Pnueli and Zaks, operationally.

$\exists$pz-monitorability coincides with informative monitorability: $\exists$pz-monitorable properties are those for which some monitor can reach a verdict on some finite trace. For similar reasons, $\forall$pz-monitorability coincides with persistently informative monitorability. See Fig. 1.

Theorem 7.1.

\textsf{\existsPZ}=\textsf{ICmp}* and \textsf{\forallPZ}=\textsf{PICmp}.*

Proof.

Since the proofs of the two claims are analogous, we simply outline the one for \textsf{\forallPZ}=\textsf{PICmp}. Let P\in\textsf{\forallPZ} and pick a finite trace $s\in\textsc{Act}^{*}$. By Lem. 2, $m_{P}$ is sound for $P$. By Def. 6 we need to show that there exists an $f$ such that $\textbf{acc}(m_{P},sf)$ or $\textbf{rej}(m_{P},sf)$. From Defs. 15 and 14 we know that there is a finite $r$ such that $sr$ positively or negatively determines $P$. By Def. 2 we know that $\textbf{acc}(m_{P},sr)$ or $\textbf{rej}(m_{P},sr)$. Thus $P\in\textsf{PICmp}$, which is the required result.

Conversely, assume $P\in\textsf{PICmp}$, and pick a $s\in\textsc{Act}^{*}$. By Defs. 15 and 14, we need to show that there is an extension of $s$ that positively or negatively determines $P$. From Defs. 6 and 7, there exists a $f$ such that $\textbf{acc}(m_{P},sf)$ or $\textbf{rej}(m_{P},sf)$. By Def. 1, there is a finite extension of $s$, say $sr$, that is a prefix of $sf$ such that $\textbf{acc}(m_{P},sr)$ or $\textbf{rej}(m_{P},sr)$. By Def. 2, we know that $sr$ either positively or negatively determines $P$. Thus P\in\textsf{\forallPZ}. ∎

8 Monitorability in other settings

We have shown how classical definitions of monitorability fit into our hierarchy and provided the corresponding operational interpretations and syntactic characterisations, focussing on regular finfinite properties over a finite alphabet and monitors with irrevocable verdicts. Here we discuss how different parameters, both within our setting and beyond, affect what is monitorable.

Monitorability with respect to the alphabet.

The monitorability of a property can depend on Act. For instance, if Act has at least two elements $\left\{a,b,\ldots\right\}$, property $\{a^{\omega}\}$, which can be represented as $\textsf{max}~{}X.\langle a\rangle X$, is $s$-monitorable for every sequence $s$, as $s$ can be extended to $sb$, which negatively determines the property. On the other hand, assume that $\textsc{Act}=\{a\}$. In this case, $\{a^{\omega}\}$ is neither $\exists$pz- nor $\forall$pz-monitorable. Indeed, no string $s=a^{k}$, $k\geq 0$, determines $\{a^{\omega}\}$ positively or negatively as $s$ does not satisfy $p$ but its extension $a^{\omega}$ does. On the other hand, when restricted to infinite traces, $p$ is again $\exists$pz-monitorable.

So far, we only considered finite alphabets; how an infinite alphabet, which may encode integer data for example, affects monitorability is left as future work.

Monitoring with revocable verdicts.

Early on, we postulated that verdicts are irrevocable. Although this is a typical (implicit) assumption in most work on monitorability, some authors have considered monitors that give revocable judgements when an irrevocable one is not appropriate. This approach is taken by Bauer et al. when they define a finite-trace semantics for LTL, called RV-LTL [14]. Falcone et al. [24] also have a definition of monitorability based on this idea (in addition to those discussed in Remark 4). It uses the four-valued domain $\{\textsf{yes},\textsf{no},\textsf{yes}_{c},\textsf{no}_{c}\}$ ($c$ for currently). Finite traces that do not determine a property yield a (revocable) verdict $\textsf{yes}_{c}$ or $\textsf{no}_{c}$ that indicates whether the trace observed so far satisfies the property; yes and no are still irrevocable. This definition allows all finfinite properties to be monitored since it does not require verdicts to be irrevocable.

This type of monitoring does not give any guarantees beyond soundness: there are properties that are monitorable according to this definition for which no sound monitor ever reaches an irrevocable verdict: F G s for the system from Example 1 has no sound informative monitor, yet can be monitored according to Falcone et al.’s four-valued monitoring. This type of monitorability is complete, in the sense of providing at least a revocable verdict for all traces.

Monitorability in the infinite and finite.

Bauer et al. use $\forall$pz-monitorability in their study of runtime verification for LTL  [16] and attribute it to Pnueli and Zaks. However, unlike Falcone et al., Pnueli and Zaks [35] and ourselves, they focus on properties over infinite traces. There are some striking differences that arise if there is no risk of an execution ending. Aceto et al. show that, unlike in the finfinite domain, a set of non-trivial properties becomes completely monitorable: HML [28] (a.k.a. modal logic) is both satisfaction- and violation-monitorable over infinite traces [5]. Furthermore, some properties, like $\{a^{\omega}\}$ over $\textsc{Act}=\{a\}$, that were not $\exists$pz- or $\forall$pz-monitorable on the finfinite domain, are $\exists$pz- or even $\forall$pz-monitorable on the infinite domain. The full analysis of how the hierarchy in Fig. 1 changes for the infinite domain is left for future work.

Barringer et al. [12] consider monitoring of properties over finite traces. In this domain, all properties are monitorable if, as is the case in [12], the end of a trace is observable; in this setting the question of monitorability is less relevant.

9 Conclusion

We have proposed a unified, operational view on monitorability. This allows us to clearly state the implicit operational guarantees of existing definitions of monitorability. For instance, recall Example 1 from the introduction: since $(\textsf{G}\,\neg\textsf{f})\wedge(\textsf{F}\,\textsf{s})$ is $\exists$pz- and $\forall$pz-monitorable but it is not a safety nor co-safety property, we know there is a monitor which can recognise some violations and satisfactions of this property, but there is no monitor that can recognise all satisfactions nor all violations.

Although we focussed on the setting of regular, finfinite properties, the definitions of monitorability in Sec. 3, and, more fundamentally, the methodology that systematically puts the relationship between monitor behaviour and specification centre stage, are equally applicable to other settings. We have already mentioned the infinite domain and richer alphabets in Sec. 8. Another interesting direction would be to lift the restriction to regular properties and finite-state monitors. Indeed, while Barringer et al. consider a specification logic that allows for context-free properties [12], in [25], Ferrier et al. consider monitors with registers (i.e., infinite state monitors) to verify safety properties that are not regular. It seems likely that monitorability beyond safety may also be worth studying in these extended settings.

Acknowledgements

This research was partially supported by the projects “TheoFoMon: Theoretical Foundations for Monitorability” (grant number: 163406-051) and “Epistemic Logic for Distributed Runtime Monitoring” (grant number: 184940-051) of the Icelandic Research Fund, by the BMBF project “Aramis II” (project number:01IS160253) and the EPSRC project “Solving parity games in theory and practice” (project number:EP/P020909/1).

Appendix 0.A Monitorability à la Falcone et al.

Falcone et al. [24] propose three definitions of monitorability (Definitions 16 and 17 in [24]) which they claim to coincide with safety, co-safety, and the union of safety and co-safety properties (Theorem 3 in [24]). We discuss this claim in more detail here, and argue that it does not hold. In brief, their definition deems all properties that are uniform over finite traces, such as “success infinitely often”, or “the trace is finite” to be monitorable, not just safety and co-safety properties. In this appendix we recall Falcone et al.’s definitions and show that their definitions of monitorability include more than just safety and co-safety properties.

Remark 5.

Falcone et al. present finfinite properties as a pair consisting of a set of finite traces and a set of infinite traces. Here we will speak of just one set, containing both finite and infinite traces.

The definition of monitorability proposed by Falcone et al. in [24] is parameterised by a truth domain, and a mapping of formulas into this domain. They then give a uniform condition that defines monitorability with respect to any truth-domain and its associated mapping. Here we focus on their monitorability with respect to the truth-domains $\{\mathsf{tt},?\}$, $\{\mathsf{ff},?\}$ and $\{\mathsf{tt},\mathsf{ff},?\}$, which they claim correspond to co-safety, safety and their union, respectively.

Definition 17 (Property evaluation with respect to a truth-domain [24]).

For each of three different verdict-domains and finfinite properties $P$ (“$r$-properties” in their terminology), Falcone, Fernandez and Mournier define the following evaluation functions:

** For $\mathds{B}=\{\mathsf{ff},?\}$ and $s\in\textsc{Act}^{*}$:**

$\llbracket P\rrbracket_{\mathds{B}}(s)=\mathsf{ff}$ if $\forall f\in{\textsc{Act}^{\infty}}.~{}sf\notin P$

$\llbracket P\rrbracket_{\mathds{B}}(s)=?$ otherwise.

** For $\mathds{B}=\{\mathsf{tt},?\}$ and $s\in\textsc{Act}^{*}$:**

$\llbracket P\rrbracket_{\mathds{B}}(s)=\mathsf{tt}$ if $\forall f\in{\textsc{Act}^{\infty}}.~{}sf\in P$

$\llbracket P\rrbracket_{\mathds{B}}(s)=?$ otherwise.

For $\mathds{B}=\{\mathsf{tt},\mathsf{ff},?\}$ and $s\in\textsc{Act}^{*}$:

$\llbracket P\rrbracket_{\mathds{B}}(s)=\mathsf{tt}$ if $s\in P$ and $\forall f\in{\textsc{Act}^{\infty}}.~{}sf\in P$

$\llbracket P\rrbracket_{\mathds{B}}(s)=\mathsf{ff}$ if $s\notin P$ and $\forall f\in{\textsc{Act}^{\infty}}.~{}sf\notin P$

$\llbracket P\rrbracket_{\mathds{B}}(s)=?$ otherwise. $\hfill\blacksquare$

Definition 18 (FFM-monitorability Definition 17, [24]).

A property $P$ is $\mathds{B}$-monitorable over a truth domain $\mathds{B}$ if for all $s,r\in\textsc{Act}^{*}$, if $s\in P$ and $r\notin P$, then $\llbracket P\rrbracket_{\mathds{B}}(s)\neq\llbracket P\rrbracket_{\mathds{B}}(r)$. $\hfill\blacksquare$

From this definition, it easily follows that any property $P$ for which $P\cap\textsc{Act}^{*}=\emptyset$ or $\textsc{Act}^{*}\subseteq P$ is vacuously monitorable for any truth-domain, and evaluation function. However, not all such properties are safety or co-safety properties: “always eventually success” for instance is neither a safety nor a co-safety property.

We believe the critical points are Lemma 3 and Theorem 3 in [24], which do not hold. The proof of Lemma 3 in particular (Appendix 2.3) falsely claims that $P\cap\textsc{Act}^{*}=\emptyset$ or $\textsc{Act}^{*}\subseteq P$ implies that $P$ is a safety or co-safety properties.

Appendix 0.B An Operational Monitoring System: Regular Monitors

The monitoring system $(\textsc{Mon},\textbf{acc},\textbf{rej})$ is given by a Labelled Transition System (LTS) based on Act, which is comprised of the monitor states, or monitors, and a transition relation. The set of monitor states, Mon, and the monitor transition relation, $\longrightarrow\subseteq(\textsc{Mon}\times(\textsc{Act}\cup\left\{\tau\right\})\times\textsc{Mon})$, are defined in Fig. 3. The suggestive notation $m\xrightarrow{\;\mu\;}n$ denotes $(m,\mu,n)\in\longrightarrow$; we also write $m\not\!\xrightarrow{\;\mu\;}$ to denote $\neg(\exists n.\;m\xrightarrow{\;\mu\;}n)$. We employ the usual notation for weak transitions and write $m\xRightarrow{\quad}n$ in lieu of $m(\xrightarrow{\;\tau\;})^{\ast}n$ and $m\xRightarrow{\;\mu\;}n$ for $m\xRightarrow{\quad}\cdot\xrightarrow{\;\mu\;}\cdot\xRightarrow{\quad}n$. We write sequences of transitions $m\xRightarrow{\alpha_{1}}\cdots\xRightarrow{\alpha_{k}}n$ as $m\xRightarrow{\;s\;}n$, where $s=\alpha_{1}\cdots\alpha_{k}$. A monitor that does not use any parallel operator is called a regular monitor. The full monitoring system and regular monitors were defined and used in [1, 27, 5].

Definition 19 (Acceptance and Rejection).

For a monitor $m\in\textsc{Mon}$, we define $\textbf{rej}(m,s)$ (resp., $\textbf{acc}(m,s)$) and say that $m$ rejects (resp., accepts) when $m\xRightarrow{\;s\;}\textsf{no}$ (resp., $m\xRightarrow{\;s\;}\textsf{yes}$). Similarly, for $t\in\textsc{Act}^{\omega}$, we write $\textbf{rej}(m,t)$ (resp., $\textbf{acc}(m,t)$) if there exist $s\in\textsc{Act}^{*}$ and $u\in\textsc{Act}^{\omega}$ such that $t=su$ and $m$ rejects (resp., accepts) $s$. $\hfill\blacksquare$

For a finite nonempty set of indices $I$, we use $\sum_{i\in I}m_{i}$ to denote any combination of the monitors in $\{m_{i}\mid i\in I\}$ using the operator $+$. For each $j\in I$, $\sum_{i\in I}m_{i}$ is called a sum of $m_{j}$, and $m_{j}$ is called a summand of $\sum_{i\in I}m_{i}$. The following Lem. 3 assures us that regular monitors satisfy the conditions to be a monitoring system, given in Def. 1.

Lemma 3 (Verdict Persistence, [27, 5]).

$v\xRightarrow{\;s\;}m\text{ implies }m=v.$

We will use the following definitions and results in the proofs of Appendix 0.C. We define determinism for regular monitors.

Definition 20 ([4, 3]).

A closed regular monitor $m$ is * deterministic* iff every sum of at least two summands that appears in $m$ is of the form $\sum_{\alpha\in A}\alpha.m_{\alpha}$, where $A\subseteq\textsc{Act}$. $\hfill\blacksquare$

Definition 21 (Verdict Equivalence).

Monitors $m$ and $n$ are called verdict equivalent when for every $f\in{\textsc{Act}^{\infty}}$, $\textbf{acc}(m,f)$ iff $\textbf{acc}(n,f)$ and $\textbf{rej}(m,f)$ iff $\textbf{rej}(n,f)$. $\hfill\blacksquare$

Theorem 0.B.1 ([4, 5]).

Every monitor in Mon is verdict equivalent to a deterministic regular monitor.

In the following, we say that $P$ is suffix-closed when for all $s,r\in\textsc{Act}^{*}$, $s\in P$ implies $sr\in P$ — notice that we only quantify over finite traces. The suffix-closure of $P$ is $\{sf\in{\textsc{Act}^{\infty}}\mid s\in P\}$.

Theorem 0.B.2 ([4, 3]).

If $L,L^{\prime}\subseteq\textsc{Act}^{*}$ are regular and suffix-closed, and $L\cap L^{\prime}=\emptyset$, then there is a regular monitor $m$, such that $\textbf{acc}(m,s)$ iff $s\in L$ and $\textbf{rej}(m,s)$ iff $s\in L^{\prime}$.

In this appendix, we use the formula synthesis function from regular monitors to sHML formulae, from [27, 5]:

[TABLE]

Theorem 0.B.3 ([5]).

For every regular monitor $m$, $\textsf{f}(m)\in\textsc{sHML}$, and $m$ is sound and violation-complete for $\textsf{f}(m)$.

Appendix 0.C Proofs Omitted from the Main Document

Here we present the proofs of results that were omitted from the main text.

We use the following classical result (see [8] for more on the $\mu$-calculus and recHML):

Lemma 4.

If $\varphi\in\textsc{recHML}$, then $\llbracket\varphi\rrbracket\cap\textsc{Act}^{*}$ is regular.

Due to Thm. 0.B.1, we can assume that every monitor in Mon is a regular, or deterministic regular monitor. We often do so in the following proofs.

Definition 22.

Let $P\subseteq{\textsc{Act}^{\infty}}$. We define the following two sets of finite traces:

$D^{-}_{P}=\{s\in\textsc{Act}^{*}\mid P\text{ is negatively determined by }s\}$;

$D^{+}_{P}=\{s\in\textsc{Act}^{*}\mid P\text{ is positively determined by }s\}$. $\hfill\blacksquare$

Lemma 5.

If $P\subseteq{\textsc{Act}^{\infty}}$ is monitorable for satisfaction (resp., for violation) by any monitoring system, then every $f\in P$ (resp., $f\in{\textsc{Act}^{\infty}}\setminus P$) has a finite prefix that positively (resp., negatively) determines $P$.

Proof.

We treat the case for satisfaction, as the case for violation is dual. Let $f\in P$ and $m$ be a monitor that is sound and satisfaction-complete for $P$. Then, due to satisfaction-completeness, $\textbf{acc}(m,f)$, and by the requirements of Def. 1, there is a finite prefix $s$ of $f$, such that $\textbf{acc}(m,s)$. Therefore, by the same requirements, for every $g\in{\textsc{Act}^{\infty}}$, $\textbf{acc}(m,sg)$. As we know that $m$ is sound for $P$, this yields that $s$ positively determines $P$. ∎

For a set of finite traces $S\subseteq\textsc{Act}^{*}$, we define

[TABLE]

Lemma 6.

Assume that every finfinite trace that satisfies (resp., violates) $P$ has a prefix that positively (resp., negatively) determines $P$. Then $P$ (resp., ${\textsc{Act}^{\infty}}\setminus P$) is the suffix-closure of $\min(P\cap\textsc{Act}^{*})$ (resp., of $\min(({\textsc{Act}^{\infty}}\setminus P)\cap\textsc{Act}^{*})$).

Proof.

Again, we only treat the case for satisfaction. Let $f\in P$. By our assumptions, there is at least one finite prefix of $f$ that positively determines $P$. These prefixes of $f$ are well-ordered by the prefix relation, and therefore there is a smallest prefix $s$ of $f$ that positively determines $P$. Therefore, $s\in\min(P\cap\textsc{Act}^{*})$, and we see that $f$ is in the suffix-closure of $\min(P\cap\textsc{Act}^{*})$. Conversely, let $s\in\min(P\cap\textsc{Act}^{*})$ and $f$ be an extension of $s$. Then, $s\in\llbracket P\rrbracket$, so by the proviso of the lemma, there is a prefix $r$ of $s$ (and of $f$) that positively determines $P$,333The reader may also notice that $s=r$, due to the minimality of $s$. and therefore $f\in P$. ∎

0.C.0.1 Proofs Omitted from Sec. 4: Regularity and Monitors

Lemma 7.

If $\varphi\in\textsc{recHML}$, then $D^{+}_{\varphi}$ and $D^{-}_{\varphi}$ are regular.

Proof.

We know that $\llbracket\varphi\rrbracket\cap\textsc{Act}^{*}$ is regular (Lem. 4) and $\llbracket\varphi\rrbracket\cap\textsc{Act}^{\omega}$, the infinite-trace interpretation of $\varphi$, is $\omega$-regular. Therefore, there are a DFA $D_{F}$ that recognizes $\llbracket\varphi\rrbracket\cap\textsc{Act}^{*}$ and a deterministic $\omega$-automaton $D_{I}$ that recognizes $\llbracket\varphi\rrbracket\cap\textsc{Act}^{\omega}$. Let $A_{F}=\{s\in\textsc{Act}^{*}\mid\forall r\in\textsc{Act}^{*}.~{}sr\in\llbracket\varphi\rrbracket\}$ and $A_{I}=\{s\in\textsc{Act}^{*}\mid\forall t\in\textsc{Act}^{\omega}.~{}st\in\llbracket\varphi\rrbracket\}$. Let $Q_{F}$ (resp., $Q_{I}$) be the set of states in $D_{F}$ (resp., in $D_{I}$) that can be reached reading some trace $s\in\textsc{Act}^{*}$. By construction, for each $s\in\textsc{Act}^{*}$, we have that $s\in A_{F}$ (resp., $s\in A_{I}$) if and only if $s$ ends in the respective set in the automaton. Therefore, there are DFAs $D^{\prime}_{F}$ and $D^{\prime}_{I}$ for $A_{F}$ and $A_{I}$, respectively, and thus $D^{+}_{\varphi}=A_{F}\cap A_{I}$ is regular. The case for $D^{-}_{\varphi}$ is similar. ∎

• Theorem 4.1

For all $\varphi{\in}\textsc{recHML}$, there is a monitor $m{\in}\textsc{Mon}$ that is sound for $\varphi$ and accepts all finite traces that positively determine $\varphi$ and rejects all finite traces that negatively determine $\varphi$.

Proof.

By Lem. 7, $D^{+}_{\varphi}$ and $D^{-}_{\varphi}$, the sets of finite traces that (respectively) positively or negatively determine $\varphi$ are regular. It is also not hard to see that they are suffix-closed. Therefore the theorem follows from Thm. 0.B.2. ∎

Corollary 1.

If $m$ is a sound monitor for $\varphi\in\textsc{recHML}$, then there is a regular monitor $n$ that is sound for $\varphi$, and such that for every $s\in\textsc{Act}^{*}$, $\textbf{acc}(m,s)$ implies $\textbf{acc}(n,s)$, and $\textbf{rej}(m,s)$ implies $\textbf{rej}(n,s)$.

Proof.

By Thm. 4.1, there is a regular monitor $n$ that is sound for $\varphi$, and accepts all finite traces that positively determine $\varphi$, and rejects all the finite traces that negatively determine $\varphi$. If $\textbf{acc}(m,s)$ (resp., $\textbf{rej}(m,s)$) for some finite trace $s$, then, due to the soundness of $m$, $s\in\llbracket\varphi\rrbracket$ (resp., $s\notin\llbracket\varphi\rrbracket$), and therefore, from Lem. 1, $s$ positively (resp., negatively) determines $\varphi$. By the properties of $n$, we have that $\textbf{acc}(n,s)$ (resp., $\textbf{rej}(n,s)$). ∎

0.C.0.2 Proofs Omitted from Sec. 5: Syntactic Characterizations

Definition 23.

Let $m$ be a closed regular monitor, and let $n$ be one of its submonitors. We say that $n$ can refute (resp., verify) in 0 unfoldings, when no (resp., yes) appears in $n$, and that it can refute (resp., verify) in $k+1$ unfoldings, when it can refute (resp., verify) in $k$ unfoldings, or $x$ appears in $n$ and $n$ is in the scope of a submonitor $\textsf{rec}\,x.n^{\prime}$ of $m$ that can refute (resp., verify) in $k$ unfoldings. We simply say that $n$ can refute (resp., verify) in $m$ when it can refute (resp., verify) in $k$ unfoldings, for some $k\geq 0$. $\hfill\blacksquare$

We define the depth of $\mathsf{ff}$ in an sHML formula in a recursive way: $d_{\mathsf{ff}}(\mathsf{ff})=0$; $d_{\mathsf{ff}}(\mathsf{tt})=d_{\mathsf{ff}}(X)=\infty$; $d_{\mathsf{ff}}(\psi_{1}\land\psi_{2})=\min\{d_{\mathsf{ff}}(\psi_{1}),d_{\mathsf{ff}}(\psi_{2})\}+1$; $d_{\mathsf{ff}}(\mathbf{[}\alpha\mathbf{]}\psi)=d_{\mathsf{ff}}(\psi)+1$; and $d_{\mathsf{ff}}(\max X.\psi)=d_{\mathsf{ff}}(\psi)+1$.

Lemma 8.

For all possibly open $\varphi,\psi\in\textsc{sHML}$ $d_{\mathsf{ff}}(\varphi[\psi/X])\leq d_{\mathsf{ff}}(\varphi)$.

Proof.

Straightforward induction on $\varphi$. ∎

Lemma 9.

If $\varphi\in\textsc{iHML}$, then there is a regular monitor that is sound and informative for $\varphi$.

Proof.

We assume that $\varphi\in\textsc{siHML}$, as the case for $\varphi\in\textsc{ciHML}$ is similar. Let $\varphi=\varphi_{1}\land\varphi_{2}$, where $\varphi_{1}\in\textsc{sHML}$ and $\mathsf{ff}$ appears in $\varphi_{1}$. We prove by induction on $d_{\mathsf{ff}}(\psi)$ that for all $\psi\in\textsc{sHML}$, if $d_{\mathsf{ff}}(\psi)<\infty$, then there is a finite trace that negatively determines $\psi$. If $d_{\mathsf{ff}}(\psi)=0$, then $\psi=\mathsf{ff}$, and we are done, as $\varepsilon$ negatively determines $\mathsf{ff}$. Otherwise, $d_{\mathsf{ff}}(\psi)=k+1$ and we consider the following cases:

$\psi=\psi_{1}\land\psi_{2}$

In this case, either $d_{\mathsf{ff}}(\psi_{1})=k$ or $d_{\mathsf{ff}}(\psi_{2})=k$, so by the inductive hypothesis, there is a finite trace that negatively determines one of the two conjuncts, and therefore also $\psi$.

$\psi=\mathbf{[}\alpha\mathbf{]}\psi^{\prime}$

In this case, $d_{\mathsf{ff}}(\psi^{\prime})=k$, so, by the inductive hypothesis, there is a finite trace $s$ that negatively determines $\psi^{\prime}$, so $\alpha s$ negatively determines $\psi$.

$\psi=\max X.\psi^{\prime}$

In this case, $d_{\mathsf{ff}}(\psi^{\prime})=k$. Therefore, from Lem. 8, $d_{\mathsf{ff}}(\psi^{\prime}[\psi/X])\leq d_{\mathsf{ff}}(\psi^{\prime})=k$, so, by the inductive hypothesis, there is a finite trace $s$ that negatively determines $\psi^{\prime}[\psi/X]$, so it also negatively determines $\psi$, because $\llbracket\psi^{\prime}[\psi/X]\rrbracket=\llbracket\psi\rrbracket$.

As $\mathsf{ff}$ appears in $\varphi_{1}$, $d_{\mathsf{ff}}(\varphi)<\infty$, so there is a finite trace that negatively determines $\varphi_{1}$, and therefore also $\varphi$. The theorem follows from Thm. 4.1. ∎

Lemma 10.

If $\varphi\in\textsc{recHML}$ and there is a monitor that is sound and informative for $\varphi$, then there is some $\psi\in\textsc{iHML}$ such that $\llbracket\psi\rrbracket=\llbracket\varphi\rrbracket$.

Proof.

If $m$ is sound and informative for $\varphi$, then by Lem. 1, there is a finite trace $s$ that positively or negatively determines $\varphi$. Without loss of generality, we assume that $s$ positively determines $\varphi$. We can then easily construct a formula $\psi_{1}(s)$ that is satisfied exactly by $s$ and all its extensions, recursively on $s$: let $\psi_{1}(\varepsilon)=\mathsf{tt}$, and let $\psi_{1}(\alpha s)=\mathbf{\langle}\alpha\mathbf{\rangle}\psi_{1}(s)$. Then, let $\psi=\psi_{1}(s)\lor\varphi$. Thus, $\psi\in\textsc{iHML}$ and $\llbracket\psi\rrbracket=\llbracket\varphi\rrbracket$. ∎

• Theorem 5.2

For $\varphi\in\textsc{recHML}$, $\varphi$ is informatively monitorable if and only if there is some $\psi\in\textsc{iHML}$, such that $\llbracket\psi\rrbracket=\llbracket\varphi\rrbracket$.

Proof.

A consequence of Lems. 9 and 10. ∎

Lemma 11.

If $\max X.\varphi\in\textsc{sHML}$ can refute in $\max X.\varphi\in\textsc{sHML}$, then it is also the case that $\varphi[\max X.\varphi/X]$ can refute in $\varphi[\max X.\varphi/X]$.

Lemma 12.

If all subformulae of $\mathbf{[}\alpha\mathbf{]}\varphi$ or $\varphi\land\psi$ or $\psi\land\varphi$ can refute, then all subformulae of $\varphi$ can refute. If all subformulae of $\max X.\varphi$ can refute, then all subformulae of $\varphi[\max X.\varphi/X]$ can refute.

We define the box-depth of a formula from $\textsc{eHML}\cap\textsc{sHML}$ recursively:

[TABLE]

Lemma 13.

For all possibly open $\varphi,\psi\in\textsc{eHML}\cap\textsc{sHML}$ $d_{B}(\varphi[\psi/X])\leq d_{B}(\varphi)$.

Proof.

Straightforward induction on $\varphi$. ∎

Lemma 14.

Let $\alpha\in\textsc{Act}$ and $\varphi\in\textsc{eHML}\cap\textsc{sHML}$ (resp., $\varphi\in\textsc{eHML}\cap\textsc{cHML}$), where all subformulae of $\varphi$ can refute (resp., verify). There is some $\psi\in\textsc{eHML}\cap\textsc{sHML}$ (resp., $\psi\in\textsc{eHML}\cap\textsc{cHML}$), such that all subformulae of $\psi$ can refute (resp., verify), and for every $f\in{\textsc{Act}^{\infty}}$, $\alpha f\in\llbracket\varphi\rrbracket$ implies that $f\in\llbracket\psi\rrbracket$ (resp., $f\in\llbracket\psi\rrbracket$ implies that $\alpha f\in\llbracket\varphi\rrbracket$).

Proof.

We assume that $\varphi\in\textsc{eHML}\cap\textsc{sHML}$, as the case for $\varphi\in\textsc{eHML}\cap\textsc{cHML}$ is similar. Since $\varphi$ is a closed formula and can refute, $\mathsf{ff}$ appears in $\varphi$, and therefore $d_{B}(\varphi)<\infty$. We proceed to prove the lemma by induction on $d_{B}(\varphi)$, similarly to the proof of Lem. 9.

If $\varphi=\mathsf{ff}$,

then we are done immediately by taking $\psi=\mathsf{ff}$.

If $\varphi=\bigwedge_{\gamma\in\textsc{Act}}\mathbf{[}\gamma\mathbf{]}\varphi_{\gamma}$,

then we can set $\psi=\varphi_{\alpha}$.

If $\varphi=\varphi_{1}\land\varphi_{2}$,

then either $d_{a}(\varphi_{1})<\infty$ or $d_{a}(\varphi_{2})<\infty$, and we are done by the inductive hypothesis on one of the two subformulae.

If $\varphi=\max X.\varphi^{\prime}$,

then $\varphi^{\prime}[\varphi/X]\in\textsc{eHML}\cap\textsc{sHML}$ and all subformulae of $\varphi^{\prime}[\varphi/X]$ can refute, by Lem. 12. Furthermore, $\llbracket\varphi\rrbracket=\llbracket\varphi^{\prime}[\varphi/X]\rrbracket$, and we are done by the inductive hypothesis. ∎

Lemma 15.

If $\varphi\in\textsc{spHML}$ or $\varphi\in\textsc{cpHML}$, then there is a regular monitor that is sound for $\varphi$ and persistently rejecting, or, respectively, persistently verifying.

Proof.

We assume that $\varphi\in\textsc{spHML}$, as the case for $\varphi\in\textsc{cpHML}$ is similar. Let $\varphi=\psi\land\psi_{*}$, where $\psi\in\textsc{eHML}\cap\textsc{sHML}$ and all of its subformulae can refute. By Thm. 4.1, it suffices to prove that for every $s\in\textsc{Act}^{*}$, there is some $r\in\textsc{Act}^{*}$, such that $sr$ negatively determines $\varphi$. We prove this by induction on $s$. If $s=\varepsilon$, then as in the proof of Lem. 9, we can show that there is a finite trace that negatively determines $\psi$. If $s=as^{\prime}$, then by Lem. 14. there is some $\psi^{\prime}\in\textsc{eHML}\cap\textsc{sHML}$, such that all subformulae of $\psi^{\prime}$ can refute, and for every $f\in{\textsc{Act}^{\infty}}$, $af\in\llbracket\psi\rrbracket$ implies that $f\in\llbracket\psi^{\prime}\rrbracket$. By the inductive hypothesis, there is some $r$, such that $s^{\prime}r$ negatively determines $\psi^{\prime}$, and therefore, $sr$ negatively determines $\psi$. ∎

We define the depth of a variable $x$ in a regular monitor $m$ recursively: $d_{x}(x)=0$ and $d_{x}(y)=d(\textsf{no})=d(\textsf{yes})=\infty$, where $y\neq x$; $d_{x}(m_{1}+m_{2})=\min\{d_{x}(m_{1}),d_{x}(m_{2})\}+1$; $d_{x}(\alpha.m)=d_{x}(m)+1$; and $d_{x}(\textsf{rec}\,x.~{}m)=d_{x}(\textsf{rec}\,y.~{}m)=d_{x}(m)+1$.

Lemma 16.

Let $m$ be a persistently rejecting, deterministic regular monitor. If $A\subsetneq\textsc{Act}$, then $\sum_{\alpha\in A}\alpha.m_{\alpha}$ can only appear in $m$ as a submonitor of a larger sum.

Proof.

Let $a\in\textsc{Act}\setminus A$ and let $m^{\prime}$ be an open monitor and $x$ a variable that does not appear in $m$, such that $m=m^{\prime}[\sum_{\alpha\in A}\alpha.m_{\alpha}/x]$. It is clear that $\sum_{\alpha\in A}\alpha.m_{\alpha}\centernot{\xRightarrow{\;a\;}}$. Therefore, it suffices to prove that for every deterministic $n$ with free variable $x$, if $n^{\prime}\centernot{\xRightarrow{\;a\;}}$, then there is a finite trace $s$, such that there is no regular monitor $o$ for which $n[n^{\prime}/x]\xRightarrow{\;sa\;}o$. We proceed to prove this claim by induction on $d_{x}(n)$, and the case for $n=x$ is immediate. If $n=n_{1}+n_{2}$, then, as $n$ is deterministic, $n=b.n_{1}^{\prime}+c.n_{2}^{\prime}$, where $b\neq c$, and we are done by the inductive hypothesis on either $n_{1}^{\prime}$ or $n_{2}^{\prime}$, and $n^{\prime}$. If $n=b.n_{1}$, then if the inductive hypothesis on $n_{1}^{\prime}$ and $n^{\prime}$ gives trace $r$, then we can set $s=br$. If $n=\textsf{rec}\,y.n_{1}$, then we re done by the inductive hypothesis on $n_{1}[n/y]$ and $n^{\prime}[n/y]$. ∎

Here we call a regular monitor explicit when it is generated by the grammar:

[TABLE]

Corollary 2.

Every persistently rejecting, deterministic regular monitor is explicit.

Proof.

From Lem. 16. ∎

Lemma 17.

Let $m$ be an explicit deterministic regular monitor, such that all of its submonitors can refute. Then, $\textsf{f}(m)\in\textsc{eHML}$ and all of its subformulae can refute.

Proof.

By induction on the construction of $m$. ∎

Lemma 18.

If $\varphi\in\textsc{recHML}$ and there is a monitor that is sound for $\varphi$ and persistently rejecting or persistently verifying, then there is some $\psi\in\textsc{spHML}$, or, respectively, $\psi\in\textsc{cpHML}$, such that $\llbracket\psi\rrbracket=\llbracket\varphi\rrbracket$.

Proof.

We treat the case where the monitor is persistently rejecting, as the case for a persistently verifying monitor is similar. From Cor. 1, there is a regular monitor, $m$, that is sound for $\varphi$ and persistently rejecting. By Thm. 0.B.1, we can assume that $m$ is deterministic (Def. 20). From Cor. 2, $m$ is explicit. If there is a submonitor of $m$ that cannot refute, then we can inductively on $m$ prove that there is a finite trace $s$, for which there is no finite trace $r$, such that $m\xRightarrow{\;sr\;}\textsf{no}$, which is a contradiction. Therefore, from Lem. 17, the sHML formula $\textsf{f}(m)$ that we can synthesize from $m$ is in eHML, and all of its subformulae can refute. Since $m$ is sound for $\varphi$ and sound and violation complete for $\textsf{f}(m)$, it is the case that ${\textsc{Act}^{\infty}}\setminus\llbracket\textsf{f}(m)\rrbracket\subseteq{\textsc{Act}^{\infty}}\setminus\llbracket\varphi\rrbracket$, and therefore $\textsf{f}(m)\land\varphi\in\textsc{spHML}$ and $\llbracket\textsf{f}(m)\land\varphi\rrbracket=\llbracket\varphi\rrbracket$. ∎

• Theorem 5.3

For $\varphi\in\textsc{recHML}$, $\varphi$ is persistently informatively monitorable for violation (resp., for satisfaction) if and only if there is some $\psi\in\textsc{spHML}$ (resp., $\psi\in\textsc{cpHML}$), such that $\llbracket\psi\rrbracket=\llbracket\varphi\rrbracket$.

Proof.

A consequence of Lems. 15 and 18. ∎