Adventures in Monitorability: From Branching to Linear Time and Back Again

TL;DR

This paper develops a comprehensive theory of runtime monitorability for a highly expressive modal logic, comparing linear and branching time settings, and providing a hierarchy of monitorable fragments with guarantees.

Contribution

It introduces an expressiveness hierarchy of monitorable fragments of Hennessy-Milner logic with recursion in linear time, and characterizes what properties can be monitored within each fragment.

Findings

Established a hierarchy of monitorable logic fragments.

Identified exactly which properties are monitorable in each fragment.

Provided a framework for automatic synthesis of correct monitors.

Abstract

This paper establishes a comprehensive theory of runtime monitorability for Hennessy-Milner logic with recursion, a very expressive variant of the modal $\mu$-calculus. It investigates the monitorability of that logic with a linear-time semantics and then compares the obtained results with ones that were previously presented in the literature for a branching-time setting. Our work establishes an expressiveness hierarchy of monitorable fragments of Hennessy-Milner logic with recursion in a linear-time setting and exactly identifies what kinds of guarantees can be given using runtime monitors for each fragment in the hierarchy. Each fragment is shown to be complete, in the sense that it can express all properties that can be monitored under the corresponding guarantees. The study is carried out using a principled approach to monitoring that connects the semantics of the logic and the operational semantics of monitors. The proposed framework supports the automatic, compositional synthesis of correct monitors from monitorable properties.

Equations

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

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

$$\mid ⟨A⟩\phi$$

$$\mid \mathsf{min}X.\phi$$

$$\mid X$$

$$\begin{array}[]{rlrl}\llbracket\mathsf{tt},\sigma\rrbracket_{\textsc{L}}&\!\!\!\,\overset{\leavevmode\resizebox{6.0pt}{}{\,{def}}\,}{=}\,\textsc{Trc}&\llbracket\mathsf{ff},\sigma\rrbracket_{\textsc{L}}&\!\!\!\,\overset{\leavevmode\resizebox{6.0pt}{}{\,{def}}\,}{=}\,\emptyset\\ \llbracket\varphi_{1}\mathbf{\vee}\varphi_{2},\sigma\rrbracket_{\textsc{L}}&\!\!\!\,\overset{\leavevmode\resizebox{6.0pt}{}{\,{def}}\,}{=}\,\llbracket\varphi_{1},\sigma\rrbracket_{\textsc{L}}\cup\llbracket\varphi_{2},\sigma\rrbracket_{\textsc{L}}&\llbracket\varphi_{1}\mathbf{\wedge}\varphi_{2},\sigma\rrbracket_{\textsc{L}}&\!\!\!\,\overset{\leavevmode\resizebox{6.0pt}{}{\,{def}}\,}{=}\,\llbracket\varphi_{1},\sigma\rrbracket_{\textsc{L}}\cap\llbracket\varphi_{2},\sigma\rrbracket_{\textsc{L}}\\ \llbracket\mathbf{\langle}A\mathbf{\rangle}\varphi,\sigma\rrbracket_{\textsc{L}}&\lx@intercol\!\!\!\,\overset{\leavevmode\resizebox{6.0pt}{}{\,{def}}\,}{=}\,\left\{t\;|\;\exists u\cdot\exists\alpha\in A\cdot t=\alpha u\;\text{ and }\;u\in\llbracket\varphi,\sigma\rrbracket_{\textsc{L}}\right\}\hfil\lx@intercol\\ \llbracket\mathbf{[}A\mathbf{]}\varphi,\sigma\rrbracket_{\textsc{L}}&\lx@intercol\!\!\!\,\overset{\leavevmode\resizebox{6.0pt}{}{\,{def}}\,}{=}\,\left\{t\;|\;\forall u\cdot\forall\alpha\in A\cdot t=\alpha u\;\text{ implies }\;u\in\llbracket\varphi,\sigma\rrbracket_{\textsc{L}}\right\}\hfil\lx@intercol\par\\ \llbracket\mathsf{min}\,\!X.\varphi,\sigma\rrbracket_{\textsc{L}}&\!\!\!\,\overset{\leavevmode\resizebox{6.0pt}{}{\,{def}}\,}{=}\,\bigcap\left\{\textsl{T}\;|\;\llbracket\varphi,\sigma[X\mapsto\textsl{T}]\rrbracket_{\textsc{L}}\subseteq\textsl{T}\ \right\}\par\\ \llbracket\mathsf{max}\,\!X.\varphi,\sigma\rrbracket_{\textsc{L}}&\!\!\!\,\overset{\leavevmode\resizebox{6.0pt}{}{\,{def}}\,}{=}\,\bigcup\left\{\textsl{T}\;|\;\textsl{T}\subseteq\llbracket\varphi,\sigma[X\mapsto\textsl{T}]\rrbracket_{\textsc{L}}\ \right\}&\llbracket X,\sigma\rrbracket_{\textsc{L}}&\!\!\!\,\overset{\leavevmode\resizebox{6.0pt}{}{\,{def}}\,}{=}\,\sigma(X)\\ \\ \end{array}$$

$$\begin{array}[]{rlrl}\llbracket\mathsf{tt},\rho\rrbracket_{\textsc{B}}&\!\!\!\,\overset{\leavevmode\resizebox{6.0pt}{}{\,{def}}\,}{=}\,\textsc{Prc}&\llbracket\mathsf{ff},\rho\rrbracket_{\textsc{B}}&\!\!\!\,\overset{\leavevmode\resizebox{6.0pt}{}{\,{def}}\,}{=}\,\emptyset\\ \llbracket\varphi_{1}\mathbf{\vee}\varphi_{2},\rho\rrbracket_{\textsc{B}}&\!\!\!\,\overset{\leavevmode\resizebox{6.0pt}{}{\,{def}}\,}{=}\,\llbracket\varphi_{1},\rho\rrbracket_{\textsc{B}}\cup\llbracket\varphi_{2},\rho\rrbracket_{\textsc{B}}&\llbracket\varphi_{1}\mathbf{\wedge}\varphi_{2},\rho\rrbracket_{\textsc{B}}&\!\!\!\,\overset{\leavevmode\resizebox{6.0pt}{}{\,{def}}\,}{=}\,\llbracket\varphi_{1},\rho\rrbracket_{\textsc{B}}\cap\llbracket\varphi_{2},\rho\rrbracket_{\textsc{B}}\\ \llbracket\mathbf{\langle}A\mathbf{\rangle}\varphi,\rho\rrbracket_{\textsc{B}}&\lx@intercol\!\!\!\,\overset{\leavevmode\resizebox{6.0pt}{}{\,{def}}\,}{=}\,\left\{p\;|\;\exists q\cdot\exists\alpha\in A\cdot p\xRightarrow{\;\alpha\;}q\;\text{ and }\;q\in\llbracket\varphi,\rho\rrbracket_{\textsc{B}}\right\}\hfil\lx@intercol\\ \llbracket\mathbf{[}A\mathbf{]}\varphi,\rho\rrbracket_{\textsc{B}}&\lx@intercol\!\!\!\,\overset{\leavevmode\resizebox{6.0pt}{}{\,{def}}\,}{=}\,\left\{p\;|\;\forall q\cdot\forall\alpha\in A\cdot p\xRightarrow{\;\alpha\;}q\;\text{ implies }\;q\in\llbracket\varphi,\rho\rrbracket_{\textsc{B}}\right\}\hfil\lx@intercol\\ \llbracket\mathsf{min}\,\!X.\varphi,\rho\rrbracket_{\textsc{B}}&\!\!\!\,\overset{\leavevmode\resizebox{6.0pt}{}{\,{def}}\,}{=}\,\bigcap\left\{\textsl{P}\;|\;\llbracket\varphi,\rho[X\mapsto\textsl{P}]\rrbracket_{\textsc{B}}\subseteq\textsl{P}\right\}\\ \llbracket\mathsf{max}\,\!X.\varphi,\rho\rrbracket_{\textsc{B}}&\!\!\!\,\overset{\leavevmode\resizebox{6.0pt}{}{\,{def}}\,}{=}\,\bigcup\left\{\textsl{P}\;|\;\textsl{P}\subseteq\llbracket\varphi,\rho[X\mapsto\textsl{P}]\rrbracket_{\textsc{B}}\right\}&\llbracket X,\rho\rrbracket_{\textsc{B}}&\!\!\!\,\overset{\leavevmode\resizebox{6.0pt}{}{\,{def}}\,}{=}\,\rho(X)\end{array}$$

$$\text{hfill}\text{qed}$$

$${\phi }_1$$

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

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

$$\displaystyle\inference[\textsc{mAct}]{}{\alpha.{m}\;\xrightarrow{\;\alpha\;}\;m}\penalty 50\hskip 20.00003pt plus 0.5fil minus 5.0pt\inference[\textsc{mRec}]{}{\textsf{rec}\,x.m\;\xrightarrow{\;\tau\;}\;m[\raisebox{2.15277pt}{\small$\textsf{rec}\,x.m$}\!/\!\mbox{\small$x$}]}\penalty-10000\hskip 20.00003pt plus 0.5fil minus 5.0pt\penalty-10000\hskip 20.00003pt plus 0.5fil minus 5.0pt\penalty-10000\hskip 20.00003pt plus 0.5fil minus 5.0pt\inference[\textsc{mSelL}]{m\;\xrightarrow{\;\mu\;}\;m^{\prime}}{m+n\;\xrightarrow{\;\mu\;}\;m^{\prime}}\penalty 50\hskip 20.00003pt plus 0.5fil minus 5.0pt\inference[\textsc{mSelR}]{n\;\xrightarrow{\;\mu\;}\;n^{\prime}}{m+n\;\xrightarrow{\;\mu\;}\;n^{\prime}}\penalty 50\hskip 20.00003pt plus 0.5fil minus 5.0pt\inference[\textsc{mVer}]{}{v\;\xrightarrow{\;\alpha\;}\;v}$$

$$\displaystyle\inference[\textsc{iMon}]{p\;\xrightarrow{\;\alpha\;}\;p^{\prime}&m\;\xrightarrow{\;\alpha\;}\;m^{\prime}}{m\triangleleft\,p\;\xrightarrow{\;\alpha\;}\;m^{\prime}\triangleleft\,p^{\prime}}\penalty 50\hskip 20.00003pt plus 0.5fil minus 5.0pt\inference[\textsc{iTer}]{p\;\xrightarrow{\;\alpha\;}\;p^{\prime}&m\;\not\!\xrightarrow{\;\alpha\;}\;m\;\not\!\xrightarrow{\;\tau\;}\;}{m\triangleleft\,p\;\xrightarrow{\;\alpha\;}\;\textsf{end}\triangleleft\,p^{\prime}}\penalty-10000\hskip 20.00003pt plus 0.5fil minus 5.0pt\penalty-10000\hskip 20.00003pt plus 0.5fil minus 5.0pt\penalty-10000\hskip 20.00003pt plus 0.5fil minus 5.0pt\inference[\textsc{iAsyP}]{p\;\xrightarrow{\;\tau\;}\;p^{\prime}}{m\triangleleft\,p\;\xrightarrow{\;\tau\;}\;m\triangleleft\,p^{\prime}}\penalty 50\hskip 20.00003pt plus 0.5fil minus 5.0pt\inference[\textsc{iAsyM}]{m\;\xrightarrow{\;\tau\;}\;m^{\prime}}{m\triangleleft\,p\;\xrightarrow{\;\tau\;}\;m^{\prime}\triangleleft\,p}$$

$$\text{rec}x.(a.x+b.\text{yes})◃a.\text{rec}x.b.x\stackrel{\tau }{\to }(a.(\text{rec}x.(a.x+b.\text{yes}))+b.\text{yes})◃a.\text{rec}x.b.x\stackrel{a}{\to }$$

$$\text{rec}x.(a.x+b.\text{yes})◃\text{rec}x.b.x\stackrel{\tau \tau }{\to }\to a.\text{rec}x.(a.x+b.\text{yes})+b.\text{yes}◃b.\text{rec}x.b.x\stackrel{b}{\to }\text{yes}◃\text{rec}x.b.x.$$

$$\text{rec}x.(a.a.x+b.\text{yes})◃a.\text{rec}x.b.x\stackrel{\tau }{\to }(a.a.(\text{rec}x.(a.a.x+b.\text{yes}))+b.\text{yes})◃a.\text{rec}x.b.x\stackrel{a}{\to }$$

$$a.\text{rec}x.(a.x+b.\text{yes})◃\text{rec}x.b.x\stackrel{\tau }{\to }a.\text{rec}x.(a.x+b.\text{yes})◃b.\text{rec}x.b.x\stackrel{b}{\to }\text{end}◃\text{rec}x.b.x$$

$$\displaystyle m,n\in\textsc{Mon}\ \mathrel{::=}\$$

$$\mid$$

$$\displaystyle\inference[\textsc{mPar}]{m\;\xrightarrow{\;\alpha\;}\;m^{\prime}&n\;\xrightarrow{\;\alpha\;}\;n^{\prime}}{m{\odot}n\;\xrightarrow{\;\alpha\;}\;m^{\prime}{\odot}n^{\prime}}\quad\inference[\textsc{mTauL}]{m\;\xrightarrow{\;\tau\;}\;m^{\prime}}{m{\odot}n\;\xrightarrow{\;\tau\;}\;m^{\prime}{\odot}n}\quad\inference[\textsc{mVrE}]{}{\textsf{end}{\odot}\textsf{end}\xrightarrow{\;\tau\;}\textsf{end}}\penalty-10000\hskip 20.00003pt plus 0.5fil minus 5.0pt\penalty-10000\hskip 20.00003pt plus 0.5fil minus 5.0pt\penalty-10000\hskip 20.00003pt plus 0.5fil minus 5.0pt\inference[\textsc{mVrC1}]{}{{{\textsf{yes}{\otimes}m}\xrightarrow{\;\tau\;}{m}}}\quad\inference[\textsc{mVrC2}]{}{{{\textsf{no}{\otimes}m}\xrightarrow{\;\tau\;}{\textsf{no}}}}\quad\inference[\textsc{mVrD1}]{}{{{\textsf{no}{\oplus}m}\xrightarrow{\;\tau\;}{m}}}\quad\inference[\textsc{mVrD2}]{}{{{\textsf{yes}{\oplus}m}\xrightarrow{\;\tau\;}{\textsf{yes}}}}$$

$$\text{hfill}\text{qed}$$

$$\text{m}(\mathsf{ff})$$

$$\text{hfill}\text{qed}$$

$$\text{m}(\phi )=m$$

$$\text{hfill}\text{qed}$$

$$\text{noR}(x)$$

$$\text{hfill}\text{qed}$$

$$\phi ::=\mathsf{tt}\mid \mathsf{ff}\mid {\bigwedge }_{\alpha \in B}[\alpha ]{\phi }_{\alpha }\mid {\bigvee }_{\alpha \in D}⟨\alpha ⟩{\phi }_{\alpha },$$

$$[\text{textsc}Act]\mathsf{ff}$$

$$\mathsf{tt}\wedge \phi$$

$$\underset{\alpha \in A}{\bigwedge }[\alpha ]{\phi }_{\alpha }\wedge \underset{\alpha \in B}{\bigwedge }[\alpha ]{\psi }_{\alpha }$$

$$\underset{\alpha \in A}{\bigwedge }[\alpha ]{\phi }_{\alpha }\vee \underset{\alpha \in B}{\bigwedge }[\alpha ]{\psi }_{\alpha }$$

$$\underset{\alpha \in A}{\bigvee }⟨\alpha ⟩{\phi }_{\alpha }\vee \underset{\alpha \in B}{\bigvee }⟨\alpha ⟩{\psi }_{\alpha }$$

$$\underset{\alpha \in A}{\bigvee }⟨\alpha ⟩{\phi }_{\alpha }\wedge \underset{\alpha \in B}{\bigvee }⟨\alpha ⟩{\psi }_{\alpha }$$

$$\underset{\alpha \in A}{\bigwedge }[\alpha ]{\phi }_{\alpha }\wedge \underset{\alpha \in B}{\bigvee }⟨\alpha ⟩{\psi }_{\alpha }$$

$$\underset{\alpha \in A}{\bigwedge }[\alpha ]{\phi }_{\alpha }\vee \underset{\alpha \in B}{\bigvee }⟨\alpha ⟩{\psi }_{\alpha }$$

Full text

monitorability, linear-time and branching-time logics, monitor synthesis

††copyright: rightsretained††journal: PACMPL††journalyear: 2019††journalvolume: 3††journalnumber: POPL††article: 52††publicationmonth: 1††doi: 10.1145/3290365††ccs: Theory of computation Logic and verification††ccs: Theory of computation Modal and temporal logics††ccs: Theory of computation Automata over infinite objects††ccs: Theory of computation Complexity theory and logic

1. Introduction

The ubiquitous proliferation of software—from high-frequency stock market trading and autonomous vehicles, down to mundane objects such as mobile phones and household appliances—makes a strong case for stringent software correctness requirements. This proliferation has also substantially altered the manner in which software is developed and deployed. Today’s software often consists of multiple components (e.g., third-party libraries, mobile apps, microservices, cloud services etc.) that are developed and maintained by independent software organisations. In this setting, access to the components’ internal workings varies (e.g., open-source versus proprietary code) and different components may be subject to diverse quality controls. Moreover, time-to-market constraints often impose multiple deployment phases where software is rolled out in stages and third-party components change without notice from one deployment phase to the next. Requirements from various stakeholders may also evolve between deployment phases and occasionally become conflicting. These realities suggest that there is no silver bullet for ensuring software correctness. Any adequate solution will most likely need to employ multiple verification techniques (e.g., testing, model checking, theorem proving, log analysis, type checking, monitoring etc.) in a coherent manner, spanning the various stages of the software development lifecyle.

Runtime Verification (RV) (Bartocci et al., 2018) is a lightweight verification technique that checks for the correctness of the system under scrutiny by analysing the current execution exhibited by the system. RV generally assumes a logic (or some other formal language) for describing the correctness specifications of the system. From these specifications, (online) RV generates computational entities called monitors that are then instrumented to run with the system so as to incrementally analyse its execution (expressed as a trace of captured events) and reach (irrevocable) judgements relating to system violations or satisfactions for these specifications. These characteristics make RV an ideal candidate to be used in a multi-pronged approach towards ensuring software correctness: it can verify the correctness of components that are either not available for inspection prior to deployment, or are too expensive to check via more exhaustive and less scalable verification techniques such as model checking (Baier et al., 2008; Clarke et al., 1999). Importantly, in settings where multiple verification techniques are used, one cannot necessarily expect specifications to be expressed in a language tailored specifically to RV. Indeed, the use of disparate specification logics specific to every verification technique that is used for validating system correctness is expensive. Moreover, an RV-specific property language leads to a poor separation of concerns between the effort required to formulate the specifications and the engineering endeavour needed to determine how to best verify them. Therefore it is natural and important to develop RV foundations that are based on general-purpose specification languages, which subsume application-specific verification concerns.

In order for RV to be used effectively in this way, a few foundational questions need to be addressed. Principal among them is the question of monitorability: for sufficiently expressive specification logics, it is often the case that some specifications cannot be monitored at runtime. For example, the observation of finite executions does not give sufficient information to decide whether the specification “every request is eventually followed by an answer” is satisfied. It is thus important to identify which specifiable properties are monitorable and which are not, since this directly impinges on whether to use RV or some other verification technique instead. Another fundamental question is that of monitor correctness. Monitors are often considered part of the trusted computing base and any errors in their code could either invalidate the runtime analysis they perform or, even worse, compromise the execution of the system itself. In order to ensure monitor correctness, one must first establish what it means for a monitor to adequately verify a specification at runtime. In fact, there may be a number of plausible definitions for this notion, each contributing to different monitor implementations. The question of what it means to adequately verify a specification at runtime directly impacts the question of monitorability as well, and guides the design of algorithms for the synthesis of correct monitors from monitorable properties. A third fundamental question concerns the limits of monitor expressiveness. After one has established the monitorability of a set of properties from a reasonably general specification logic, it is important to know whether this set contains all properties that can be expressed in the logic and can, at the same time, be monitored at runtime. This is the question of maximality of the monitorable fragment of the specification language, and its importance lies in the knowledge that one can identify a logical sub-language that syntactically characterises all monitorable properties: syntactic characterisations of monitorable properties provide a core calculus for conducting further studies and facilitate tool construction.

In prior work (Francalanza et al., 2015, 2017b; Aceto et al., 2017a; Francalanza et al., 2017a; Aceto et al., 2018a), these foundational questions have been investigated for a highly expressive logic called Hennessy-Milner Logic with recursion (recHML) (Larsen, 1990), a variant of the modal $\mu$-calculus (Kozen, 1983), that can embed a variety of widely used logics such as LTL and CTL, thus guaranteeing a good level of generality for the obtained results. A distinctive aspect of this programme of study is the differentiation between the semantics of the logic on the one hand, and the operational semantics of monitors on the other, which mirrors the separation of concerns required for the multi-pronged verification approach advocated earlier. Within the proposed framework, the definitions of monitorability and correctness emerge naturally as relationships between the two semantics. That is, the relationship between the verdicts reached by a monitor and the satisfaction of a specification by the observed system naturally characterises both the monitor’s correctness and the specification’s monitorability.

Despite its merits, that body of work remains rather disconnected from the more established classical results on monitorability (Manna and Pnueli, 1991; Chang et al., 1992; Pnueli and Zaks, 2006; Bauer et al., 2010; Falcone et al., 2012a). One major complication obstructing a unified understanding of all these monitoring theories is the fact that the former work on recHML is carried out for a branching-time semantics, whereas the classical theories target specifications for a linear-time semantics. Propitiously, however, the modal $\mu$-calculus also has a well-established linear-time semantics, which can be easily adapted to recHML. This provides us with an opportunity to extend the principled framework developed in Aceto et al. (2017a) and Francalanza et al. (2015, 2017b) to a linear-time setting, offering an ideal basis to better understand the connections between monitorability for branching-time and linear-time specifications. We contend that this framework is general enough to lay the foundations for a potential unified theory of monitorability.

Contributions and Synopsis.

This paper sets out to establish a comprehensive theory of monitorability for recHML, by investigating the monitorability of that logic with a linear-time semantics and then comparing the obtained results with those presented in the literature in a branching-time setting. We identify the trade-offs between monitoring guarantees and expressiveness: In general, the more we expect from monitors, the fewer specifications can be monitored. Here we establish an expressiveness hierarchy within linear-time recHML and identify exactly what kind of guarantees can be given for each type of specification.

• •

We show that, compared to branching time, linear time allows for a much stronger notion of monitorability requiring that a monitor correctly report both the satisfaction and the violation of the property it checks on all system executions. We identify a fragment of recHML that captures exactly linear-time properties with such monitors (Prop. 4.7), and show how to synthesise monitors from them (Def. 4.4).

• •

For any collection of monitors with irrevocable acceptance and rejection verdicts, which are reported after examining a finite prefix of the observed execution, we show a strong maximality result for the above-mentioned logical fragment (Thm. 4.8), which guarantees that all monitorable properties of traces can be expressed in that fragment of recHML.

• •

We apply the weaker notion of monitorability called partial monitorability from Francalanza et al. (2017b), which guarantees that a monitor does not reach an incorrect verdict and reaches a verdict for either all violations or all satisfactions. Again, we give a syntactic characterisation of linear-time properties that can be monitored with such monitors (Prop. 4.18), we show how to synthesise correct monitors from them (Def. 4.12), and prove maximality results.

• •

We establish a relationship between specifications that are partially monitorable in branching-time and in linear-time semantics (Sec. 5). To establish this result, we study how considering specifications over both finite and infinite executions affects monitorability. Our main observation here is that the syntactic fragment identified as partially monitorable with respect to branching-time semantics and the one identified as partially monitorable with respect to linear-time semantics are equally expressive under linear-time semantics over a finite set of actions. This bridges the gap in the treatment of monitorability on linear- versus branching-time domains.

Our results establish a unified foundation for an increasingly important verification technique, covering both branching-time and linear-time specifications. We establish simple syntactic characterisations for specifications that can be monitored at runtime for various monitor requirements. For each characterisation, we provide a synthesis function that automates the generation of the corresponding monitors, whose correctness proofs depend on delicate arguments about the monitor semantics. This approach facilitates the design and implementation of correct monitors, along the lines of previous work on tool construction (Attard and Francalanza, 2016; Attard et al., 2017; Francalanza and Seychell, 2015). Throughout our technical development, we also highlight the subtle aspects of moving between semantics of branching processes, infinite traces, and potentially finite traces, and provide ample discussion on how they affect monitorability. Crucially, our results are not just limited to our line of work. For instance, the syntactic characterisations of monitorable properties set maximality limits to a number of existing RV tools using popular logics such as LTL since these logics can be embedded in our general language recHML.

The proofs of all the results in the paper may be found in the appendix.

2. Preliminaries

We provide a brief overview of our touchstone logic, recHML (Larsen, 1990; Aceto et al., 2007), a reformulation of the highly expressive and extensively studied modal $\mu$-calculus (Kozen, 1983).

2.1. The Syntax

The logic described in Fig. 1 is a mild generalisation of recHML (Larsen, 1990; Aceto et al., 2007). It assumes a set of actions, $\alpha,\beta,\ldots\in\textsc{Act}$, together with a distinguished internal action $\tau$, where $\tau\not\in\textsc{Act}$. We refer to the actions in Act as external actions, as opposed to the action $\tau$, and use ${\mu\in\textsc{Act}\cup\left\{\tau\right\}}$ to refer to either. The metavariables $A,B,\ldots\subseteq\textsc{Act}$ range over sets of (external) actions, where the convenient notation $\overline{A}$ is occasionally used to denote $\textsc{Act}\setminus A$; whenever the context allows us to do so unambiguously, singleton sets $\left\{\alpha\right\}$ are also occasionally denoted as $\alpha$, and $\overline{\{\alpha\}}$ is occasionally denoted as $\overline{\alpha}$.

The grammar in Fig. 1 also 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 and universal modal operators that use sets of actions, $A$. A hallmark of the logic is the use of two recursion operators that express least or greatest fixpoints: formulae $\mathsf{min}\,X.\varphi$ and $\mathsf{max}\,X.\varphi$ bind free instances of the logical variable $X$ in $\varphi$, inducing the usual notions of open/closed formulae and formula equality up to alpha-conversion. A formula is said to be guarded if every fixpoint variable appears within the scope of a modality within its fixpoint binding. All formulae are assumed to be guarded (without loss of expressiveness (Kupferman et al., 2000)). For a formula $\varphi$, we use $l(\varphi)$ to denote the length of $\varphi$ as a string of symbols.

2.2. The models

We provide linear- and branching-time interpretations for the logic. The metavariables $t,u{\in}\textsc{Trc}=\textsc{Act}^{\omega}$ range over infinite sequences of external actions, abstractly representing complete system runs; the metavariable $\textsl{T}\subseteq\textsc{Trc}$ ranges over sets of traces. Finite traces, denoted as $s,r\in\textsc{Act}^{\ast}$, represent finite prefixes of a system run or finite executions. Explicit traces, denoted as $e,f\in{(\textsc{Act}\cup\{\tau\})}^{\ast}$, represent detailed finite prefixes of a system run that also include its internal transitions; the function $\lceil e\rceil$ returns the finite trace $s$ that is left after dropping all the $\tau$-actions from $e$. We say that two explicit traces agree on the external actions, denoted as $e_{1}\equiv_{\textsc{Act}}e_{2}$, whenever $\lceil e_{1}\rceil=\lceil e_{2}\rceil$. A trace (resp., finite trace) with action $\alpha$ at its head is denoted as $\alpha t$ (resp., $\alpha s$). An explicit trace with action $\mu$ at its head is denoted as $\mu e$. Similarly, a trace with a prefix $s$ and continuation $t$ is denoted as $st$.

The denotational semantic function $\llbracket-\rrbracket_{\textsc{L}}$ in Fig. 1 maps a formula to a set of traces, and is referred to as the linear-time semantics of recHML. It uses valuations that map logical variables to sets of traces, $\sigma:\textsc{LVar}\to\mathcal{P}(\textsc{Trc})$, to define the semantics by induction on the structure of the formulae. Intuitively, $\sigma(X)$ is the set of traces assumed to satisfy $X$. The cases for truth, falsehood, disjunction and conjunction are straightforward. An existential modal formula $\mathbf{\langle}A\mathbf{\rangle}\varphi$ denotes all traces with a prefix action $\alpha$ from the action set $A$ and a continuation that satisfies $\varphi$. A universal modal formula $\mathbf{[}A\mathbf{]}\varphi$ denotes all traces that are either not prefixed by any $\alpha$ in $A$, or have a continuation $u$ satisfying $\varphi$. The sets of traces satisfying the least and greatest fixpoint formulae, $\mathsf{min}\,X.\varphi$ and $\mathsf{max}\,X.\varphi$, are defined as intersection (resp., union) of all the pre-fixpoints (resp., post-fixpoints) of the function induced by the formula $\varphi$.

The second interpretation of recHML, denoted by $\llbracket-\rrbracket_{\textsc{B}}$, is defined in terms of processes, Prc, and is referred to as the branching-time semantics. It assumes a set of process states, $p,q,\ldots\in\textsc{Prc}$ where $\textsl{P}\subseteq\textsc{Prc}$, and a transition relation, $\longrightarrow\subseteq(\textsc{Prc}\times(\textsc{Act}\cup\left\{\tau\right\})\times\textsc{Prc})$. The triple $\langle\textsc{Prc},(\textsc{Act}\cup\left\{\tau\right\}),\longrightarrow\rangle$ forms a Labelled Transition System (LTS) (Keller, 1976). The suggestive notation $p\xrightarrow{\;\mu\;}p^{\prime}$ denotes $(p,\mu,p^{\prime})\in\ \longrightarrow$; we also write $p\not\!\xrightarrow{\;\mu\;}$ to denote $\neg(\exists p^{\prime}\cdot\;p\xrightarrow{\;\mu\;}p^{\prime})$. We employ the usual notation for weak transitions and write $p\xRightarrow{\quad}p^{\prime}$ in lieu of $p(\xrightarrow{\;\tau\;})^{\ast}p^{\prime}$ and $p\xRightarrow{\;\mu\;}p^{\prime}$ for $p\xRightarrow{\quad}\cdot\xrightarrow{\;\mu\;}\cdot\xRightarrow{\quad}p^{\prime}$, referring to $p^{\prime}$ as a $\mu$-derivative of $p$. As we have done for strong transitions, for weak transitions we use $p\xRightarrow{\;\mu\;}$ to denote $\exists p^{\prime}\cdot\;p\xRightarrow{\;\mu\;}p^{\prime}$ and $p\centernot{\xRightarrow{\;\mu\;}}$ to denote $\neg(\exists p^{\prime}\cdot\;p\xRightarrow{\;\mu\;}p^{\prime})$. Sequences of weak transitions $p\xRightarrow{\alpha_{1}}\cdots\xRightarrow{\alpha_{n}}p^{\prime}$ are written as $p\xRightarrow{\;s\;}p^{\prime}$, where $s=\alpha_{1}\cdots\alpha_{n}$. Similarly, for strong transitions, $p\xrightarrow{\mu_{1}}\cdots\xrightarrow{\mu_{n}}p^{\prime}$ is written as $p\xrightarrow[]{\;e\;}\mathrel{\mkern-14.0mu}\rightarrow p^{\prime}$, where $e=\mu_{1}\cdots\mu_{n}$. We say that $p$ produces a trace $t=\alpha_{1}\alpha_{2}\cdots$ if there are processes $p_{0},p_{1},p_{2},\ldots$ such that $p=p_{0}$ and $p_{0}\xRightarrow{\;\alpha_{1}\;}p_{1}\xRightarrow{\;\alpha_{2}\;}p_{2}\cdots$. While an LTS can be used to model a single system, it can also model all possible system behaviours.

The branching-time semantics in Fig. 1 follows the linear-time semantics for most cases, using a valuation from variables to sets of processes, $\rho:\textsc{LVar}\to\mathcal{P}(\textsc{Prc})$, instead. The main differences are with respect to the modal formulae. A universal modal formula $\mathbf{[}A\mathbf{]}\varphi$ requires all $\alpha$-derivatives of a process, where $\alpha\in A$, to satisfy $\varphi$. By contrast, an existential modal formula $\mathbf{\langle}A\mathbf{\rangle}\varphi$ requires the existence of at least one $\alpha$-derivative, for some $\alpha\in A$, that satisfies $\varphi$.

For closed formulae, we use $\llbracket\varphi\rrbracket_{\textsc{L}}$ and $\llbracket\varphi\rrbracket_{\textsc{B}}$ in lieu of $\llbracket\varphi,\sigma\rrbracket_{\textsc{L}}$ and $\llbracket\varphi,\rho\rrbracket_{\textsc{L}}$ (for some $\sigma$ and $\rho$) resp., since the semantics is independent of the valuation. We also write $\llbracket\varphi\rrbracket$ instead of $\llbracket\varphi\rrbracket_{\textsc{L}}$ or $\llbracket\varphi\rrbracket_{\textsc{B}}$, whenever the correct interpretation can be discerned from the context or the specific interpretation is unimportant. Unless otherwise stated, we assume that the formulae we consider are all closed.

Example 2.1 (Expressiveness).

For arbitrary formulae $\varphi,\psi\in\textsc{recHML}$, we can encode the following characteristic LTL operators (Clarke et al., 1999) as:

[TABLE]

Example 2.2 (Comparison).

Assume $\textsc{Act}=\left\{a,b,c\right\}$. Consider the two formulae

[TABLE]

together with the trace (denoted by the $\omega$-regular expression) $t=(a.b)^{\omega}$, and the (non-deterministic) process (described by the regular CCS syntax (Milner, 1989)) $p=\textsf{rec}\,x.(a.{b.{x}}+a.{a.{x}}+a.{\textsf{nil}})$. In particular, we note that $p$ can produce the infinite trace $t$.

Whereas $t\in\llbracket\varphi_{1}\rrbracket_{\textsc{L}}$, we have $p\not\in\llbracket\varphi_{1}\rrbracket_{\textsc{B}}$ because along one branch we have $p\xRightarrow{\;a\;}a.{p}$ and $a.{p}\not\in\llbracket\mathbf{[}a\mathbf{]}\mathsf{ff}\rrbracket_{\textsc{B}}$. In linear-time semantics, the equality $\llbracket\mathbf{\langle}A\mathbf{\rangle}\mathsf{tt}\mathbf{\vee}\mathbf{\langle}\overline{A}\mathbf{\rangle}\mathsf{tt}\rrbracket_{\textsc{L}}=\llbracket\mathsf{tt}\rrbracket_{\textsc{L}}$ holds for each $A$. One can also easily deduce that $\llbracket\mathbf{[}A\mathbf{]}\mathsf{tt}\rrbracket=\llbracket\mathsf{tt}\rrbracket$ for both linear- and branching-time semantics from the semantics of Fig. 1. Hence, in our case (where $\textsc{Act}=\left\{a,b,c\right\}$), we obtain $\llbracket\mathbf{\langle}a\mathbf{\rangle}\mathsf{tt}\mathbf{\vee}\mathbf{\langle}\left\{b,c\right\}\mathbf{\rangle}\mathsf{tt}\rrbracket_{\textsc{L}}=\llbracket\mathsf{tt}\rrbracket_{\textsc{L}}$ by instantiating $\llbracket\mathbf{\langle}A\mathbf{\rangle}\mathsf{tt}\mathbf{\vee}\mathbf{\langle}\overline{A}\mathbf{\rangle}\mathsf{tt}\rrbracket_{\textsc{L}}=\llbracket\mathsf{tt}\rrbracket_{\textsc{L}}$ with $A=\left\{a\right\}$. As a result, $\varphi_{2}$ is equivalent to $\mathsf{tt}$ under linear-time semantics and we have $t{\in}\llbracket\varphi_{2}\rrbracket_{\textsc{L}}$ for every trace $t$. However, under branching-time semantics $\llbracket\mathbf{\langle}a\mathbf{\rangle}\mathsf{tt}\mathbf{\vee}\mathbf{\langle}\left\{b,c\right\}\mathbf{\rangle}\mathsf{tt}\rrbracket_{\textsc{B}}\neq\llbracket\mathsf{tt}\rrbracket_{\textsc{B}}$ (one witness for the inequality is the deadlocked process nil, $\llbracket\mathsf{tt}\rrbracket_{\textsc{B}}\ni\textsf{nil}\not\in\llbracket\mathbf{\langle}a\mathbf{\rangle}\mathsf{tt}\mathbf{\vee}\mathbf{\langle}\left\{b,c\right\}\mathbf{\rangle}\mathsf{tt}\rrbracket_{\textsc{B}}$). In fact, $p\xrightarrow{\;a\;}\textsf{nil}$ and thus $p\not\in\llbracket\varphi_{2}\rrbracket_{\textsc{B}}$. $\hfill\qed$

Remark*.*

Action sets $A$ in $\mathbf{[}A\mathbf{]}\varphi$ and $\mathbf{\langle}A\mathbf{\rangle}\varphi$ are typically expressed using predicates in tools such as those described in Attard and Francalanza (2016), Attard et al. (2017) and Aceto et al. (2018b). For example, modalities can be labelled by an output action on port $x$ carrying payload $\langle 8,y\rangle$ where the data variables $x$ and $y$ are constrained by conditions, as in $\mathbf{[}\textbf{out}(x,\langle 8,y\rangle),(192.188.34.42\geq x\geq 192.188.34.1)\wedge\textbf{mod}(y)=1\mathbf{]}\varphi$. In the sequel, we shall assume that Act (and thus any action set $A$) is a finite set of actions. This helps to simplify our technical development and enables us to focus on the core issues being studied. However, finite action sets are not necessarily a limitation since, in most cases, infinite data sets can be treated in a finite manner using standard symbolic techniques (e.g., see Francalanza (2017) for a recent treatment of the subject in the context of monitors). $\hfill\qed$

Remark*.*

For a finite set $I$ of indices, the (standard) notation $\bigwedge_{i\in I}\varphi_{i}$ denotes $\mathsf{tt}$ when $I=\emptyset$, and a conjunction of the formulae in $\{\varphi_{i}\mid i\in I\}$ when $I\neq\emptyset$. Similarly $\bigvee_{i\in I}\varphi_{i}$ denotes $\mathsf{ff}$ when $I=\emptyset$, and a disjunction of the formulae in $\{\varphi_{i}\mid i\in I\}$ when $I\neq\emptyset$. These notations are justified by the fact that $\vee$ and $\wedge$ are commutative and associative with respect to all the semantics considered in the paper. We also observe that, for both semantics, $\mathbf{[}A\mathbf{]}\varphi$ is equivalent to $\bigwedge_{\alpha\in A}\mathbf{[}\alpha\mathbf{]}\varphi$, and $\mathbf{\langle}A\mathbf{\rangle}\varphi$ is equivalent to $\bigvee_{\alpha\in A}\mathbf{\langle}\alpha\mathbf{\rangle}\varphi$ for finite $A$, so we use these equivalent notations interchangeably. $\hfill\qed$

3. A monitoring framework

A distinctive feature of the work in Aceto et al. (2017a, 2018a) and Francalanza et al. (2017b) is the full description of the monitoring setup used, which incorporates the monitor definition together with the system instrumentation mechanism—monitor compositionality results have shown that the semantics of monitors in an instrumented setup differs substantially from that given for monitors in isolation (Francalanza, 2016, 2017). Here we follow this comprehensive approach.

3.1. Regular Monitors

Regular monitors are LTSs defined by the grammar and transition rules in Fig. 2, used already in Aceto et al. (2017a) and Francalanza et al. (2017b). A transition $m\xrightarrow{\;\alpha\;}n$ denotes that the monitor in state $m$ can analyse the (external) action $\alpha$ and transition to state $n$. Monitors may reach any one of three verdicts after analysing a finite trace: acceptance, yes, rejection, no, and the inconclusive verdict end. We highlight the transition rule for verdicts in Fig. 2, describing the fact that from a verdict state any action can be analysed by transitioning to the same state; verdicts are thus irrevocable. The remaining constructs and transitions are standard. If at most one of the verdicts $\textsf{yes},\textsf{no}$ appears in $m$, then $m$ is called a single-verdict monitor. Otherwise, $m$ is called a dual-verdict monitor. Just like for formulae, we use $l(m)$ to denote the length of $m$ as a string of symbols. In the sequel, for a finite nonempty set of indices $I$, we use notation $\sum_{i\in I}m_{i}$ to denote a combination of the monitors in $\{m_{i}\mid i\in I\}$ using the operator $+$. The notation is justified, because $+$ is commutative and associative with respect to the transitions that a resulting monitor can exhibit. We also use the shorthand notation A.$$m to denote $\sum_{\alpha{\in}A}\alpha.{m}$ (for finite non-empty $A$). The regular monitors in Fig. 2 have an important property, namely that their state space, i.e., the set of reachable states, is finite. This is a valuable property for ensuring reasonable overheads in terms of the amount of memory the monitor will use at runtime (see Prop. 3.2, whose proof is in Sec. A.1).

Lemma 3.1** (Verdict Persistence).**

$v\xrightarrow[]{\;e\;}\mathrel{\mkern-14.0mu}\rightarrow m\text{ implies }m=v.$∎

Definition 3.1 (Monitor Reachable States).

$\textsf{reach}(m)\,\overset{\leavevmode\resizebox{6.0pt}{}{\,{def}}\,}{=}\,\{\,n\,\mid\,\exists e\cdot m\xrightarrow[]{\;e\;}\mathrel{\mkern-14.0mu}\rightarrow n\,\}.$ $\hfill\qed$

Proposition 3.2**.**

Regular monitors are finite state i.e., for all $m\in\textsc{REMon}$, $\textsf{reach}(m)$ is finite. ∎

We define the following behavioural predicate on monitors, which relates to their correctness.

Definition 3.2 (Monitor Consistency).

A monitor $m$ is consistent when there is no finite trace $s$ such that $m\xRightarrow{\;s\;}\textsf{yes}$ and $m\xRightarrow{\;s\;}\textsf{no}$. $\hfill\qed$

Monitors are intended to run in conjunction with the system (i.e., process) they are analysing. Following Francalanza (2016, 2017) and Francalanza et al. (2017b), Fig. 2 defines a transition relation for a process $p$ instrumented with a monitor $m$, denoted as $m\triangleleft\,p$. The relation is parametric with respect to the transition semantics of the process $p$ and the monitor, as long as the latter includes the inconclusive verdict end (e.g., the monitor transition semantics given in Fig. 2 does). The semantics relegates the monitor $m$ to a passive role in an instrumented system $m\triangleleft\,p$, meaning that $m\triangleleft\,p$ transitions with an external action $\alpha$ only when $p$ transitions with that action. For instance, when $p$ transitions with action $\alpha$ to some $p^{\prime}$, and $m$ can analyse this action and transition to state $m^{\prime}$, the instrumented pair transitions in lockstep to $m^{\prime}\triangleleft\,p^{\prime}$; see rule iMon. Conversely, if $p$ wants to transition with an action $\alpha$ that the instrumented monitor is not able to analyse (perhaps due to underspecification), the instrumented system is still allowed to transition with $\alpha$, but the monitor analysis is prematurely aborted to the inconclusive state; see rule iTer. The other rules allow monitors and processes to execute independently of one another with respect to internal ($\tau$-)moves.

Example 3.1.

When the monitor $\textsf{rec}\,x.(a.{x}+b.{\textsf{yes}})$ is instrumented with the process $a.{\textsf{rec}\,x.b.{x}}$, it can reach an acceptance verdict thus:

[TABLE]

However, if the same process is instrumented with a slightly different monitor $\textsf{rec}\,x.(a.{a.{x}}+b.{\textsf{yes}})$ we obtain a different verdict.

[TABLE]

The last transition is obtained via rule iTer, whereby the process exhibited an action that the current monitor state was unable to analyse (i.e., it could only analyse action $a$, not $b$). $\hfill\qed$

The following lemmata describe how the respective monitor and system LTSs can be composed and decomposed according to instrumentation  (Francalanza, 2016; Francalanza et al., 2017b).

Lemma 3.3** **(General Unzipping

).

$m\triangleleft\,p$* $\xRightarrow{\;s\;}$ $n\triangleleft\,q$ implies*

• •

$p\xRightarrow{\;s\;}q$* and*

• •

$m\xRightarrow{\;s\;}n$* or ($\exists s_{1},s_{2},\alpha,m^{\prime}\cdot s=s_{1}\alpha s_{2}$ and $m\xRightarrow{\;s_{1}\;}m^{\prime}\not\!\xrightarrow{\;\tau\;}$ and $m^{\prime}\not\!\xrightarrow{\;\alpha\;}$ and $n=\textsf{end}$). ∎*

Lemma 3.4** **(Zipping

).

$(p\xRightarrow{\;s\;}q\text{ and }m\xRightarrow{\;s\;}n)$* implies ${m\triangleleft\,p\xRightarrow{\;s\;}n\triangleleft\,q}$. ∎*

Within this framework, we can formalise our understanding of process and trace acceptance and rejection by a monitor. Acceptances and rejections will constitute the monitoring counterpart to formula satisfactions and violations from Sec. 2 when we consider our definitions of monitorability.

Definition 3.3 (Process and Trace Acceptance and Rejection).

A monitor $m$ rejects $p$ along $s$, denoted as $\textbf{rej}(m,p,s)$, if $m\triangleleft\,p\xRightarrow{\;s\;}\textsf{no}\triangleleft\,p^{\prime}$ for some $p^{\prime}$. Similarly, $m$ accepts $p$ along $s$, denoted as $\textbf{acc}(m,p,s)$, if $m\triangleleft\,p\xRightarrow{\;s\;}\textsf{yes}\triangleleft\,p^{\prime}$ for some $p^{\prime}$.

• •

A monitor $m$ rejects (resp., accepts) $t$, using the abuse of notation $\textbf{rej}(m,t)$ (resp., $\textbf{acc}(m,t)$), if $\exists p,s,u$ such that ${t=su}$ and $\textbf{rej}(m,p,s)$ (resp., $\textbf{acc}(m,p,s)$).

• •

A monitor $m$ rejects (resp., accepts) $p$, using the abuse of notation $\textbf{rej}(m,p)$ (resp., $\textbf{acc}(m,p)$), if $\exists s$ such that $\textbf{rej}(m,p,s)$ (resp., $\textbf{acc}(m,p,s)$).

We also say that $m$ rejects $s$ as a shorthand for $\exists p\cdot\textbf{rej}(m,p,s)$, and similarly, $m$ accepts $s$ is a shorthand for $\exists p\cdot\textbf{acc}(m,p,s)$. $\hfill\qed$

As Defs. 3.3, 3.3 and 3.4 make clear, a monitor accepts or rejects a finite trace $s$ iff it can transition to the appropriate verdict by reading $s$. This hints at the fact that each monitor might be “equivalent to a deterministic one”. As we will see in Prop. 3.11, this is indeed the case.

3.2. Parallel Composition of Monitors

When relating monitors to formulae, it may be convenient not to view monitors as one monolithic entity but rather as a system of sub-monitors where the constituent submonitors are concerned with checking specific subformulae. For instance, the use of sub-monitors executing in parallel facilitates the synthesis of monitors from formulae in a compositional fashion. Monitors with parallel composition, $m,n\in\textsc{Mon}$, are defined by the grammar and transition rules in Fig. 3. In particular, we endow monitors with conjunctive parallelism, ${\otimes}$, and disjunctive parallelism, ${\oplus}$. We use the notation ${\odot}$ to range over either ${\otimes}$ or ${\oplus}$ (i.e., ${\odot}\in\left\{{\otimes},{\oplus}\right\}$).

Fig. 3 also outlines the behaviour of parallel monitors. Rule mPar states that both submonitors need to be able to analyse an external action $\alpha$ for their parallel composition to transition with that action. The rules in Fig. 3 also allow $\tau$-transitions for the reconfiguration of parallel compositions of monitors. For instance, rules mVrC1 and mVrC2 describe the fact that, whereas yes verdicts are uninfluential in conjunctive parallel compositions, no verdicts supersede the verdicts of other monitors in a conjunctive parallel compositions (Fig. 3 omits the obvious symmetric rules). The dual applies for yes and no verdicts in a disjunctive parallel composition, as described by rules mVrD1 and mVrD2. Rule mVrE applies to both forms of parallel composition and consolidates multiple inconclusive verdicts. Finally, rules mTauL and its dual mTauR (omitted) are contextual rules for these monitor reconfiguration steps.

We identify a useful monitor predicate that obviates the need for the rule iTer of Fig. 2 that prematurely terminates monitors; see 3.1. In the case of parallel monitors, it also allows us to neatly decompose the monitor behaviour in terms of the respective sub-monitors.

Definition 3.4 (Monitor Reactivity).

We call a monitor $m$ reactive when for every $n\in\textsf{reach}(m)$ and $\alpha\in\textsc{Act}$, there is some $n^{\prime}$ such that $n\xRightarrow{\;\alpha\;}n^{\prime}$. $\hfill\qed$

3.2 below indicates why the assumption that $m_{1}$ and $m_{2}$ are reactive is needed in Lem. 3.5, which states that parallel monitors behave as expected with respect to the acceptance and rejection of traces as long as the consitituent submonitors are reactive.

Example 3.2.

Assume that $\textsc{Act}=\left\{a,b\right\}$. The monitors $a.{\textsf{yes}}+b.{\textsf{no}}$ and $\textsf{rec}\,x.(a.{x}+b.{\textsf{yes}})$ are both reactive. The monitor $m=a.{\textsf{yes}}{\otimes}b.{\textsf{no}}$, however, is not reactive. Since the submonitor $a.{\textsf{yes}}$ can only transition with $a$, according to the rules of Fig. 3, $m$ cannot transition with any action that is not $a$. Similarly, as the submonitor $b.{\textsf{no}}$ can only transition with $b$, $m$ cannot transition with any action that is not $b$. Thus, $m$ cannot transition to any monitor, and therefore it cannot reject or accept any trace. By contrast, the monitor $n=(a.{\textsf{yes}}+b.{\textsf{end}}){\otimes}(b.{\textsf{yes}}+a.{\textsf{end}})$ is reactive, because its constituent submonitors are reactive as well. $\hfill\qed$

Lemma 3.5** (Monitor Composition and Decomposition).**

For reactive $m_{1}$ and $m_{2}$:

• •

$m_{1}{\otimes}m_{2}$* rejects $t$ if and only if either $m_{1}$ or $m_{2}$ rejects $t$.*

• •

$m_{1}{\otimes}m_{2}$* accepts $t$ if and only if both $m_{1}$ and $m_{2}$ accept $t$.*

• •

$m_{1}{\oplus}m_{2}$* rejects $t$ if and only if both $m_{1}$ and $m_{2}$ reject $t$.*

• •

$m_{1}{\oplus}m_{2}$* accepts $t$ if and only if either $m_{1}$ or $m_{2}$ accepts $t$. ∎*

Parallel monitors are a convenient formalism for constructing monitors in a compositional fashion and facilitate the definition of monitor synthesis functions from a specification logic. However, these monitors are only as expressive as regular monitors, as Prop. 3.8 demonstrates. Sec. 3.3 is devoted to the proof of this result.

3.3. Monitor Transformations: Parallel to Regular

We describe how one can transform a parallel monitor to a verdict-equivalent regular one. For this, we use known results about alternating finite automata, restated here for completeness.

Definition 3.5 (Alternating Automata).

An alternating finite automaton is a quintuple $A=(Q,\Sigma,q_{0},\delta,F)$, where $Q$ is a finite set of states, $\Sigma$ is a finite alphabet, $q_{0}$ is the starting state, $F\subseteq Q$ is the set of accepting/final states, and $\delta:(Q\times\Sigma)\to(2^{Q}\to\{0,1\})$ is the transition function. An alternating finite automaton is non-deterministic (NFA) if for each $\alpha\in\Sigma$ and $q\in Q$, there is some $S_{q,\alpha}\subseteq Q$, such that for all $S\subseteq Q$, $\delta(q,\alpha)(S)=1$ if and only if $S\cap S_{q,a}\neq\emptyset$. $\hfill\qed$

Intuitively, given a state $q\in Q$ and a symbol $\alpha\in\Sigma$, $\delta$ returns a boolean function on $2^{Q}$ that evaluates, given a truth-assignment on the states of $Q$ (represented by a subset of $Q$), an assigned truth-value for $q$. We can extend the transition function to $\delta^{*}:(Q\times\Sigma^{*})\to(2^{Q}\to\{0,1\})$, so that $\delta^{*}(q,\varepsilon)(R)=1$ iff $q\in R$, and $\delta^{*}(q,\alpha w)(R)=\delta(q,\alpha)(\{q^{\prime}\in Q\mid\delta^{*}(q^{\prime},w)(R)=1\})$. We say that the automaton accepts $w\in\Sigma^{*}$ when $\delta^{*}(q_{0},w)(F)=1$, and that it recognizes $L\subseteq\Sigma^{*}$ when $L$ is the set of strings accepted by the automaton.

Definition 3.6 (Monitor Language Acceptance and Rejection).

A monitor $m$ accepts (resp., rejects) a set of finite traces (i.e., a language) $L\subseteq\textsc{Act}^{*}$ when for every $s\in\textsc{Act}^{*}$, $s\in L$ if and only if $m$ accepts (resp., rejects) $s$. We call the set that $m$ accepts (resp., rejects) $L_{a}(m)$ (resp., $L_{r}(m)$). $\hfill\qed$

Proposition 3.6**.**

*For every reactive parallel monitor $m$, there is an alternating automaton that accepts $L_{a}(m)$ and one that accepts $L_{r}(m)$. *

Proof.

We describe the process of constructing an alternating automaton that accepts $L_{a}(m)$ — the case for $L_{r}(m)$ is similar. We assume that for every variable $x$ that appears in $m$, there is a unique submonitor of $m$ of the form $\textsf{rec}\,x.n$, such that $x$ appears in $n$. The automaton for $m$ is $A_{m}=(Q,\textsc{Act},m,\delta,F)$, where

• •

$Q$ is the set of submonitors of $m$;

• •

$F=\{n\in Q\mid n\text{ accepts }\varepsilon\}$;

• •

Let for every $S\subseteq Q$, $\delta_{0}(q,\alpha)(S)=1$ iff $q\in F$; $\delta$ is the closure of $\delta_{0}$ under the following conditions. For every $S\subseteq Q$:

• –

if $n\in S$, then $\delta(\alpha.n,\alpha)(S)=1$;

• –

if $\delta(n,\alpha)(S)=1$ or $\delta(n^{\prime},\alpha)(S)=1$, then $\delta(n+n^{\prime},\alpha)(S)=1$;

• –

if $\delta(n,\alpha)(S)=1$ or $\delta(n^{\prime},\alpha)(S)=1$, and $n\xRightarrow{\;\alpha\;}$ and $n^{\prime}\xRightarrow{\;\alpha\;}$, then $\delta(n{\oplus}n^{\prime},\alpha)(S)=1$;

• –

if $\delta(n,\alpha)(S)=1$ and $\delta(n^{\prime},\alpha)(S)=1$, then $\delta(n{\otimes}n^{\prime},\alpha)(S)=1$;

• –

if $\delta(n,\alpha)(S)=1$ and $\textsf{rec}\,x.n\in Q$, then $\delta(\textsf{rec}\,x.n,\alpha)(S)=\delta(x,\alpha)(S)=1$.

In Sec. A.4, we present the remaining proof, that $m$ accepts $s$ if and only if $\delta^{*}(m,s)(F)=1$. ∎

Remark*.*

The assumption that the monitor is reactive is necessary for the construction in the proof of Prop. 3.6 to be correct. Consider, for example, the monitor $m_{1}=a.{a.{\textsf{yes}}}{\oplus}a.{b.{\textsf{yes}}}$. Although $a.{a.{\textsf{yes}}}\xrightarrow{\;a\;}a.{\textsf{yes}}\xrightarrow{\;a\;}\textsf{yes}$, the monitor does not accept any trace since $b.{\textsf{yes}}\centernot{\xrightarrow{\;a\;}}$. By the construction, in the resulting alternating automaton, $F=\{\textsf{yes}\}$, and therefore $\delta(\textsf{yes},a)(F)=1$, implying that $\delta(a.\textsf{yes},a)(F)=1$, in turn implying that $\delta^{*}(m_{1},aa)(F)=1$, according to the closure conditions for $\delta$. Therefore, $aa$ is a finite trace that the automaton accepts and the monitor does not.

In light of our assumption that monitor $m$ in Prop. 3.6 is reactive, the third condition for $\delta$ in the construction in the proof of the proposition may seem superfluous. However, reactivity does not transfer to submonitors. For example, let $m_{2}=(a.{\textsf{yes}}{\oplus}b.{\textsf{yes}})+a.{\textsf{end}}+b.{\textsf{end}}$. Reasoning similarly to the above argument for $m_{1}$, $m_{2}$ is a reactive parallel monitor, which accepts no traces. On the other hand, a more naive construction that ensures that $\delta(n{\oplus}n^{\prime},\alpha)(S)=1$ whenever $\delta(n,\alpha)(S)=1$ or $\delta(n^{\prime},\alpha)(S)=1$, would result in an automaton that accepts the finite trace $a$.

As we see in the remainder of this section, Prop. 3.6 implies that potentially infinite-state parallel monitors are equivalent to finite-state regular monitors. The subtleties that we pointed out are the trade-off for keeping the construction of the alternating automaton straightforward. $\hfill\qed$

Corollary 3.7**.**

For every reactive parallel monitor $m$, there is an NFA that accepts $L_{a}(m)$ and an NFA that accepts $L_{r}(m)$, and each has at most $2^{l(m)}$ states.

Proof.

The alternating automaton that is constructed in the proof of Prop. 3.6 has at most as many states as there are submonitors in $m$ which, in turn, are not more than $l(m)$. Furthermore, it is a known result that every alternating automaton with $k$ states can be converted into an NFA with at most $2^{k}$ states that accepts the same language (Chandra et al., 1981; Fellah et al., 1990). ∎

We now have all the ingredients to complete the proof of Prop. 3.8. This relies on a notion of monitor equivalence from Aceto et al. (2017b) that focusses on how monitors can reach verdicts.

Definition 3.7 (Verdict Equivalence).

Monitors $m$ and $n$ are acceptance equivalent (resp., rejection equivalent), denoted as $m\simeq_{\text{acc}}n$ (resp., $m\simeq_{\text{rej}}n$), if for every finite trace $s$, $m\xRightarrow{s}\textsf{yes}$ iff $n\xRightarrow{s}\textsf{yes}$ (resp., $m\xRightarrow{s}\textsf{no}$ iff $n\xRightarrow{s}\textsf{no}$). They are verdict equivalent, denoted as $m\simeq_{\text{ver}}n$, if they are both acceptance- and rejection-equivalent. $\hfill\qed$

Proposition 3.8**.**

For all reactive parallel monitors $m$, there exist regular monitors $n_{1},n_{2}$, and $n$ such that $n_{1}$ and $n_{2}$ are single-verdict monitors that are respectively acceptance-equivalent and rejection-equivalent to $m$, and $m$ and $n$ are verdict equivalent, and $l(n_{1}),l(n_{2}),l(n)=2^{O\left(l(m)\cdot 2^{l(m)}\right)}$.

Proof.

Let $A_{m}^{a}$ be an NFA for $L_{a}(m)$ with at most $2^{l(m)}$ states, and let $A_{m}^{r}$ be an NFA for $L_{r}(m)$ with at most $2^{l(m)}$ states, which exist by Cor. 3.7. From these NFAs, we can construct regular monitors $m_{R}^{a}$ and $m_{R}^{r}$, such that $m_{R}^{a}$ accepts $L_{a}(m)$ and $m_{R}^{r}$ rejects $L_{r}(m)$, and $l(m_{R}^{a}),l(m_{R}^{r})=2^{O\left(l(m)\cdot 2^{l(m)}\right)}$ (Aceto et al., 2016). Therefore, $m_{R}^{a}\simeq_{\text{acc}}m$ and $m_{R}^{r}\simeq_{\text{rej}}m$, and $m_{R}^{a}+m_{R}^{r}$ is regular and verdict-equivalent to $m$, and $l(m_{R}^{a}+m_{R}^{r})=2^{O\left(l(m)\cdot 2^{l(m)}\right)}$. ∎

The techniques of Aceto et al. (2016) can also be used to produce deterministic monitors.

Definition 3.8 ((Aceto et al., 2016)).

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

Example 3.3.

The monitor $a.{b.{\textsf{yes}}}+a.{a.}{\textsf{no}}$ is not syntactically deterministic while the verdict-equivalent monitor $a.$($b.{\textsf{yes}}+a.{\textsf{no}}$) is syntactically deterministic. $\hfill\qed$

One can also consider non-syntactic notions of determinism, such as if $m\xRightarrow{\;s\;}n$ and $m\xRightarrow{\;s\;}n^{\prime}$, then $n\simeq_{\text{ver}}n^{\prime}$. Lem. 3.9 shows that syntactic determinism implies this semantic notion. Henceforth we will simply say deterministic to mean syntactically deterministic.

Lemma 3.9** ((Aceto et al., 2016)).**

If $m$ is deterministic, $m\xRightarrow{\;s\;}n$, and $m\xRightarrow{\;s\;}n^{\prime}$, then $n\simeq_{\text{ver}}n^{\prime}$. ∎

Theorem 3.10** ((Aceto et al., 2016)).**

For every consistent regular monitor $m$, there is a verdict-equivalent deterministic regular monitor $n$ such that $l(n)=2^{2^{O(l(m))}}$. ∎

Proposition 3.11**.**

For every consistent reactive parallel monitor $m$, there is a verdict-equivalent deterministic regular monitor $n$ such that $l(n)=2^{2^{2^{O\left(l(m)\cdot 2^{l(m)}\right)}}}$.

Proof.

Using Prop. 3.8, $m$ can be translated into a (possibly nondeterministic) verdict-equivalent (hence consistent) regular monitor $n_{r}$, such that $l(n_{r})=2^{O\left(l(m)\cdot 2^{l(m)}\right)}$. Thm. 3.10 can then be used to convert $n_{r}$ into a verdict-equivalent deterministic regular monitor $n$, such that $l(n)=2^{2^{O(l(n_{r}))}}$. Therefore, $l(n)=2^{2^{2^{O\left(l(m)\cdot 2^{l(m)}\right)}}}$. ∎

4. Monitorability for recHML

Monitorability is the study of the relationship between the semantics of a logic on the one hand (i.e., satisfactions and violations), and the verdicts that can be discerned by the monitoring setup on the other (i.e., acceptances and rejections). The concept relies on what a correct monitor for a particular formula is, which, in turn, defines what it means for a formula to be monitorable. In this section we focus on the monitorability of recHML. Based on the definition of trace acceptance and rejection of Def. 3.3, we adapt the concepts of monitor soundness and completeness (with respect to a formula) from Francalanza et al. (2017b) to the linear-time setting.

Definition 4.1 (Linear-time Monitor Soundness and Completeness).

• •

A monitor $m$ is sound for a (closed) formula $\varphi$ of recHML over traces if, for all $t\in\textsc{Trc}$:

• –

$\textbf{rej}(m,t)$ implies $t\not\in\llbracket\varphi\rrbracket_{\textsc{L}}$;

• –

$\textbf{acc}(m,t)$ implies $t\in\llbracket\varphi\rrbracket_{\textsc{L}}$.

• •

A monitor $m$ is violation-complete for a (closed) formula $\varphi$ of recHML over traces if for all $t\in\textsc{Trc}$, $t\not\in\llbracket\varphi\rrbracket_{\textsc{L}}$ implies $\textbf{rej}(m,t)$. It is satisfaction-complete if $t\in\llbracket\varphi\rrbracket_{\textsc{L}}$ implies $\textbf{acc}(m,t)$.

• •

A monitor $m$ is complete for a (closed) formula $\varphi$ of recHML if it is both violation- and satisfaction-complete for it. $\hfill\qed$

The definition of soundness and completeness for monitors depends on the semantics given to the formulae. Since we focus on linear-time semantics in this section, instead of saying that a monitor is sound or violation- or satisfaction-complete, or complete for a formula over traces, we respectively simply say that it is sound or violation- or satisfaction-complete, or complete for the formula. In Sec. 5, we will introduce variations of Def. 4.1 that depend on different semantics for recHML. Observe that a monitor that is sound for some formula must be consistent.

Following Francalanza et al. (2017b), we assume that the minimum requirement for a monitor to correctly correlate to a formula is for it to be sound. It can be however argued that, depending on the circumstance of the application requirements, different notions of completeness may be deemed adequate enough. It turns out that not all formulae can be monitored adequately at runtime. Moreover, the more stringent the requirement for adequate monitoring, the more are the formulae that cannot be monitored. In the remainder of the section, we consider different definitions for adequate monitoring and establish recHML monitorability results in each case.

In Sec. 4.1, we present monitorability results with respect to complete monitors. In Sec. 4.2, we introduce the additional requirement of tightness for a monitor, under which the monitor reaches a verdict as soon as it has read sufficient information from the input trace and not later. We explain what one needs to do to construct a tight monitor. In Sec. 4.3, we establish monitorability results for partially complete monitors, which are satisfaction-complete or violation-complete for their respective formulae, but are not required to be both. This relaxation allows us to monitor for more formulae. Finally, in Sec. 4.4, we examine what one must do to construct tight partially complete monitors, and we explain why the methods of Sec. 4.2 are not likely to apply for this case.

4.1. Complete Monitorability

We first consider (sound and) complete monitors as our notion of adequate monitoring for a particular formula. This induces the following definition of monitorable formula and (sub)logic.

Definition 4.2 (Complete Monitorability).

A formula $\varphi\in\textsc{recHML}$ is complete-monitorable over traces iff there exists a monitor $m$ that is sound and complete for it. A (sub)logic $\mathcal{L}\subseteq\textsc{recHML}$ is complete-monitorable over traces iff each formula $\varphi\in\mathcal{L}$ is complete-monitorable. $\hfill\qed$

Remark*.*

In this section we only use Def. 4.2 for the linear-time interpretation of recHML. However, its general form allows it to be used for other interpretations of the logic, with the appropriate adaptation of complete monitors (e.g., along the lines of Francalanza et al. (2017b)). $\hfill\qed$

As the following results highlight, soundness and completeness for monitors are invariant under verdict equivalence.

Proposition 4.1**.**

If $m$ is sound and complete for $\varphi$ then

1. (1)

$m\simeq_{\text{ver}}n$* implies $n$ is sound and complete for $\varphi$;* 2. (2)

$m$* is a sound and complete monitor for $\varphi^{\prime}$ implies $\llbracket\varphi\rrbracket_{\textsc{L}}=\llbracket\varphi^{\prime}\rrbracket_{\textsc{L}}$. ∎*

In line with other works on monitorability (Manna and Pnueli, 1991; Chang et al., 1992; Pnueli and Zaks, 2006; Bauer et al., 2010; Falcone et al., 2012a; Cini and Francalanza, 2015; Francalanza et al., 2017b), not all properties in recHML are complete monitorable.

Example 4.1.

The formula $\varphi_{1}=\mathbf{\langle}a\mathbf{\rangle}\mathsf{tt}\,\textsf{U}\,\mathbf{\langle}b\mathbf{\rangle}\mathsf{tt}$ is not complete-monitorable. For if, by contradiction, we assume that it was then there must exist some sound and complete monitor $m$ for $\varphi_{1}$. Since the trace $a^{\omega}\not\in\llbracket\varphi_{1}\rrbracket_{\textsc{L}}$, this monitor $m$ rejects $a^{\omega}$ which, by Def. 3.3, means that it must reach a violation after observing a finite prefix $a^{k}$ (for $k\geq 0$). But this would also mean that $m$ rejects all traces of the form $a^{k}bt$, which clearly satisfy $\varphi_{1}$, thereby contradicting the assumption that $m$ is sound. Similarly, it can be argued that the formula $\varphi_{2}=\mathbf{\langle}a\mathbf{\rangle}\mathbf{\langle}b\mathbf{\rangle}\mathbf{\langle}b\mathbf{\rangle}\mathsf{tt}\,\textsf{R}\,\mathbf{\langle}a\mathbf{\rangle}\mathsf{tt}$ is not complete-monitorable either. For if it was, a sound and complete monitor $m_{2}$ would accept the trace $a^{\omega}$ after analysing some prefix $a^{n}$ of it; this would also mean that this monitor would also accept any trace of the form $a^{n}bat$, which clearly violates the property. Thus, no such monitor exists. $\hfill\qed$

4.1 raises the question as to which recHML properties can be monitored according to Def. 4.2. To answer this question, we first identify a fragment of recHML that is guaranteed to be complete-monitorable and then show its maximality.

Definition 4.3 (The complete-monitorable fragment of recHML).

The recursion-free syntactic fragment of recHML (a syntactic variant of HML (Hennessy and Milner, 1985)) is defined as:

[TABLE]

For every formula $\varphi\in\textsc{HML}$, we can define a monitor synthesis function as follows.

Definition 4.4 (Complete Monitor Synthesis).

The function $\textsf{m}(-):\textsc{HML}\to\textsc{Mon}$ is defined inductively as follows:

[TABLE]

Lemma 4.2**.**

For all $\varphi\in\textsc{HML}$, $\textsf{m}(\varphi)$ is reactive. ∎

Example 4.2.

Assuming $\textsc{Act}=\left\{a,b,c\right\}$, the synthesised monitor for $\varphi=\mathbf{[}a\mathbf{]}\mathbf{\langle}b\mathbf{\rangle}\mathsf{tt}\mathbf{\wedge}\mathbf{\langle}a\mathbf{\rangle}\mathbf{[}c\mathbf{]}\mathsf{ff}$, where $\llbracket\varphi\rrbracket_{\textsc{L}}=\{\,abt\,\mid\,t\in\textsc{Act}^{\omega}\,\}$, is

[TABLE]

When we compose $m$ with $p=\textsf{rec}\,x.a.{b.{x}}$, we observe the following monitored behaviour:

[TABLE]

We show that, for each formula $\varphi\in\textsc{HML}$, the monitor $\textsf{m}(\varphi)$ is the witness sound and complete monitor for it. This, in turn, shows that HML is complete-monitorable, in the sense of Def. 4.2.

Proposition 4.3**.**

For all $\varphi\in\textsc{HML}$, $\textsf{m}(\varphi)$ is a sound and complete monitor for $\varphi$.

Proof.

From Def. 4.1, soundness requires us to show that $(i)$ $\textbf{rej}(\textsf{m}(\varphi),t)$ implies $t\not\in\llbracket\varphi\rrbracket$ and $(ii)$ $\textbf{acc}(\textsf{m}(\varphi),t)$ implies $t\in\llbracket\varphi\rrbracket$. Completeness, requires us to show $(i)$ $t\not\in\llbracket\varphi\rrbracket$ implies $\textbf{rej}(\textsf{m}(\varphi),t)$ and $(ii)$ $t\in\llbracket\varphi\rrbracket$ implies $\textbf{acc}(\textsf{m}(\varphi),t)$. See Sec. B.1. ∎

Corollary 4.4**.**

HML* is complete monitorable. ∎*

Following Francalanza et al. (2017b), we go one step further and show that the fragment HML of Def. 4.3 is maximally expressive with respect to sound and complete monitors. By this we mean that every formula $\varphi\in\textsc{recHML}$ that is complete-monitorable, in the sense of Def. 4.2, is semantically equivalent to a formula from HML. Thus, we can limit ourselves to the syntactic fragment HML without sacrificing any expressiveness in terms of complete-monitorable properties.

We show this claim in two steps. First, we tighten expressiveness results from Sec. 3 for the specific case of complete monitoring. Concretely, we argue that every complete-monitorable formula (Def. 4.2) can be monitored adequately by a recursion-free syntactically deterministic monitor (see Def. 3.8). This is shown via Lem. 4.5, which relies on Def. 4.5. In the second step, we devise an inverse synthesis function to obtain complete-monitorable HML formulae from recursion-free deterministic monitors, Lem. 4.6. This formula synthesis function is then used for Prop. 4.7, the last main result of Sec. 4.1.

Definition 4.5 (Removing Monitor Recursion).

For each monitor $m$, we define $\textsf{noR}(m)$ thus:

[TABLE]

Lemma 4.5**.**

If $m$ is a syntactically deterministic monitor that is sound and complete for $\varphi$, then $\textsf{noR}(m)$ is also a sound and complete monitor for $\varphi$.

Proof.

Using Prop. 4.1, the result follows if we show that $m\simeq_{\text{ver}}\textsf{noR}(m)$. See Sec. B.1. ∎

The next step towards proving Prop. 4.7 is that of synthesising formulae from any recursion-free syntactically deterministic monitor, which can be described by the following grammar.

Definition 4.6 (Recursion-free

Deterministic Monitors).

[TABLE]

We now show how to convert any recursion-free monitor $m$ into an HML formula $\textsf{f}(m)$. We then argue that a reactive $m$ monitors soundly and completely for $\textsf{f}(m)$.

Definition 4.7.

The synthesis function $\textsf{f}(-):\textsc{FMon}\to\textsc{HML}$ is defined as follows:

[TABLE]

Lemma 4.6**.**

Every reactive monitor $m\in\textsc{FMon}$ is a sound and complete monitor for $\textsf{f}(m)$. ∎

We are now in a position to prove the expressive maximality of HML from Def. 4.3.

Proposition 4.7** (Maximality for HML).**

For each $\varphi\in\textsc{recHML}$, if $\varphi$ is complete-monitorable, then there exists some $\psi\in\textsc{HML}$ such that $\llbracket\varphi\rrbracket_{\textsc{L}}=\llbracket\psi\rrbracket_{\textsc{L}}$.

Proof.

From the results in Sec. 3 and Lem. 4.5, each complete-monitorable $\varphi\in\textsc{recHML}$ has a recursion-free deterministic monitor $m$ that is sound and complete for it. By Lem. 4.6, $m$ is sound and complete for $\textsf{f}(m)$ as well which is in HML. Prop. 4.1 thus yields $\llbracket\varphi\rrbracket_{\textsc{L}}=\llbracket\textsf{f}(m)\rrbracket_{\textsc{L}}$ as required. See Sec. B.1 for more details. ∎

The proof of Prop. 4.7 is constructive. We are also able to prove (albeit in a non-constructive manner) an even stronger result (Thm. 4.8) with respect to complete monitoring for any arbitrary logic defined over traces. This increases the importance of the fragment identified in Def. 4.3 for the linear-time interpretation. The proof of Thm. 4.8 can be found in Sec. B.1.

Theorem 4.8**.**

Let $m$ be a monitor from a monitoring system with the following two properties:

1. (1)

verdicts are irrevocable, that is, if $m$ accepts (respectively, rejects) a finite trace $s$, then it accepts (respectively, rejects) all its extensions, and 2. (2)

$m$* accepts (respectively, rejects) a trace $t$ if, and only if, it accepts (respectively, rejects) some finite prefix $s$ of $t$.*

For any property $\varphi$ with a trace interpretation (not necessarily syntactically represented using recHML), if $m$ is sound and complete for $\varphi$ then $\varphi$ can be expressed via the syntactic fragment HML of Def. 4.3. ∎

4.2. Tightly-Complete Monitors

The sound and complete monitoring studied in Sec. 4.1 does not specify when a monitor should reach a verdict while it analyses a trace, as illustrated by the following example.

Example 4.3.

Assume $\textsc{Act}=\left\{a,b\right\}$ and consider the formula $\varphi=\mathbf{\langle}a\mathbf{\rangle}\mathbf{\langle}a\mathbf{\rangle}\mathsf{ff}$, which is equivalent to $\mathsf{ff}$. Following Def. 4.4, the synthesised monitor for $\varphi$ is $m=a.{(a.{\textsf{no}}+b.{\textsf{no}})}+b.{\textsf{no}}$. After at most two consecutive actions, $m$ will definitely reject, and therefore it correctly rejects all traces. However, a more “efficient” correct monitor for $\varphi$ is no, which rejects immediately. $\hfill\qed$

A finite trace for which every extension violates (resp., satisfies) a property $\varphi$ is often called a bad prefix (resp., a good prefix) for $\varphi$ (Alpern and Schneider, 1985; Pnueli and Zaks, 2006; Bauer et al., 2010); good/bad prefixes provide sufficient finite information for acceptance/rejection.

Example 4.4.

$\mathbf{[}A\mathbf{]}\mathsf{tt}$ is equivalent to $\mathsf{tt}$, and thus $\varepsilon$ is a good prefix for it. But $\textsf{m}(\mathbf{[}A\mathbf{]}\mathsf{tt})$ from Def. 4.4 would first need to observe one action before accepting. Similarly, $\mathbf{[}\textsc{Act}\mathbf{]}\mathsf{ff}$ is equivalent to $\mathsf{ff}$ and $\varepsilon$ is a valid bad prefix. Yet the synthesised monitor only rejects after observing one action. $\hfill\qed$

Although the monitors synthesised in Sec. 4.1 are complete, there may be a delay from the moment a good/bad prefix is seen to the point when a verdict is reached. This observation does not affect monitor completeness: the assurance that the stream of events is infinite guarantees that any delay in reporting a verdict will not affect the formula’s monitorability. However, it may be important for a monitor to report a verdict as soon as it gathers sufficient information to do so.

Definition 4.8.

A monitor $m$ is tight when, for every $s\in\textsc{Act}^{*}$, if $m$ rejects (resp., accepts) $st$ for every $t\in\textsc{Trc}$, then $m\xRightarrow{\;s\;}\textsf{no}$ (resp., $m\xRightarrow{\;s\;}\textsf{yes}$). $\hfill\qed$

Although, as 4.3 demonstrates, Def. 4.4 does not always yield tight monitors we can identify a fragment of HML for which it does.

Definition 4.9.

A slim formula is defined by the following grammar:

[TABLE]

where $B,D\neq\emptyset$, $\forall\alpha\in B.\varphi_{\alpha}\neq\mathsf{tt}$, $\forall\alpha\in D.\varphi_{\alpha}\neq\mathsf{ff}$, either $B\neq\textsc{Act}$ or $\exists\alpha\in B.\varphi_{\alpha}\neq\mathsf{ff}$, and either $D\neq\textsc{Act}$ or $\exists\alpha\in D.\varphi_{\alpha}\neq\mathsf{tt}$. $\hfill\qed$

All slim formulae are HML formulae. However, the conditions imposed on their syntax exclude redundancies that yield non-tight monitors. We proceed to show that if $\varphi$ is slim, then $\textsf{m}(\varphi)$ is tight. To this end, we prove a lemma showing the absence of redundancy in slim formulae.

Lemma 4.9**.**

If $\varphi\in\textsc{HML}$ is slim and $\llbracket\varphi\rrbracket_{\textsc{L}}=\emptyset$ (resp., $\llbracket\varphi\rrbracket_{\textsc{L}}=\textsc{Trc}$), then $\varphi=\mathsf{ff}$ (resp., $\varphi=\mathsf{tt}$). ∎

Lemma 4.10**.**

If $\varphi$ is a slim HML formula, then $m(\varphi)$ is tight.

Proof.

By Prop. 4.3, $t{\notin}\llbracket\varphi\rrbracket_{L}$ implies that there is a finite prefix $s$ of $t$ such that $m(\varphi)\xRightarrow{s}\textsf{no}$. We prove by induction on $s$that if $\forall t.~{}\textbf{rej}(m,st)$, then $m\xRightarrow{\;s\;}\textsf{no}$ (the case for acceptance is symmetric). See Sec. B.3 for details. ∎

We can transform every HML formula into an equivalent slim formula. This transformation is based on a set of rewrite rules of the form $\varphi\Rrightarrow_{L}\psi$, given in Fig. 4, that allows us to iteratively replace the formula on the left-hand side with that on the right-hand side.

Lemma 4.11**.**

$\varphi\Rrightarrow_{L}\psi$* implies $\llbracket\varphi\rrbracket_{\textsc{L}}=\llbracket\psi\rrbracket_{\textsc{L}}$ and $l(\varphi)>l(\psi)$ ∎*

Proposition 4.12** (HML normalisation).**

For every formula $\varphi\in\textsc{HML}$, there exists $k\leq l(\varphi)$ such that $\varphi=\varphi_{0}\Rrightarrow_{L}\varphi_{1}\Rrightarrow_{L}\ldots\Rrightarrow_{L}\varphi_{k}=\psi$ where $\psi$ is slim and $\llbracket\varphi\rrbracket_{\textsc{L}}=\llbracket\psi\rrbracket_{\textsc{L}}$. ∎

Example 4.5.

Assume $\textsc{Act}=\left\{a,b\right\}$ and consider the non-slim HML formula $\varphi=\mathbf{\langle}a\mathbf{\rangle}\mathbf{\langle}a\mathbf{\rangle}\mathsf{ff}\mathbf{\wedge}\mathbf{[}b\mathbf{]}\mathsf{ff}$. The synthesised monitor $\textsf{m}(\varphi)=(a.{(a.{\textsf{no}}+b.{\textsf{no}})}+b.{\textsf{no}}){\otimes}(b.{\textsf{no}}+a.{\textsf{no}})$ is not tight. However, we can apply the transformations based on the given equivalences to obtain an equivalent slim formula thus: ${\mathbf{\langle}a\mathbf{\rangle}\mathbf{\langle}a\mathbf{\rangle}\mathsf{ff}}\land{\mathbf{[}b\mathbf{]}\mathsf{ff}}\Rrightarrow_{L}{\mathbf{\langle}a\mathbf{\rangle}\mathbf{\langle}a\mathbf{\rangle}\mathsf{ff}}\Rrightarrow_{L}{\mathbf{\langle}a\mathbf{\rangle}\mathsf{ff}}\Rrightarrow_{L}\mathsf{ff}.$ $\hfill\qed$

4.3. Partially-Complete Monitors

As opposed to the branching-time semantics of recHML, where only properties that are semantically equivalent to $\mathsf{tt}$ and $\mathsf{ff}$ have sound and complete monitors (Francalanza et al., 2017b), the linear-time semantics permits a far richer class of complete-monitorable properties, namely HML. By some measures, however, this monitorable fragment is still quite restrictive. For example, whereas the property “initialise occurs within the first ten actions” can be expressed in terms of HML, the property “initialise eventually occurs”—which can be expressed using least fixpoints—cannot. In fact, although the latter property cannot be monitored for in a complete manner, it can be monitored completely for satisfaction. In this section, we relax the notion of monitorability to partial-completeness, which only requires a monitor to be either violation- or satisfaction-complete.

Definition 4.10.

A formula $\varphi\in\textsc{recHML}$ is monitorable for satisfaction (resp., for violation) iff there exists a monitor $m$ that is a sound and satisfaction-complete (resp., and violation-complete) monitor for $\varphi$. It is partially-monitorable when it is monitorable for satisfaction or for violation. $\hfill\qed$

We can extend these definitions to fragments of recHML in a similar way to that in Def. 4.2. Here, the trade-off between the guarantees we expect from monitors and the monitorable specifications is clear: for the linear-time interpretation, recursion can be traded for partial-completeness, while no such option exists for branching-time. We can extend the observations of Sec. 4.1 to the context of partial monitorability.

Proposition 4.13**.**

If $m$ is sound and satisfaction-complete (resp., violation-complete) for $\varphi$, then

1. (1)

$m\simeq_{\text{ver}}n$* implies $n$ is sound and satisfaction-complete (resp., violation-complete) for $\varphi$.* 2. (2)

If for all $v\in\{\textsf{yes},\textsf{no}\}$, $n\xRightarrow{\;s\;}v$ implies $m\xRightarrow{\;s\;}v$, then $n$ is sound for $\varphi$. 3. (3)

$m\simeq_{\text{acc}}n$* (resp., $m\simeq_{\text{rej}}n$) implies $n$ is satisfaction-complete (resp., violation-complete) for $\varphi$.* 4. (4)

$m$* is sound and satisfaction-complete (resp., violation-complete) for $\varphi^{\prime}$ implies $\llbracket\varphi\rrbracket_{\textsc{L}}=\llbracket\varphi^{\prime}\rrbracket_{\textsc{L}}$. ∎*

Example 4.6.

Let $\textsc{Act}=\{a,b,c\}$ and $\varphi=\max X.(\mathbf{[}b\mathbf{]}\mathsf{ff}\land\mathbf{[}\{a,c\}\mathbf{]}X)\lor\min Y.(\mathbf{\langle}c\mathbf{\rangle}\mathsf{tt}\lor\mathbf{[}\{a,b\}\mathbf{]}Y)$, which is satisfied by traces of the form (a+c)^{\omega}+\bigl{(}(a+b)^{*}c(a+b+c)^{\omega}\bigr{)}, i.e., traces where either $b$ does not appear, or $c$ does appear. We show that $\varphi$ is not partially-monitorable. For if there was some $m$ that is sound and satisfaction-complete for $\varphi$, it should accept $a^{\omega}$; this means that $m$ must reach yes after analysing $a^{k}$ for some $k\geq 0$. In this case, the trace $a^{k}b^{\omega}$, which does not satisfy $\varphi$, must also be accepted by $m$, resulting in a contradiction. If, on the other hand, there was some $m$ that is sound and violation-complete for $\varphi$, then it should reject $b^{\omega}$. Again, $m$ must reach no after $b^{k}$ for some $k\geq 0$, but $b^{k}c^{\omega}$ satisfies $\varphi$. Therefore, $\varphi$ cannot be partially monitorable. $\hfill\qed$

For partial monitorability, we can identify two fragments of recHML, namely minHML, which is monitorable for satisfaction, and maxHML, which is monitorable for violation.

Definition 4.11 (MAX and MIN Fragments of recHML).

The greatest-fixed-point and least-fixed point fragments of recHML are, respectively, defined as:

[TABLE]

Both maxHML and minHML are extensions of HML. We can extend the monitor synthesis from Def. 4.4 to these fragments by using the recursion that is available for monitors.

Definition 4.12 (Monitor Synthesis).

The monitor synthesis for maxHML and minHML results by simply extending the definition of $\textsf{m}(-)$ from Def. 4.4 with the cases for the respective fixed-point of each fragment: $\textsf{m}(\mathsf{max}\,X.\varphi)=\textsf{m}(\mathsf{min}\,X.\varphi)=\textsf{rec}\,x.\textsf{m}(\varphi)$ and $\textsf{m}(X)=x$. $\hfill\qed$

We observe that the extended monitor synthesis function still produces reactive monitors. We also show the first important result of this subsection, namely that Def. 4.12 yields the required witness monitors to prove that the syntactic fragment $\textsc{maxHML}\cup\textsc{minHML}$ is partially-monitorable.

Proposition 4.14**.**

For every $\varphi\in\textsc{maxHML}\cup\textsc{minHML}$, $\textsf{m}(\varphi)$ is reactive. ∎

Proposition 4.15**.**

For every $\varphi\in\textsc{maxHML}$, $\textsf{m}(\varphi)$ is a sound and violation-complete monitor for $\varphi$. For every $\varphi\in\textsc{minHML}$, $\textsf{m}(\varphi)$ is a sound and satisfaction-complete monitor for $\varphi$.

Proof.

This requires us to prove soundness and violation/satisfaction-completeness for every $\varphi\in\textsc{maxHML}$ and $\varphi\in\textsc{minHML}$ resp., as stated in Def. 4.1. See Sec. B.4. ∎

As in the case of Sec. 4.1, we now turn our attention to the maximality of the syntactic fragment $\textsc{maxHML}\cup\textsc{minHML}$ for partial-monitorability. Particularly, we can define two formula synthesis functions that produce partially monitorable formulae from monitors: one maps monitors to formulae in maxHML, and the other one to formulae in minHML. Depending on the fragment, we then show that if $m$ is mapped to $\varphi$, then $m$ is sound and violation-complete, or satisfaction-complete resp., for $\varphi$. Here we only present the synthesis function for maxHML; the case for minHML is dual.

Definition 4.13 (maxHML Formula Synthesis).

[TABLE]

Example 4.7.

Let $m=a.{b.{\textsf{no}}}+a.{a.{\textsf{yes}}}$. Then, $\textsf{f}(m)=\mathbf{[}a\mathbf{]}\mathbf{[}b\mathbf{]}\mathsf{ff}\mathbf{\wedge}\mathbf{[}a\mathbf{]}\mathbf{[}a\mathbf{]}\mathsf{tt}$ (which is equivalent to just $\mathbf{[}a\mathbf{]}\mathbf{[}b\mathbf{]}\mathsf{ff}$). The monitor $m$ rejects traces of the form $abt$ which are exactly all the traces violating $\textsf{f}(m)$. Thus $m$ is sound and violation-complete for $\textsf{f}(m)$. $\hfill\qed$

Note that $\textsf{f}(m)\in\textsc{maxHML}$, for any $m$. However, when we apply the formula synthesis function from Def. 4.13 to a consistent monitor $m$ to generate a formula $\varphi$, and then apply the monitor synthesis from Def. 4.12 to $\varphi$, we will generate a monitor that has similar parts to $m$, but it will be somewhat different due to the asymmetry of the resp., syntheses. For example, for $\textsc{Act}=\left\{a,b\right\}$, $\textsf{f}(a.{\textsf{no}}+b.{\textsf{yes}})=\mathbf{[}a\mathbf{]}\mathsf{ff}\mathbf{\wedge}\mathbf{[}b\mathbf{]}\mathsf{tt}$, and $\textsf{m}(\mathbf{[}a\mathbf{]}\mathsf{ff}\mathbf{\wedge}\mathbf{[}b\mathbf{]}\mathsf{tt})=(a.{\textsf{no}}+b.{\textsf{yes}}){\otimes}(b.{\textsf{yes}}+a.{\textsf{yes}})$. The following lemma allows us to abstract from these discrepancies, thereby enabling the proof of Prop. 4.17.

Lemma 4.16**.**

$\textsf{m}(\textsf{f}(m))$* rejects the same traces as $m$. ∎*

Proposition 4.17**.**

If $m$ is consistent, then $m$ is a sound and violation-complete monitor for $\textsf{f}(m)$.

Proof.

From Lem. 4.16, $\textsf{m}(\textsf{f}(m))$ rejects the same traces as $m$, and therefore, by Props. 4.13 and 4.15, $m$ is violation-complete for $\textsf{f}(m)$. Since $m$ rejects the same traces as $\textsf{m}(\textsf{f}(m))$, if $m$ rejects a trace $t$, then $t\notin\llbracket\varphi\rrbracket_{\textsc{L}}$. Since $m$ is consistent, if $m$ accepts a trace $t$, then it does not reject $t$, and because $m$ rejects the same traces as $\textsf{m}(\textsf{f}(m))$, $\textsf{m}(\textsf{f}(m))$ does not reject $t$ either. Since $\textsf{m}(\textsf{f}(m))$ is also violation-complete by Prop. 4.15, this yields that $t\in\llbracket\varphi\rrbracket_{\textsc{L}}$. Therefore, $m$ is also sound for $\varphi$. ∎

The following proposition tells us that, up to logical equivalence, maxHML is the largest fragment of recHML that is monitorable for violation. Dually, minHML is the largest fragment of recHML that is monitorable for satisfaction.

Proposition 4.18**.**

If a formula $\varphi\in\textsc{recHML}$ has a sound and violation-complete monitor over infinite traces, then it is equivalent to a formula $\psi\in\textsc{maxHML}$ over infinite traces.

Proof.

Let $m$ be a sound and violation-complete monitor for $\varphi$ and let $\psi=\textsf{f}(m)\in\textsc{maxHML}$ be the witness formula. Since $m$ is sound for $\varphi$, it must be consistent, and by Prop. 4.17, $m$ is a sound and violation-complete monitor for $\textsf{f}(m)$. Therefore, by Prop. 4.13, $\llbracket\varphi\rrbracket_{\textsc{L}}=\llbracket\textsf{f}(m)\rrbracket_{\textsc{L}}$. ∎

Remark*.*

Thm. 4.8 demonstrates that HML can express any property of infinite traces that has a complete monitor in any monitoring system, assuming that verdicts remain irrevocable. Unfortunately, this result cannot be replicated for partial completeness. For instance, let $L\subseteq(\textsc{Act}\setminus\{c\})^{*}$ be a non-regular language, where $c\in\textsc{Act}$ is some distinguished action, and $L_{c}=\{\,sct\,\mid\,s\in L\text{ and }t\in\textsc{Act}^{\omega}\,\}$. If $L_{c}$ could be expressed in minHML, then there would be a sound and satisfaction-complete monitor for $L_{c}$, and by a straightforward use of Prop. 3.6, we could construct a finite automaton that recognizes $L$, which contradicts the assumption that $L$ is non-regular. Yet, we could imagine appropriate choices for $L$ and monitoring systems in which $L_{c}$ is monitorable. For instance, suppose that monitors are described using pushdown automata and let $L$ contain exactly the finite words on $\{0,1\}$ that have the same number of occurrences of [math] and of $1$. $\hfill\qed$

4.4. Tightly-Complete Monitors for Recursion

To synthesise a tight monitor for a formula $\varphi$ of maxHML (or minHML), one can synthesise a parallel monitor $m(\varphi)$, then, using the methods of Subsection 3.3, turn $m(\varphi)$ into a verdict-equivalent deterministic regular monitor, and, finally, consecutively replace instances of $\sum_{\alpha\in\textsc{Act}}\alpha.\textsf{no}$ and $\textsf{rec}\,x.\textsf{no}$ by no and instances of $\sum_{\alpha\in\textsc{Act}}\alpha.\textsf{yes}$ and $\textsf{rec}\,x.\textsf{yes}$ by yes. The resulting monitor is tight.

Lemma 4.19**.**

Let $m$ be a deterministic regular monitor, where $\sum_{\alpha\in\textsc{Act}}\alpha.\textsf{no}$, $\textsf{rec}\,x.\textsf{no}$, $\sum_{\alpha\in\textsc{Act}}\alpha.\textsf{yes}$, and $\textsf{rec}\,x.\textsf{yes}$ do not occur as submonitors. Then, $m$ is tight. ∎

We would like to be able to apply a convenient method to process the formula or the monitor, so that right after the monitor synthesis we could produce a tight monitor. However, as we will see, a more reasonable monitor synthesis function that produces tight monitors is unlikely, as one could use it to solve the satisfiability problem for maxHML— by checking whether a produced monitor for the formula immediately evaluates to no (or to yes, for its negation), — which is PSPACE-complete.

Proposition 4.20**.**

For $|\textsc{Act}|\geq 2$, the satisfiability problem for maxHML is PSPACE-complete.

Proof.

Satisfiability for recHML (and therefore for maxHML as well) is known to be in PSPACE (Vardi, 1988). That satisfiability for maxHML is PSPACE-hard results from the observation that maxHML with at least two actions can encode the $1$-variable, diamond-free fragment of $D\oplus_{\subseteq}D4$, which is PSPACE-complete (Achilleos, 2016). The reduction can be found in Appendix B.2. ∎

Remark*.*

For singleton $\textsc{Act}=\left\{a\right\}$, recHML-satisfiability is a lot simpler, as there is only one trace, $a^{\omega}$. Therefore, satisfiability for maxHML can be reduced to model-checking on $a^{\omega}$. A more direct way to solve satisfiability is to reduce the given formula by using the following straightforward rewrite rules: $\mathsf{ff}\land\varphi\Rrightarrow_{L}\mathsf{ff}$, $\mathsf{ff}\lor\varphi\Rrightarrow_{L}\varphi$, $\mathbf{\langle}\alpha\mathbf{\rangle}\mathsf{ff}\Rrightarrow_{L}\mathsf{ff}$, $\mathbf{[}\alpha\mathbf{]}\mathsf{ff}\Rrightarrow_{L}\mathsf{ff}$, and $\max X.\mathsf{ff}\Rrightarrow_{L}\mathsf{ff}$; the cases for $\mathsf{tt}$ are symmetric. After applying these formula simplifications, we will either reach one of $\mathsf{tt},\mathsf{ff}$, in which case the answer to satisfiability is obvious, or we will reach a formula $\varphi$ without these constants. In the latter case, we can easily see that $\textsf{m}(\varphi)$ can never reach a verdict, and therefore it will never reject a trace, which, from Prop. 4.15, implies that $\llbracket\varphi\rrbracket_{\textsc{L}}=\textsc{Trc}=\{\alpha^{\omega}\}$. $\hfill\qed$

5. Branching-Time Monitorability

Monitorability over branching-time semantics has been examined in Aceto et al. (2017a, 2018a) and Francalanza et al. (2017b) for various frameworks. In this section we compare the results of Francalanza et al. (2017b), the closest to our setting, with those of Sec. 4. We begin by revisiting the basic definitions and results for branching-time monitorability. Then, in Sec. 5.1 and Sec. 5.2, we extend the study of monitorability to a domain that allows both finite and infinite traces, and conclude, in Sec. 5.3, by comparing the monitorable fragments in this domain to those in the branching-time setting. All omitted proofs are in Appendix C.

Definition 5.1 (Branching-time Monitor Soundness and Completeness).

• •

A monitor $m$ is sound for a (closed) formula $\varphi$ over processes if, for all $p\in\textsc{Prc}$ of every LTS, i.e., a triple $\langle\textsc{Prc},(\textsc{Act}\cup\left\{\tau\right\}),\longrightarrow\rangle$:

• –

$\textbf{rej}(m,p)$ implies $p\not\in\llbracket\varphi\rrbracket_{\textsc{B}}$;

• –

$\textbf{acc}(m,p)$ implies $p\in\llbracket\varphi\rrbracket_{\textsc{B}}$.

• •

A monitor $m$ is violation-complete for a formula $\varphi$ over processes if for all $p\in\textsc{Prc}$ of every LTS, $p\notin\llbracket\varphi\rrbracket_{\textsc{B}}$ implies $\textbf{rej}(m,p)$. It is satisfaction-complete if $p\in\llbracket\varphi\rrbracket_{\textsc{B}}$ implies $\textbf{acc}(m,p)$. $\hfill\qed$

Remark*.*

The LTS is often omitted when it is clear from the context. As before, a monitor $m$ is complete for $\varphi$ if it is violation- and satisfaction-complete for it. A rejection monitor is a monitor without the verdict yes; an acceptance monitor is one without the verdict no. $\hfill\qed$

In the branching-time setting, monitors with both yes and no verdicts are unsound for any formula, as whenever one trace leads to an acceptance and another to a rejection, one can easily construct a process that can emit both traces. As a single-verdict (uni-verdict (Francalanza et al., 2017b)) monitor can only be either satisfaction- or violation-complete for a formula (except monitors for $\mathsf{tt}$ and $\mathsf{ff}$ which can be both), one cannot hope for complete monitors for recHML, and therefore the best one can do is to identify its fragments for which partially complete monitors exist. These are sHML and cHML, defined by the following grammars:

Definition 5.2 (Safety and Cosafety Fragments for Branching-time recHML).

[TABLE]

Theorem 5.1** (Branching-time Monitorability (Francalanza et al., 2017b)).**

For every $\varphi\in\textsc{sHML}$, there is a regular rejection monitor $m$ that is sound and violation-complete for $\varphi$. For every $\varphi\in\textsc{cHML}$, there is a regular acceptance monitor $m$ that is sound and satisfaction-complete for $\varphi$. ∎

Theorem 5.2** (Maximality of sHML and cHML (Francalanza et al., 2017b)).**

For every regular rejection monitor $m$, there is a formula $\varphi\in\textsc{sHML}$, such that $m$ is sound and violation-complete for $\varphi$. For every regular acceptance monitor $m$, there is a formula $\varphi\in\textsc{cHML}$, such that $m$ is sound and satisfaction-complete for $\varphi$. ∎

One can identify two key differences between the linear-time and the branching-time semantics introduced in Sec. 2. The first and most characteristic difference is that for branching-time semantics, where formulae are interpreted over processes, a process is allowed to emit more than one trace. In other words, a process may exhibit different behaviour each time it runs, and therefore, a trace does not give the whole picture of its possible executions. By contrast, for linear-time semantics, if one observes an action or a finite trace, then there is no possibility that another one could have been exhibited instead. This allows for constructs such as parallel monitors to monitor for conjunctions and disjunctions at the same time: simply decompose the formula as the monitor synthesis function directs in Defs. 4.4 and 4.12, and let each monitor component examine the trace until a conclusion is reached. For branching-time semantics, this method does not help to monitor a conjunction for satisfaction or a disjunction for rejection, as Francalanza et al. (2017b) demonstrates.

Example 5.1.

Consider $\varphi=\mathbf{[}a\mathbf{]}\mathsf{ff}\lor\mathbf{[}b\mathbf{]}\mathsf{ff}\notin\textsc{sHML}$. In contrast to the linear-time setting, $\varphi$ is not monitorable for violation under a branching-time interpretation. For assume, towards a contradiction, that there is a rejection monitor for $\varphi$. Assume an LTS with a process $p$ that has two transitions, $p\xrightarrow{\;a\;}\textsf{nil}$ and $p\xrightarrow{\;b\;}\textsf{nil}$. Then, $p\notin\llbracket\varphi\rrbracket_{\textsc{B}}$ and $p$ can produce three possible traces: $\varepsilon,a,b$. If a monitor rejected one of these, say $a$, then it would reject $p$, but also process $q_{a}$ that has exactly one transition, $q_{a}\xrightarrow{\;a\;}\textsf{nil}$. But we observe that $q_{a}\in\llbracket\varphi\rrbracket_{\textsc{B}}$, meaning that the monitor would not be sound for $\varphi$. The formula $\mathbf{[}a\mathbf{]}\mathsf{ff}\mathbf{\vee}\mathbf{[}b\mathbf{]}\mathsf{ff}$ is however monitorable in a linear-time setting (Defs. 4.3 and 4.11). $\hfill\qed$

The second difference is that, in the linear-time semantics, formulae are only interpreted over infinite traces while, in branching-time semantics, a trace is allowed to end. Unlike the first difference, this one is not inherent to the linear- versus branching-time distinction, but it is one we have lifted from standard LTL-style semantics (Vardi, 1988; Bradfield and Stirling, 2001). Therefore, as a first step to reconcile the two semantics, we focus on this less essential difference for our logic.

5.1. The Finfinite Domain

We introduce an alternative linear-time semantics for our logic, where formulae are interpreted over traces that are allowed to be either finite or infinite. For convenience, we call these kinds of traces finfinite and the resulting semantics finfinite linear-time semantics, or just finfinite semantics. (A semantics akin to ours for a linear-time temporal logic may be found in, for instance, Schneider (1997). Falcone et al. (2012b) define linear-time properties over finite and infinite traces, but do not consider a specific logic.) The finfinite semantics, $\llbracket-\rrbracket_{\textsc{F}}$, is presented in Fig. 5. The set of finfinite traces is $\textsc{fTrc}=\textsc{Trc}\cup\textsc{Act}^{*}$ and we use $g,h\in\textsc{fTrc}$ (resp., $\textsl{F}\subseteq\textsc{fTrc}$) to range over (resp., sets of) finfinite traces.

Remark*.*

For recHML, $\mathbf{\langle}\textsc{Act}\mathbf{\rangle}\varphi$ and $\mathbf{[}\textsc{Act}\mathbf{]}\varphi$ can be seen as the strong and weak next operators, $X\varphi$ and $\overline{X}\varphi$ from LTL (Clarke et al., 1999). In this same setting, $\mathbf{[}A\mathbf{]}\varphi$ may be seen as shorthand for $\mathbf{\langle}\overline{A}\mathbf{\rangle}\mathsf{tt}\mathbf{\vee}\mathbf{\langle}A\mathbf{\rangle}\varphi$. However the encoding does not work for the finfinite interpretation of Fig. 5. $\hfill\qed$

The two linear-time semantics for recHML still correspond in some sense; see Lem. 5.3. In particular, formula equivalence over finfinite traces implies equivalence over infinite traces.

Lemma 5.3**.**

For all $\varphi\in\textsc{recHML}$, $\llbracket\varphi\rrbracket_{\textsc{F}}\cap\textsc{Trc}=\llbracket\varphi\rrbracket_{\textsc{L}}$. ∎

We consider the same monitoring systems of regular and parallel monitors that were introduced in Sec. 3. However, what it means for $m$ to monitor for $\varphi$ depends on the semantics that we use for the formulae: the definition used in Sec. 4 is therefore not sufficient for the finfinite domain.

Definition 5.3 (Finfinite Linear-time Monitor Soundness and Completeness).

• •

A monitor $m$ is sound for a (closed) formula $\varphi$ over finfinite traces if, for all $g\in\textsc{fTrc}$:

• –

$\textbf{rej}(m,g)$ implies $g\not\in\llbracket\varphi\rrbracket_{\textsc{F}}$;

• –

$\textbf{acc}(m,g)$ implies $g\in\llbracket\varphi\rrbracket_{\textsc{F}}$.

• •

A monitor $m$ is violation-complete for a formula $\varphi$ over finfinite traces if for all $g\in\textsc{fTrc}$, $g\not\in\llbracket\varphi\rrbracket_{\textsc{F}}$ implies $\textbf{rej}(m,g)$. It is satisfaction-complete if $g\in\llbracket\varphi\rrbracket_{\textsc{F}}$ implies $\textbf{acc}(m,g)$. It is complete for a formula $\varphi$ over finfinite traces if it is both violation- and satisfaction complete for it. $\hfill\qed$

Monitorability of formulae and logics can be adjusted to finfinite traces analogously.

5.2. Monitorability over Finfinite Traces

We now identify the complete- and partial-monitorable fragments of recHML over finfinite traces. Our first observation is that under finfinite semantics, there are no complete-monitorable formulae, except the ones equivalent to $\mathsf{tt}$ or $\mathsf{ff}$.

Lemma 5.4**.**

If $m$ is sound and complete for $\varphi$ over finfinite traces, then $\llbracket\varphi\rrbracket_{\textsc{F}}=\textsc{fTrc}$ or $\llbracket\varphi\rrbracket_{\textsc{F}}=\emptyset$. ∎

Remark*.*

Lem. 5.4 holds regardless of the considered logic: due to verdict-persistence (Lem. 3.1), a logical fragment that is complete-monitorable over finfinite traces must be trivial for any logic interpreted over finfinite traces. $\hfill\qed$

The concept of tightness, as defined in Def. 4.8, does not apply for the finfinite interpretation since there is no guarantee that a finfinite trace will have a continuation. A definition of tightness might stipulate that a rejection-monitor is tight for a formula when it is guaranteed to reject any finite trace as long as the trace and all of its (finfinite) continuations violate the formula (i.e., bad prefixes). However, this notion of tightness is implied by partial completeness.

Example 5.2.

In contrast to the infinite trace semantics, $\mathbf{\langle}a\mathbf{\rangle}\mathsf{tt}$ is not monitorable for violation under finfinite semantics. For assume towards a contradiction that $m$ is a monitor that is sound and violation-complete for $\mathbf{\langle}a\mathbf{\rangle}\mathsf{tt}$. Then, $m$ must reject the empty trace, $\varepsilon$, and thus all of its extensions, including $a\in\llbracket\mathbf{\langle}a\mathbf{\rangle}\mathsf{tt}\rrbracket_{\textsc{F}}$, making $m$ unsound. Similarly, $[\alpha]\mathsf{ff}$ is not monitorable for satisfaction. $\hfill\qed$

Our next goal is to characterize the expressive power of monitors in finfinite semantics. To this end, we identify the following fragments of recHML. Only one type of modality is kept in each of these fragments. This is because, as observed in 5.2, the two modalities are not mutually expressive and even simple formulae using them are not monitorable for violation or satisfaction.

Definition 5.4.

[TABLE]

The next lemma formalises the property that formulae in unHML denote prefix-closed sets of (finfinite) traces whereas formulae in exHML denote suffix-closed sets of traces.

Lemma 5.5**.**

For all $s\in\textsc{Act}^{*}$ and $g\in\textsc{fTrc}$, $(i)$ if $\varphi\in\textsc{unHML}$ and $sg\in\llbracket\varphi\rrbracket_{\textsc{F}}$, then $s\in\llbracket\varphi\rrbracket_{\textsc{F}}$; $(ii)$ if $\varphi\in\textsc{exHML}$ and $s\in\llbracket\varphi\rrbracket_{\textsc{F}}$, then $sg\in\llbracket\varphi\rrbracket_{\textsc{F}}$. ∎

Interestingly, for unHML and exHML over finfinite traces, we can use the same monitor synthesis function that we used to generate monitors for maxHML and minHML over infinite traces.

Proposition 5.6**.**

For every $\varphi\in\textsc{unHML}$, $\textsf{m}(\varphi)$ is sound and violation-complete for $\varphi$ over finfinite traces. For every $\varphi\in\textsc{exHML}$, $\textsf{m}(\varphi)$ is sound and satisfaction-complete for $\varphi$ over finfinite traces. ∎

To facilitate our comparisons between the finfinite and the branching-time interpretations of recHML, we define the notion of trace-processes.

Definition 5.5.

Process $p$ is a trace-process when $p\xrightarrow{\;\mu\;}q$ and $p\xrightarrow{\;\mu^{\prime}\;}q^{\prime}$ implies $\mu=\mu^{\prime}$, $q=q^{\prime}$ and $q$ is a trace-process. A (trace) process $p$ represents a finfinite $g$ when $p\xRightarrow{\;s\;}$ iff $s$ is a prefix of $g$. $\hfill\qed$

For a trace $g$, we can assume the existence of a trace-process $p_{g}$ that represents $g$: one can construct such a trace-process $p_{g}$ whereby its states are all the prefixes of $g$ and its transitions are those of the form $s\xrightarrow{\;\alpha\;}s\alpha$, where $s$ and $s\alpha$ are prefixes of $g$.

Remark*.*

We note that, unlike for monitors, we have not assumed any specific syntax for processes, which can come from an arbitrary LTS. This makes it possible to represent every finfinite trace, even one without a finite representation, by a process. $\hfill\qed$

Example 5.3.

A process representing $ab$ is the three-state process $p$, with just the transitions $p\xrightarrow{\;a\;}p^{\prime}$ and $p^{\prime}\xrightarrow{\;b\;}\textsf{nil}$. A process representing $a^{\omega}$ is $q$ that has exactly one transition, $q\xrightarrow{\;a\;}q$. $\hfill\qed$

Lem. 5.7 shows that, for recHML, (finfinite) traces and trace-processes are different descriptions of the same model.

Lemma 5.7**.**

If $p$ represents $g$, then $g\in\llbracket\varphi\rrbracket_{\textsc{F}}$ iff $p\in\llbracket\varphi\rrbracket_{\textsc{B}}$. ∎

Coincidentally, all formulae that are monitorable for violation or satisfaction over a finfinite semantics are equivalent to sHML or cHML formulae resp., from Def. 5.2. Since unHML and exHML syntactically subsume sHML and cHML resp., they are maximally monitorable fragments of recHML when interpreted over finfinite traces.

Proposition 5.8**.**

If $\varphi\in\textsc{recHML}$ has a sound and violation-complete (resp., satisfaction-complete) reactive parallel monitor over finfinite traces, then there is some $\psi\in\textsc{sHML}$ (resp., $\psi\in\textsc{cHML}$) that is equivalent to $\varphi$ over finfinite traces.

Proof.

Let $m$ be a sound and violation-complete reactive parallel monitor for $\varphi$ over finfinite traces. By Prop. 3.8, there is a regular monitor $n$ that is verdict-equivalent to $m$, so it is also sound and violation-complete for $\varphi$ over finfinite traces. We can then obtain a single-verdict monitor $n^{\prime}$ from $n$ that is rejection equivalent to it by swapping any yes with end. $n^{\prime}$ is thus still sound and violation-complete for $\varphi$ over finfinite traces. From Thm. 5.2 there is a formula $\psi\in\textsc{sHML}$, such that $n$ is sound and violation-complete for $\psi$ over all LTSs, including the LTS of trace-processes. Since $n$ is sound and violation-complete for $\psi$ on trace processes, $p_{g}\in\llbracket\psi\rrbracket_{\textsc{B}}$ is equivalent to claiming that $n$ does not reject any trace that $p_{g}$ can produce. However, this is equivalent to saying that $n$ does not reject $g$ which, by violation-completeness, is equivalent to $g\in\llbracket\varphi\rrbracket_{\textsc{F}}$. By Lem. 5.7, $g\in\llbracket\psi\rrbracket_{\textsc{F}}$ iff $p_{g}\in\llbracket\psi\rrbracket_{\textsc{B}}$, and the proof is complete. The case for a satisfaction-complete monitor is similar. ∎

5.3. Monitorable Formulae Across Semantics

So far, we have identified a different pair of partial-monitorable syntactic fragments for each of the three semantics that we have presented in this paper. However, as the reader may suspect from Prop. 5.8, we may be able to further restrict the syntax that we allow for our formulae, and still be able to express all monitorable formulae, and therefore, an identified maximally monitorable fragment of recHML may be equally expressive as a syntactic fragment of its own.

Here we show that for each of the semantics that we have presented, i.e., over infinite traces, finfinite traces, and processes, sHML and cHML are equally expressive as the corresponding identified partially monitorable fragment. That is to say, sHML is as expressive as unHML over finfinite traces and as expressive as maxHML over infinite traces — and dually, cHML is as expressive as exHML over finfinite traces and as expressive as minHML over infinite traces.

Proposition 5.9**.**

If $\varphi\in\textsc{unHML}$ (resp., $\varphi\in\textsc{exHML}$), then there is some $\psi\in\textsc{sHML}$ (resp., $\psi\in\textsc{cHML}$) that is equivalent to $\varphi$ over finfinite traces. ∎

Proposition 5.10**.**

If $\varphi\in\textsc{maxHML}$ (resp., $\varphi\in\textsc{minHML}$), then there is some $\psi\in\textsc{sHML}$ (resp., $\psi\in\textsc{cHML}$) that is equivalent to $\varphi$ over infinite traces. ∎

The proofs of both of these propositions proceed by considering a sound and partially complete monitor for a formula in unHML, maxHML or their duals, and using the formula synthesis to find an sHML formula that is equivalent to the original formula on finfinite and infinite traces respectively. The full proofs can be found in Appendix C.

The import of Props. 5.9 and 5.10 is that, in settings where Act is finite, logical fragment $\textsc{sHML}\cup\textsc{cHML}$ can be used to syntactically characterise the class of monitorable properties (for sound and partial-completeness) for all three interpretations (i.e., traces, finfinite traces and processes). In spite of this felicitous (and somewhat surprising) result, one should nevertheless stress that their interpretation is still semantically different. In fact, the synthesised monitors presented here in Defs. 4.4 and 4.12 yield behaviourally different monitors to those obtained by the synthesis in Francalanza et al. (2017b). Moreover, they can not be used interchangeably: Defs. 4.4 and 4.12 produce multi-verdict monitors, even when applied to the syntactic fragment $\textsc{sHML}\cup\textsc{cHML}$, which makes them immediately unsound for a branching-time interpretation. In Prop. 5.11, we can however show that the monitors synthesised by the procedure of Francalanza et al. (2017b) for the sHML fragment qualify also as correct monitors for the finfinite interpretation of the logic. This means that the tools developed in Attard et al. (2017) and Attard and Francalanza (2016), which are based on the branching-time synthesis of Francalanza et al. (2017b), can be used out of the box to monitor for finfinite properties.

Proposition 5.11**.**

For a process $p$ and a formula $\varphi\in\textsc{sHML}$, the following are equivalent: $(i)$ $p\in\llbracket\varphi\rrbracket_{\textsc{B}}$ and $(ii)$ If $p$ produces a finfinite trace $g$, then $g\in\llbracket\varphi\rrbracket_{\textsc{F}}$ . ∎

6. Conclusion

We have presented a systematic study of the monitorability of recHML, a highly expressive specification logic: we have developed results relating to its linear-time interpretation and established correspondences with previous monitorability results for the branching-time interpretation of the logic. This allows us to use existing RV tools (developed for branching-time) to monitor linear-time recHML properties. To our knowledge, this is the first study of monitorability that spans across the linear-time/branching-time spectrum. Moreover, although monitorability has been studied extensively for linear-time specifications, we are unaware of any maximality results such as those presented in Props. 4.7, 4.8, 4.18, 5.8, 5.9 and 5.10.

Concretely, in Sec. 3, we introduce parallel monitors and we gave a way to construct a deterministic regular monitor (introduced in Aceto et al. (2017b) and Francalanza et al. (2017b)) from a parallel one, establishing that the two monitoring frameworks are equivalent with respect to the properties they can monitor. In Sec. 4, we give a natural monitor synthesis from three fragments of recHML to parallel monitors, and establish that the resulting monitors satisfy the requirement of soundness and a version of the requirement for completeness. For complete monitors, we identify the requirement of tightness and show how one can satisfy it. In Sec. 5, we see how these findings apply in the intermediate finfinite setting, and we establish that sHML has the same expressive power as the respective maximal monitorable fragments of recHML in the finfinite and infinite-trace settings.

Multiple Ways to Monitor

These results show that there is more than one way to monitor for a property $\varphi$ that is monitorable for violation. If $\varphi$ is already in sHML, or if we want to make the effort to write the property as an sHML formula, we can use the monitor synthesis in Francalanza et al. (2017b) to synthesise a single-verdict, sound and violation-complete regular monitor for $\varphi$ that will work in all (infinite-trace, finfinite, and branching-time) semantics. Alternatively, if we are interested in the linear-time domain (for either infinite or finfinite traces), we can synthesise a parallel monitor with the synthesis function from Def. 4.12, hoping that the possibly dual-verdict monitor may occasionally report the satisfaction of the formula, providing us with more information. In the latter case, we may choose to deploy the parallel monitor as is, or use the construction from Prop. 3.8 to obtain a verdict-equivalent regular monitor. An advantage of using the parallel monitor is that it can be significantly more concise than a regular monitor, at least at the early stages of the computation. An advantage of using a regular monitor is that it is guaranteed to be finite state (Prop. 3.2). Furthermore, regular monitors can be determinized and then minimized (see Prop. 3.11 and Aceto et al. (2016)), making their implementation more straightforward. Therefore, one can think of maxHML as a high-level specification language for properties that are monitorable for violation in the linear-time setting. From maxHML, we can generate parallel monitors that can then be compiled into (deterministic, minimized) regular monitors that can be implemented and deployed to monitor the system. On the other hand, sHML can be thought of as a lower-level language that is closer to regular monitors and can allow for better fine-tuning of the monitor’s behaviour, and avoids the cost of constructing a regular monitor.

Future Work

We are interested in a detailed taxonomy and comparison of different notions of monitorability, and this work is a first step in that direction. Additionally, in Aceto et al. (2018a), the authors examine how the set of monitorable properties can be extended by encoding additional information into the trace that describes a system execution. Noticeably, their framework allows for the interaction of multiple verification methods, and this is an approach we would like to explore for our own framework.

Related Work on Runtime Verification

RV has been applied in the computer-aided verification of complex programs and models written in a variety of high-level languages. For example, RV has been used in the verification of properties written in an extension of PSL and SVA over SystemC models in Tabakov et al. (2012) (but see Pnueli and Zaks (2006) and references in Tabakov et al. (2012) for earlier work on monitor synthesis for PSL). Like we do in this paper, Tabakov et al. argue for the algorithmic generation of “correct” monitors from properties. However, their focus is on an experimental study of monitor-generation procedures that offer the best performance in terms of runtime overhead at simulation time. In order to do so, they employ the CHIMP tool (Dutta et al., 2014) to generate monitors (represented as DFAs) from LTL properties using a number of workflows that take into account various options regarding state minimization, alphabet representation, alphabet minimization and the representation of the transition function of the monitor.

Diagnosability

It is worth mentioning here work on diagnosability, e.g., Sampath et al. (1995); Bertrand et al. (2014). Diagnosability is a similar notion to the one of monitorability. What is different is that, for diagnosability one knows a model of the system, and then, by observing the visible events of a system run, infers whether an unobservable fault event has occurred during this run. A further goal is to diagnose the kind of fault event that has occurred. Typically, the detection and diagnosis of fault events is performed by a diagnoser, which is synthesised from the model of the system. Although RV and diagnosability appear, at first glance, to work in different ways, one can view diagnosability as the runtime monitoring of a set of trace-properties (the occurrence of different types of fault events), using information about the system’s branching structure, in a framework that considers unobservable events — as in Francalanza et al. (2017b); Aceto et al. (2017a). We feel that there is significant potential in addressing the two areas in a more unified manner. This is an interesting avenue for future research.

Related Work on Specification logics

recHML is a multi-modal variant of the $\mu$-calculus that is interpreted over edge-labelled LTSs rather than node-labelled ones. The distinction is mainly a question of presentation; how to go between the two types of models is discussed by De Nicola and Vaandrager (1990). The $\mu$-calculus itself is a logic which subsumes CTL, CTL*, LTL, as well as more exotic variations thereof. Its links to automata theory are well established (Wilke, 2001) and can be used in the implementation of verification tools. This makes the $\mu$-calculus well suited for foundational research on verification, even though logics with more intuitive syntax may appeal to practitioners. recHML over traces is similar to the linear-time $\mu$-calculus. The main difference is that in the linear-time $\mu$-calculus, which is usually interpreted over infinite traces, it is common to have only one successor-modality: the difference between $\mathbf{[}\alpha\mathbf{]}$ and $\mathbf{\langle}\alpha\mathbf{\rangle}$ only manifests itself over finite traces. Here we have chosen to keep the two modalities, to enable the syntactic comparison between branching-time and linear-time monitorability. From an implementation point of view, recHML formulae, like those in the linear time $\mu$-calculus, can be represented by weak automata (Lange, 2005), which benefit from lower-complexity decision procedures than the more general parity automata, which are necessary to capture the expressiveness of the $\mu$-calculus in a branching-time setting. Note, however, that, as shown in Markey and Schnoebelen (2006), the $\mu$-calculus model-checking problem over paths of the form $s^{\omega}$ is, surprisingly, as hard as the general model-checking problem for that logic.

In the context of RV, many-valued logics (Barringer et al., 2004; d’Angelo et al., 2005; Drusinsky, 2003; Bauer et al., 2010) have also emerged as a way to reconcile the infinitary semantics of, for example, LTL specifications with the finite observations of a monitor. Our concept of monitor can itself also be understood as a logic with three-valued semantics, consisting of accepted traces, rejected traces and traces on which the monitor remains indecisive. Conversely, these many-valued logics can also be seen as describing monitor behaviour, albeit without an operational semantics as in our case. Our parallel monitors are reminiscent of alternating automata. The use of alternating automata for RV is not new: Finkbeiner and Sipma (2004) propose this for the verification of their finite-trace semantics for LTL. The main difference in their approach is that their semantics is not suffix closed: for whether “infinitely often $a$” holds in a finite trace according to their semantics will depend on whether $a$ holds in the last position. In contrast, our verdicts are irrevocable, so a sound monitor for “infinitely often $a$” in our setting will never reach a verdict.

Related Work on Monitorability

The question of exactly which specifications can be verified at runtime is very natural in the RV context. It is perhaps surprising that there is no consensus on what exactly it means for a specification to be monitorable.

The class $\Pi^{0}_{1}$ of the arithmetic hierarchy — the class of co-recursively enumerable safety properties — was proposed as the set of monitorable properties by Viswanathan and Kim (2004). It seems that our notion of partial monitorability matches well with this classical definition. In this sense, partial monitorability could be seen as an operational account of Viswanathan and Kim’s monitorability. On the other hand, Pnueli and Zaks (2006) and Bauer et al. (2011) propose a definition of monitorability that includes more properties: roughly, they call a property monitorable if every prefix has a finite continuation of which either all infinite continuations are in the property, or none is. This means that a monitor, although it does not necessarily ever reach a verdict, can never give up hope of reaching a verdict. Our definitions of monitorability appear to be stronger. For example, specifications such as “never $\mathtt{error}$ and eventually $\mathtt{success}$” is monitorable according to Pnueli and Zaks (2006) and Bauer et al. (2011) but not according to our notions of monitorability and partial monitorability.

Diekert and Leucker have studied monitorability in a topological setting in Diekert and Leucker (2014), where they show that all $\omega$-regular languages that are deterministic and co-deterministic are monitorable. Using their topological framework, they also establish that some deterministic liveness properties, such as “infinitely many a’s”, cannot be written as a countable union of monitorable languages. Diekert et al. (2015) discuss monitor constructions for deterministic $\omega$-regular languages. They isolate a collection of deterministic $\omega$-regular languages that properly includes all the languages that are deterministic and codeterministic, and for which one can construct accepting monitors. These classical definitions of monitorability are independent of how a monitor might be implemented. Conversely, implementations of LTL monitors (Giannakopoulou and Havelund, 2001; Havelund and Rosu, 2002) do not seem to refer to the concept of monitorability at all. In line with previous work (Francalanza et al., 2017b), our operational approach bridges this gap by defining what can be monitored explicitly in terms of how specifications are monitored.

Acknowledgements.

The authors thank Orna Kupferman and Moshe Vardi for clarifying remarks about guarded formulae and pointers to the literature. We thank the anonymous reviewers for their thorough reading of our paper and their insightful comments. This research was partially supported by the projects “TheoFoMon: Theoretical Foundations for Monitorability” (grant number:  Grant #163406-051) and “Epistemic Logic for Distributed Runtime Monitoring” (grant number:  Grant #184940-051) of the Icelandic Research Fund, by the BMBF project “Aramis II” (project number: Grant #01IS160253) and the EPSRC project “Solving parity games in theory and practice” (project number: Grant #EP/P020909/1).

Appendix

Appendix A Properties of Monitors

We first present the omitted proof from Sec. 3

A.1. Regular Monitor Properties

Def. A.1 attempts to characterise the set of reachable states for a monitor. Def. A.3 maps every monitor to a finite positive integer, which can be used to put an upperbound on the size of our state-space approximation of Def. A.1; see Lem. A.1.

Definition A.1 (Monitor State Space Characterisation).

[TABLE]

Definition A.2 (Skip Reachability).

$\textsf{skip\_reach}(m)\,\overset{\leavevmode\resizebox{6.0pt}{}{\,{def}}\,}{=}\,\{\,\textsf{reach}(n)\,\mid\,m\xrightarrow{\;\mu\;}n\,\}$

Definition A.3 (Monitor Measure).

[TABLE]

Lemma A.1**.**

$\forall m\in\textsc{REMon}\cdot|\textsf{states}(m)|\leq\textsf{size}(m)$**

Proof.

By structural induction on $m$. ∎

Lem. A.4 shows that the state-space approximation of Def. A.1 characterises precisely the actual state-space of a monitor. It however relies on a few technical lemmata.

Lemma A.2**.**

For all (possibly open) $m\in\textsc{REMon}$:

1. (1)

m[\raisebox{2.15277pt}{\smalln}\!/\!\mbox{\smallx}]\xrightarrow{\;\mu\;}m^{\prime}\* implies \ (\exists m^{\prime\prime}\cdot m\xrightarrow{\;\mu\;}m^{\prime\prime}\text{ and }m^{\prime\prime}[\raisebox{2.15277pt}{\smalln}\!/\!\mbox{\smallx}]=m^{\prime}) or $(x\text{ is a summand of }m\text{ and }n\xrightarrow{\;\mu\;}m^{\prime})$.* 2. (2)

m\xrightarrow{\;\mu\;}m^{\prime}\* implies \ (\exists m^{\prime\prime}\cdot m[\raisebox{2.15277pt}{\smalln}\!/\!\mbox{\smallx}]\xrightarrow{\;\mu\;}m^{\prime\prime}\text{ and }m^{\prime}[\raisebox{2.15277pt}{\smalln}\!/\!\mbox{\smallx}]=m^{\prime\prime})*

Proof.

Both clauses are proved by structural induction on $m$. The main cases for the first clause are:

**Case $m$ = y:: **

Since y[\raisebox{2.15277pt}{\smalln}\!/\!\mbox{\smallx}]\xrightarrow{\;\mu\;}m^{\prime}, it must be the case that $y=x$ (hence a summand of $m$) and y[\raisebox{2.15277pt}{\smalln}\!/\!\mbox{\smallx}]=n from which we obtain $n\xrightarrow{\;\mu\;}m^{\prime}$ as required.

**Case $m$ = $m_{1}+m_{2}$:: **

We have m[\raisebox{2.15277pt}{\smalln}\!/\!\mbox{\smallx}]=(m_{1}[\raisebox{2.15277pt}{\smalln}\!/\!\mbox{\smallx}])+(m_{2}[\raisebox{2.15277pt}{\smalln}\!/\!\mbox{\smallx}]), meaning that the transition was inferred using eSel. Without loss of generality, assume that m_{1}[\raisebox{2.15277pt}{\smalln}\!/\!\mbox{\smallx}]\xrightarrow{\;\mu\;}m^{\prime}. By the I.H. we obtain the following subcases:

• **•: **

Either (\exists m^{\prime\prime}\cdot m_{1}\xrightarrow{\;\mu\;}m^{\prime\prime}\text{ and }m^{\prime\prime}[\raisebox{2.15277pt}{\smalln}\!/\!\mbox{\smallx}]=m^{\prime}). By eSel we deduce $m_{1}+m_{2}\xrightarrow{\;\mu\;}m^{\prime\prime}$ as required.

• **•: **

Or $x$ is a summand of $m_{1}$ and $n\xrightarrow{\;\mu\;}m^{\prime}$, which is precisely the required result since $x$ is then also a summand of $m_{1}+m_{2}$.

**Case $m$ = $\textsf{rec}\,y.m_{1}$:: **

By mRec, we have m[\raisebox{2.15277pt}{\smalln}\!/\!\mbox{\smallx}]=\textsf{rec}\,y.(m_{1}[\raisebox{2.15277pt}{\smalln}\!/\!\mbox{\smallx}])\xrightarrow{\;\tau\;}m_{1}[\raisebox{2.15277pt}{\smalln}\!/\!\mbox{\smallx}][\raisebox{2.15277pt}{\small\textsf{rec},y.(m_{1}[\raisebox{1.93748pt}{\small$n$}!/!\mbox{\small$x$}])}\!/\!\mbox{\smally}]. Again, by mRec, the required transition is \textsf{rec}\,y.m_{1}\xrightarrow{\;\tau\;}m_{1}[\raisebox{2.15277pt}{\small\textsf{rec},y.m_{1}}\!/\!\mbox{\smally}], since we can infer the equality m_{1}[\raisebox{2.15277pt}{\small\textsf{rec},y.m_{1}}\!/\!\mbox{\smally}][\raisebox{2.15277pt}{\smalln}\!/\!\mbox{\smallx}]=m_{1}[\raisebox{2.15277pt}{\smalln}\!/\!\mbox{\smallx}][\raisebox{2.15277pt}{\small\textsf{rec},y.(m_{1}[\raisebox{1.93748pt}{\small$n$}!/!\mbox{\small$x$}])}\!/\!\mbox{\smally}].

For the second clause, the main cases are:

**Case $m$ = y:: **

The implication holds trivially since variables do not transition.

**Case $m$ = $m_{1}+m_{2}$:: **

By mSel, we have either $m_{1}\xrightarrow{\;\mu\;}m^{\prime}$ or $m_{2}\xrightarrow{\;\mu\;}m^{\prime}$. Without loss of generality, pick $m_{1}\xrightarrow{\;\mu\;}m^{\prime}$. By the I.H. we have m_{1}[\raisebox{2.15277pt}{\smalln}\!/\!\mbox{\smallx}]\xrightarrow{\;\mu\;}m^{\prime\prime} for some $m^{\prime\prime}$ where m^{\prime}[\raisebox{2.15277pt}{\smalln}\!/\!\mbox{\smallx}]=m^{\prime\prime}. Again, using mSel we deduce m[\raisebox{2.15277pt}{\smalln}\!/\!\mbox{\smallx}]=(m_{1}[\raisebox{2.15277pt}{\smalln}\!/\!\mbox{\smallx}])+(m_{2}[\raisebox{2.15277pt}{\smalln}\!/\!\mbox{\smallx}])\xrightarrow{\;\mu\;}m^{\prime\prime} as required.

**Case $m$ = $\textsf{rec}\,y.m_{1}$:: **

By mRec, we have \textsf{rec}\,y.m_{1}\xrightarrow{\;\tau\;}m_{1}[\raisebox{2.15277pt}{\small\textsf{rec},y.m_{1}}\!/\!\mbox{\smally}]. The required transition for m[\raisebox{2.15277pt}{\smalln}\!/\!\mbox{\smallx}]=\textsf{rec}\,y.(m_{1}[\raisebox{2.15277pt}{\smalln}\!/\!\mbox{\smallx}]) is again obtained by the rule mRec in the form of \textsf{rec}\,y.(m_{1}[\raisebox{2.15277pt}{\smalln}\!/\!\mbox{\smallx}])\xrightarrow{\;\tau\;}(m_{1}[\raisebox{2.15277pt}{\smalln}\!/\!\mbox{\smallx}])[\raisebox{2.15277pt}{\small\textsf{rec},y.(m_{1}[\raisebox{1.93748pt}{\small$n$}!/!\mbox{\small$x$}])}\!/\!\mbox{\smally}], since (m_{1}[\raisebox{2.15277pt}{\smalln}\!/\!\mbox{\smallx}])[\raisebox{2.15277pt}{\small\textsf{rec},y.(m_{1}[\raisebox{1.93748pt}{\small$n$}!/!\mbox{\small$x$}])}\!/\!\mbox{\smally}]=(m_{1}[\raisebox{2.15277pt}{\small\textsf{rec},y.m_{1}}\!/\!\mbox{\smally}])[\raisebox{2.15277pt}{\smalln}\!/\!\mbox{\smallx}]. ∎

Lemma A.3**.**

For all (possibly open) $m\in\textsc{REMon}$:

1. (1)

m[\raisebox{2.15277pt}{\smalln}\!/\!\mbox{\smallx}]\xrightarrow[]{\;e\;}\mathrel{\mkern-14.0mu}\rightarrow m^{\prime}* implies that*

• •

Either \exists m^{\prime\prime}\cdot m\xrightarrow[]{\;e\;}\mathrel{\mkern-14.0mu}\rightarrow m^{\prime\prime}\text{ and }m^{\prime\prime}[\raisebox{2.15277pt}{\smalln}\!/\!\mbox{\smallx}]=m^{\prime}

• •

Or $\exists e_{1},e_{2},m^{\prime\prime}\cdot e=e_{1}e_{2}$ and $e_{2}\neq\epsilon$ and $m\xrightarrow[]{\;e\;}\mathrel{\mkern-14.0mu}\rightarrow m^{\prime\prime}$ where $x$ is a summand of $m$ and $n\xrightarrow[]{\;e_{2}\;}\mathrel{\mkern-14.0mu}\rightarrow m^{\prime}$. 2. (2)

$m\xrightarrow[]{\;e\;}\mathrel{\mkern-14.0mu}\rightarrow m^{\prime}$* implies \exists m^{\prime\prime}\cdot(m[\raisebox{2.15277pt}{\smalln}\!/\!\mbox{\smallx}]\xrightarrow[]{\;e\;}\mathrel{\mkern-14.0mu}\rightarrow m^{\prime\prime}\text{ and }m^{\prime}[\raisebox{2.15277pt}{\smalln}\!/\!\mbox{\smallx}]=m^{\prime\prime})*

Proof.

The proof for the second clause is by a straightforward induction on the structure of $e$, where the inductive step relies Lem. A.2(2).

The proof for the first clause is also by induction on $e$, but it is slightly more involved.

**Case $e=\epsilon$:: **

Immediate, since m^{\prime}=m[\raisebox{2.15277pt}{\smalln}\!/\!\mbox{\smallx}] and $m\xrightarrow[]{\;\epsilon\;}\mathrel{\mkern-14.0mu}\rightarrow m$.

**Case $e=\mu f$:: **

We thus have

[TABLE]

By m[\raisebox{2.15277pt}{\smalln}\!/\!\mbox{\smallx}]\xrightarrow{\;\mu\;}m^{\prime\prime} and Lem. A.2(1) we have to consider either of two cases:

1. **(1): **

Either there exists some $m^{\prime\prime\prime}$ such that $m\xrightarrow{\;\mu\;}m^{\prime\prime\prime}$ and m^{\prime\prime\prime}[\raisebox{2.15277pt}{\smalln}\!/\!\mbox{\smallx}]=m^{\prime\prime}. By m^{\prime\prime}=m^{\prime\prime\prime}[\raisebox{2.15277pt}{\smalln}\!/\!\mbox{\smallx}]\xrightarrow[]{\;f\;}\mathrel{\mkern-14.0mu}\rightarrow m^{\prime} from Eq. 9 and the I.H. we have two possibilities:

1. **(a): **

Either there exists some $m^{\prime\prime\prime\prime}$ such that $m^{\prime\prime\prime}\xrightarrow[]{\;f\;}\mathrel{\mkern-14.0mu}\rightarrow m^{\prime\prime\prime\prime}$ where m^{\prime\prime\prime\prime}[\raisebox{2.15277pt}{\smalln}\!/\!\mbox{\smallx}]=m^{\prime}. By prefixing this with $m\xrightarrow{\;\mu\;}m^{\prime\prime\prime}$ gives us $m\xrightarrow[]{\;e\;}\mathrel{\mkern-14.0mu}\rightarrow m^{\prime\prime\prime\prime}$ as required. 2. **(b): **

Or $f=f_{1}f_{2}$ for some $f_{1}$ and $f_{2}\neq\epsilon$ where $m^{\prime\prime\prime}\xrightarrow[]{\;f_{1}\;}\mathrel{\mkern-14.0mu}\rightarrow m^{\prime\prime\prime\prime}$ for some $m^{\prime\prime\prime\prime}$ with a summand $x$ and $n\xrightarrow[]{\;f_{2}\;}\mathrel{\mkern-14.0mu}\rightarrow m^{\prime}$. Again, by contacting $m\xrightarrow{\;\mu\;}m^{\prime\prime\prime}$ with $m^{\prime\prime\prime}\xrightarrow[]{\;f_{1}\;}\mathrel{\mkern-14.0mu}\rightarrow m^{\prime\prime\prime\prime}$ as $m^{\prime}\xrightarrow[]{\;\mu f_{1}\;}\mathrel{\mkern-14.0mu}\rightarrow m^{\prime\prime\prime\prime}$ gives us the result required. 2. **(2): **

Or $x$ is a summand of $m$ and $n\xrightarrow{\;\mu\;}m^{\prime\prime}$. Using $m^{\prime\prime}\xrightarrow[]{\;f\;}\mathrel{\mkern-14.0mu}\rightarrow m^{\prime}$ of Eq. 9, this would satisfy the second clause with $e_{1}=\epsilon$ and $e_{2}=\mu f$ since $m\xrightarrow[]{\;\epsilon\;}\mathrel{\mkern-14.0mu}\rightarrow m$. ∎

We prove the required property for closed monitors. Note that closed monitors are closed with respect to transitions.

Lemma A.4**.**

$\forall m\in\textsc{REMon}\cdot\mathop{\textrm{fv}}(m){=}\emptyset\text{ implies }\textsf{reach}(m)=\textsf{states}(m)\text{ and }\textsf{skip\_reach}(m)=\textsf{skip\_states}(m)$**

Proof.

By structural induction on $m$:

**Case $m$ = $v$:: **

It follows from Lem. 3.1.

**Case $m$ = x:: **

Immediate since $\mathop{\textrm{fv}}(m)\neq\emptyset$.

**Case $m$ = \alpha.$$n:: **

By Def. 3.1 and mAct from Fig. 2, $\textsf{reach}(\alpha.{n})=\left\{\alpha.{n}\right\}{\cup}\textsf{reach}(n)$. By the I.H. we have $\textsf{reach}(n)=\textsf{states}(n)$, and thus $\left\{\alpha.{n}\right\}{\cup}\,\textsf{reach}(n)=\left\{\alpha.{n}\right\}{\cup}\,\textsf{states}(n)=\textsf{states}(\alpha.{n})$ (by Def. A.1). For the second property, we know that $\textsf{skip\_reach}(\alpha.{n})=\textsf{reach}(n)$ by Def. A.2, and that $\textsf{skip\_states}(\alpha.{n})=\textsf{states}(n)$ by Def. A.1. By the I.H. we then obtain $\textsf{reach}(n)=\textsf{states}(n)$ as required.

**Case $m$ = $m_{1}+m_{2}$:: **

For the first property, we deduce that $\textsf{reach}(m_{1}+m_{2})=\left\{m_{1}+m_{2}\right\}\cup\textsf{skip\_reach}(m_{1})\cup\textsf{skip\_reach}(m_{2})$ by Def. 3.1 and mSel from Fig. 2. By Def. A.1, we akso know that $\textsf{states}(m_{1}+m_{2})=\textsf{skip\_states}(m_{1})\cup\textsf{skip\_states}(m_{2})$. The rest of the proof uses the I.H. to obtain the required result, in analogous fashion to the previous case. For the second property we need to show that $\textsf{skip\_reach}(m_{1}+m_{2})=\textsf{skip\_states}(m_{1}+m_{2})$. By mSel from Fig. 2 we know that $\textsf{skip\_reach}(m_{1}+m_{2})=\textsf{skip\_reach}(m_{1})\cup\textsf{skip\_reach}(m_{1})$. By the I.H., we also know that for $i\in 1..2$ $\textsf{skip\_reach}(m_{i})=\textsf{skip\_states}(m_{i})$. The required result thus follows since, by Def. A.1 we have $\textsf{skip\_states}(m_{1}+m_{2})=\textsf{skip\_states}(m_{1})\cup\textsf{skip\_states}(m_{1})$.

**Case $m$ = $\textsf{rec}\,x.n$:: **

By Def. 3.1 and mRec from Fig. 2 we have \textsf{reach}(\textsf{rec}\,x.n)=\left\{\textsf{rec}\,x.n\right\}\cup\textsf{reach}(n[\raisebox{2.15277pt}{\small\textsf{rec},x.n}\!/\!\mbox{\smallx}]). By the I.H. we also know that $\textsf{reach}(n)=\textsf{states}(n)$ which means that (\textsf{reach}(n)[\raisebox{2.15277pt}{\small\textsf{rec},x.n}\!/\!\mbox{\smallx}])=(\textsf{states}(n)[\raisebox{2.15277pt}{\small\textsf{rec},x.n}\!/\!\mbox{\smallx}]) . From Lem. A.3 we deduce \textsf{reach}(n[\raisebox{2.15277pt}{\small\textsf{rec},x.n}\!/\!\mbox{\smallx}])=\textsf{reach}(n)[\raisebox{2.15277pt}{\small\textsf{rec},x.n}\!/\!\mbox{\smallx}] thus \left\{\textsf{rec}\,x.n\right\}\cup\textsf{reach}(n[\raisebox{2.15277pt}{\small\textsf{rec},x.n}\!/\!\mbox{\smallx}])=\left\{\textsf{rec}\,x.n\right\}\cup\textsf{states}(n)[\raisebox{2.15277pt}{\small\textsf{rec},x.n}\!/\!\mbox{\smallx}]=\textsf{states}(\textsf{rec}\,x.n) by Def. A.1, as required. For the second property, we know, by mRec and Def. A.2 that \textsf{skip\_reach}(\textsf{rec}\,x.n)=\textsf{reach}(n[\raisebox{2.15277pt}{\small\textsf{rec},x.n}\!/\!\mbox{\smallx}]). By Def. A.1, we also know that \textsf{skip\_states}(\textsf{rec}\,x.n)=\textsf{states}(n)[\raisebox{2.15277pt}{\small\textsf{rec},x.n}\!/\!\mbox{\smallx}]. Recall that by Lem. A.3 we already established that \textsf{reach}(n[\raisebox{2.15277pt}{\small\textsf{rec},x.n}\!/\!\mbox{\smallx}])=\textsf{reach}(n)[\raisebox{2.15277pt}{\small\textsf{rec},x.n}\!/\!\mbox{\smallx}]. Now by the I.H. we know that $\textsf{reach}(n)=\textsf{states}(n)$, from which we obtain \textsf{reach}(n)[\raisebox{2.15277pt}{\small\textsf{rec},x.n}\!/\!\mbox{\smallx}]=\textsf{states}(n)[\raisebox{2.15277pt}{\small\textsf{rec},x.n}\!/\!\mbox{\smallx}], which is the result required. ∎

A.2. Reactive Parallel Monitors

Lemma A.5** (Monitor Combinators).**

1. (1)

If $m_{1}$ and $m_{2}$ are reactive, then $m_{1}{\otimes}m_{2}\xRightarrow{\;s\;}\textsf{no}$ iff $m_{1}\xRightarrow{\;s\;}\textsf{no}$ or $m_{2}\xRightarrow{\;s\;}\textsf{no}$. 2. (2)

$m_{1}{\otimes}m_{2}\xRightarrow{\;s\;}\textsf{yes}$* iff $m_{1}\xRightarrow{\;s\;}\textsf{yes}$ and $m_{2}\xRightarrow{\;s\;}\textsf{yes}$.* 3. (3)

If $m_{1}$ and $m_{2}$ are reactive, then $m_{1}{\oplus}m_{2}\xRightarrow{\;s\;}\textsf{yes}$ iff $m_{1}\xRightarrow{\;s\;}\textsf{yes}$ or $m_{2}\xRightarrow{\;s\;}\textsf{yes}$. 4. (4)

$m_{1}{\oplus}m_{2}\xRightarrow{\;s\;}\textsf{no}$* iff $m_{1}\xRightarrow{\;s\;}\textsf{no}$ and $m_{2}\xRightarrow{\;s\;}\textsf{no}$.* 5. (5)

If $s\neq\varepsilon$ or $m_{1},m_{2}\neq v$, then $m_{1}+m_{2}\xRightarrow{\;s\;}v$ iff $m_{1}\xRightarrow{\;s\;}v$ or $m_{2}\xRightarrow{\;s\;}v$.

Proof.

We first prove the “only if” directions for the five statements. If $m_{1}{\otimes}m_{2}\xRightarrow{\;s\;}\textsf{no}$, then there is an explicit trace $e$ that agrees with $s$ on the external actions, such that $m_{1}{\otimes}m_{2}\xrightarrow{\;e\;}\textsf{no}$. We prove by induction on $e$ that $m_{1}\xRightarrow{\;s\;}\textsf{no}$ or $m_{2}\xRightarrow{\;s\;}\textsf{no}$.

The base case is $e=\varepsilon$, which is a contradiction, because it implies that $m_{1}{\otimes}m_{2}=\textsf{no}$. For the inductive step, let $e=\mu f$ and $m_{1}{\otimes}m_{2}\xrightarrow{\;\mu\;}m\xrightarrow{\;f\;}\textsf{no}$. We distinguish the following cases:

**Case $\mu\in\textsc{Act}$:: **

Then, $m=m_{1}^{\prime}{\otimes}m_{2}^{\prime}$, where $m_{1}\xrightarrow{\;\mu\;}m_{1}^{\prime}$ and $m_{2}\xrightarrow{\;\mu\;}m_{2}^{\prime}$, and rule mPar was used, so the claim follows by the inductive hypothesis applied to $m\xrightarrow{\;f\;}\textsf{no}$.

**Case $\mu=\tau$ and $m=m_{1}^{\prime}{\otimes}m_{2}^{\prime}$, where $m_{1}\xrightarrow{\;\mu\;}m_{1}^{\prime}$ or $m_{2}\xrightarrow{\;\mu\;}m_{2}^{\prime}$: **

(that is, rule mTauL or rule mTauR was used). Then, again, the claim follows by the inductive hypothesis.

**Otherwise:: **

The only possibilities are that $\mu=\tau$ and rule mVrC1 or mVrC2 were used, so respectively, $m=m_{1}$ or $m=m_{2}$, so $m_{1}\xrightarrow{\;f\;}\textsf{no}$ or $m_{2}\xrightarrow{\;f\;}\textsf{no}$; or $m=\textsf{no}$ and either $m_{1}=\textsf{no}$ or $m_{2}=\textsf{no}$. In all cases, we have that $m_{1}\xRightarrow{\;s\;}\textsf{no}$ or $m_{1}\xRightarrow{\;s\;}\textsf{no}$.

The “only if” directions for the other cases are proven in a similar way.

We now prove the “if” directions of the statements of the lemma, and specifically we prove that if $m_{1}\xRightarrow{\;s\;}\textsf{no}$ and $m_{2}$ is reactive, then $m_{1}{\otimes}m_{2}\xRightarrow{\;s\;}\textsf{no}$; the remaining cases are analogous. Assume that $m_{1}\xRightarrow{\;s\;}\textsf{no}$. Then, there is an explicit trace $e$ that agrees with $s$ on the external actions, such that $m_{1}\xrightarrow{\;e\;}\textsf{no}$ — fix $e$ to be the shortest such explicit trace for $m_{1}$ and $s$. We proceed by induction on the length of $e$.

**Case $e=\varepsilon$:: **

Then $m_{1}=\textsf{no}$ and $\textsf{no}{\otimes}m_{2}\xrightarrow{\;\tau\;}\textsf{no}$.

**Case $e=\tau f$:: **

Then, $m_{1}\xrightarrow{\;\tau\;}m_{1}^{\prime}\xrightarrow{\;f\;}\textsf{no}$. By rule mTauL, $m_{1}{\otimes}m_{2}\xrightarrow{\;\tau\;}m_{1}^{\prime}{\otimes}m_{2}$, and by the inductive hypothesis, $m_{1}^{\prime}{\otimes}m_{2}\xrightarrow{\;s\;}\textsf{no}$.

**Case $e=\alpha f$:: **

Then, $m_{1}\xrightarrow{\;\alpha\;}m_{1}^{\prime}\xrightarrow{\;s^{\prime}\;}\textsf{no}$. Since $m_{2}$ is reactive, there is a reactive $m_{2}^{\prime}$, such that $m_{2}\xRightarrow{\;\alpha\;}m_{2}^{\prime}$, and by successive applications of rule mTauR and then rule mPar, and the inductive hypothesis, $m_{1}{\otimes}m_{2}\xRightarrow{\;\alpha\;}m_{1}^{\prime}{\otimes}m_{2}^{\prime}\xRightarrow{\;s\;}\textsf{no}$.

Statements (2), (3), and (4) are proven similarly. For (5), we observe that if $m_{1}+m_{2}\xRightarrow{s}v$, then there is an explicit trace $e$ that agrees with $s$ on the external actions, such that $m_{1}+m_{2}\xrightarrow{\;e\;}v$, and since $m_{1}+m_{2}\neq v$, $e=\mu f$; therefore, there is some $m$ such that $m_{1}+m_{2}\xrightarrow{\;\mu\;}m\xrightarrow{\;f\;}v$. According to the monitor rules, for some $i\in\{1,2\}$, $m_{i}\xrightarrow{\;\mu\;}m$, and thus, $m_{i}\xRightarrow{\;s\;}v$. For the other direction, if, say, $m_{1}\xRightarrow{\;s\;}v$, then there is an explicit trace $e$, such that $m_{1}\xrightarrow{\;e\;}v$; since $m_{1}\neq v$ or $s\neq\varepsilon$, we see that $e=\mu f$, and the remaining argument is as above. ∎

Remark*.*

Lem. A.5 indirectly describes three different kinds of non-determinism for reactive parallel monitors. Operator ${\oplus}$ can be thought of as an existential monitor choice, as $m_{1}{\oplus}m_{2}$ will accept (resp., reject) iff either (resp., both) of its components accepts (resp., reject). Dually, ${\otimes}$ can be thought of as a universal choice. The operator $+$ is a different choice that favours neither acceptance nor rejection, but generates either verdict, as long as one of its component monitors can reach it. $\hfill\qed$

Remark*.*

3.2 indicates that the assumption that $m_{1}$ and $m_{2}$ are reactive are needed in statements (1) and (3) of the above lemma. However, as the following lemma demonstrates, that assumption is only necessary to prove one (the “if”) direction of statements (1) and (3) in Lem. A.5.

Lemma A.6**.**

1. (1)

If $m_{1}{\otimes}m_{2}\xrightarrow{\;e\;}\textsf{no}$, then $m_{1}\xrightarrow{\;f\;}\textsf{no}$ or $m_{2}\xrightarrow{\;f\;}\textsf{no}$, where $f$ agrees with $e$ on the external actions and is strictly shorter than $e$. 2. (2)

If $m_{1}{\otimes}m_{2}\xrightarrow{\;e\;}\textsf{yes}$, then $m_{1}\xrightarrow{\;f\;}\textsf{yes}$ and $m_{2}\xrightarrow{\;f^{\prime}\;}\textsf{yes}$, where $f,f^{\prime}$ agree with $e$ on the external actions and are strictly shorter than $e$. 3. (3)

If $m_{1}{\oplus}m_{2}\xrightarrow{\;e\;}\textsf{yes}$, then $m_{1}\xrightarrow{\;f\;}\textsf{yes}$ or $m_{2}\xrightarrow{\;f\;}\textsf{yes}$, where $f$ agrees with $e$ on the external actions and is strictly shorter than $e$. 4. (4)

If $m_{1}{\oplus}m_{2}\xrightarrow{\;e\;}\textsf{no}$, then $m_{1}\xrightarrow{\;f\;}\textsf{no}$ and $m_{2}\xrightarrow{\;f^{\prime}\;}\textsf{no}$, where $f,f^{\prime}$ agree with $e$ on the external actions and are strictly shorter than $e$.

Proof.

We can use the same induction as for the “only if” direction of the proof of Lemma A.5, noticing that the explicit traces for the submonitors are shorter than $e$. ∎

In the technical developments that follow, we will require the following version of statements (1) and (3) of Lems. A.5 and A.6.

Lemma A.7**.**

1. (1)

If $s$ is minimal such that $m{\otimes}n\xRightarrow{\;s\;}\textsf{no}$, then there are $q_{1},q_{2}$, such that $m\xRightarrow{\;s\;}q_{1}$ and $n\xRightarrow{\;s\;}q_{2}$, and $q_{1}=\textsf{no}$ or $q_{2}=\textsf{no}$. 2. (2)

If $s$ is minimal such that $m{\oplus}n\xRightarrow{\;s\;}\textsf{yes}$, then there are $q_{1},q_{2}$, such that $m\xRightarrow{\;s\;}q_{1}$ and $n\xRightarrow{\;s\;}q_{2}$, and $q_{1}=\textsf{yes}$ or $q_{2}=\textsf{yes}$.

Proof.

We prove the first part of the lemma, as the second one is similar. Since $m{\otimes}n\xRightarrow{\;s\;}\textsf{no}$, there must be an external trace $e$ that agrees with $s$ on the external actions, so that $m{\otimes}n\xrightarrow{\;e\;}\textsf{no}$. We can use a similar induction on $e$ as for the first direction of the proof for Lemma A.5. The base case is $e=\tau^{k}$, which is immediate, because, by Lemma A.6, it implies that $m\xRightarrow{\;\;}\textsf{no}$ or $n\xRightarrow{\;\;}\textsf{no}$. For the inductive step, let $s\neq\varepsilon$, $e=\mu e^{\prime}$, and $m{\otimes}n\xrightarrow{\;\mu\;}q\xrightarrow{\;e^{\prime}\;}\textsf{no}$. We distinguish the following cases:

**Case $\mu\in\textsc{Act}$: **

(that is, rule mPar was used): Then, $q=m^{\prime}{\otimes}n^{\prime}$, where $m\xrightarrow{\;\mu\;}m^{\prime}$ and $n\xrightarrow{\;\mu\;}n^{\prime}$, and the induction is complete by the inductive hypothesis.

**Case $\mu=\tau$ and $q=m^{\prime}{\otimes}n^{\prime}$, where $m\xrightarrow{\;\mu\;}m^{\prime}$ or $n\xrightarrow{\;\mu\;}n^{\prime}$: **

(that is, one of the rules mTauL and mTauR was used): Then, again, the induction is complete by the inductive hypothesis.

**Case $\mu=\tau$ and rule mVrC1 was used:: **

Then, without loss of generality, $m{\otimes}n\xrightarrow{\;\tau\;}m\xrightarrow{\;e^{\prime}\;}\textsf{no}$ and $n=\textsf{yes}$, in which case we have that $m\xRightarrow{\;s\;}\textsf{no}$ and $n=\textsf{yes}\xrightarrow{\;s\;}\textsf{yes}$.

**Case $\mu=\tau$ and rule mVrC2 was used:: **

Then, without loss of generality, $m{\otimes}n\xrightarrow{\;\tau\;}m=\textsf{no}$, which is a contradiction, because either $s=\varepsilon$ or it is not minimal, which violates our assumptions. ∎

Remark*.*

We remark that although Lem. A.7 seems to be an immediate consequence of Lems. A.5 and A.6, this is not the case. Notice that Lem. A.7 asserts that both components are able to follow the finite trace $s$, and this is the reason the minimality of $s$ is important. Otherwise, a counterexample would be $\textsf{no}{\otimes}\alpha.\textsf{yes}\xRightarrow{\;\beta\;}\textsf{no}$, as $\alpha.\textsf{yes}$ cannot transition with a $\beta$.

A.3. An Equivalence of Two Monitoring Systems

To prove Prop. 3.6, we assume a different set of rules for parallel and regular monitors. These rules are the ones that result by replacing mRec with the following rules:

[TABLE]

Here, we assume that for every monitor variable $x$, there is a unique monitor $p_{x}=\textsf{rec}\,x.m_{x}$ of $m$ such that $x$ appears in $m_{x}$. Therefore, the rules above are well-defined. By substituting rule mRec by mRecF and mRecB, we get an equivalent monitoring system, where reactive monitors remain reactive. This is partly shown in Aceto et al. (2016) for regular monitors and here we prove these claims in the context of parallel monitors. Thus, in the rest of this section we assume that the rules above are used.

We call System O the system of rules given in Table 2, while System N is the result of replacing rule mRec by the rules mRecF and mRecB. The reader is encouraged to read Aceto et al. (2016) for a discussion of the two systems.

For System N, we assume the fixed mappings $x\mapsto p_{x}$ and $x\mapsto m_{x}$, such that $p_{x}=\textsf{rec}\,x.m_{x}$ and $p_{x}$ is the only monitor of the form $\textsf{rec}\,x.m$ that we allow. Derivations $\xrightarrow{\;\;}$ and $\xRightarrow{\;\;}$ are defined as before, but the resulting relations are called $\xrightarrow{\;\;}_{O}$ and $\xRightarrow{\;\;}_{O}$, and $\xrightarrow{\;\;}_{N}$ and $\xRightarrow{\;\;}_{N}$, respectively for systems O and N. We prove that systems O and N are equivalent. That is, for any monitor $m$, finite trace $s$, and verdict $v$,

[TABLE]

Lemma A.8**.**

For every $x$, $p_{x}$ is simple.

Proof.

Immediate from the definition. ∎

Lemma A.9**.**

If $x$ is a free variable in $p_{y}$, then $p_{y}$ is inside the scope of $p_{x}$.

Proof.

An immediate observation. ∎

There is an ordering $\leq$ of monitor variables: $x\leq y$ iff $p_{y}$ is in the scope of $p_{x}$. We note that if we only consider a finite number of variables (say, the ones that appear in a specific monitor), then $\leq$ is a well-order. This ordering allows us to define when a submonitor can substitute a variable for its corresponding recursive formula. We recursively define when $n$ is an unfolding of $r$: $n=r$; or $n=n^{\prime}[p_{x}/x]$, where $n^{\prime}$ is an unfolding of $r$ and $x$ is $\leq$-minimal among the variables that occur free in $n^{\prime}$.

Lemma A.10**.**

If $n$ is an unfolding of $r$, then

1. (1)

$n=v$* if and only if $r=v$;* 2. (2)

for every $\alpha\in\textsc{Act}$ and $n^{\prime}$, if $n\xrightarrow{\;\alpha\;}_{N}n^{\prime}$, then there some $r^{\prime}$, such that $r\xRightarrow{\;\alpha\;}_{N}r^{\prime}$ and $n^{\prime}$ is an unfolding of $r^{\prime}$; 3. (3)

for every $\alpha\in\textsc{Act}$ and $n^{\prime}$, if $r\xrightarrow{\;\alpha\;}_{N}r^{\prime}$, then there some $n^{\prime}$, such that $n\xrightarrow{\;\alpha\;}_{N}n^{\prime}$ and $n^{\prime}$ is an unfolding of $r^{\prime}$; 4. (4)

if $n\xRightarrow{\;\;}_{N}n^{\prime}$, then there some $r^{\prime}$, such that $r\xRightarrow{\;\;}_{N}r^{\prime}$ and $n^{\prime}$ is an unfolding of $r^{\prime}$; 5. (5)

if $r\xRightarrow{\;\;}_{N}r^{\prime}$, then there some $n^{\prime}$, such that $n\xRightarrow{\;\;}_{N}n^{\prime}$ and $n^{\prime}$ is an unfolding of $r^{\prime}$.

Proof.

The proof is by induction on the number of substitutions required to construct $n$ from $r$. The base case of $n=r$ is trivial. To complete the inductive step, it suffices to prove the lemma for the case of $n=r[p_{x}/x]$. This is done by induction on the structure of $r$.

• •

If $r$ is a verdict $v$ or a variable $y\neq x$, then $n=r$ and we are done.

• •

If $r=x$, then $n=p_{x}$. Since $x$ can transition exactly to $p_{x}$ with a $\tau$, $r\centernot{\xrightarrow{\;\alpha\;}}r^{\prime}$ and if $n\xRightarrow{\;\alpha\;}n^{\prime}$, then $r=x\xrightarrow{\;\tau\;}p_{x}\xrightarrow{\;\alpha\;}n^{\prime}$. Similarly, if $r\xRightarrow{\;\;}r^{\prime}$, then either $r=r^{\prime}$, so we can have $n=n^{\prime}$, or $r=x\xrightarrow{\;\tau\;}p_{x}\xRightarrow{\;\;}r^{\prime}$, in which case $n\xRightarrow{\;\;}r^{\prime}$; if $n\xRightarrow{\;\;}n^{\prime}$, then $r=x\xrightarrow{\;\tau\;}p_{x}=n\xRightarrow{\;\;}n^{\prime}$.

• •

If $r=\alpha.r^{\prime\prime}$, then $n=\alpha.n^{\prime\prime}$ and $n^{\prime\prime}=r^{\prime\prime}[p_{x}/x]$. The only possible transitions for $n$ and $r$ are then $n\xrightarrow{\;\alpha\;}n^{\prime\prime}$ and $r\xrightarrow{\;\alpha\;}r^{\prime\prime}$, respectively. Therefore, $n\xrightarrow{\;\alpha\;}n^{\prime}$ iff $n^{\prime\prime}=n^{\prime}$ and $r\xrightarrow{\;\alpha\;}r^{\prime}$ iff $r^{\prime\prime}=r^{\prime}$; $n\xRightarrow{\;\;}n^{\prime}$ iff $n=n^{\prime}$ and $r\xRightarrow{\;\;}r^{\prime}$ iff $r=r^{\prime}$.

• •

If $r=\textsf{rec}\,x.r^{\prime\prime}$, then $n=r[r/x]=r$, as $r=p_{x}$ and $x$ is bound in $r$; therefore, this case is complete.

• •

If $r=\textsf{rec}\,y.r^{\prime\prime}$ for $y\neq x$, then $n=\textsf{rec}\,y.n^{\prime\prime}$ and $n^{\prime\prime}=r^{\prime\prime}[p_{x}/x]$. The only possible strong transitions for $n$ and $r$ are then $n\xrightarrow{\;\tau\;}n^{\prime\prime}$ and $r\xrightarrow{\;\tau\;}r^{\prime\prime}$, respectively. Then, $n\centernot{\xrightarrow{\;\alpha\;}}n^{\prime}$ and $r^{\prime\prime}\centernot{\xrightarrow{\;\alpha\;}}r^{\prime}$. If $n\xRightarrow{\;\;}n^{\prime}$, then either $n=n^{\prime}$ and we are done, or $n^{\prime\prime}\xRightarrow{\;\;}n^{\prime}$, so $r\xrightarrow{\;\tau\;}r^{\prime\prime}\xRightarrow{\;\;}r^{\prime}$; the case for $r\xRightarrow{\;\;}r^{\prime}$ is symmetric.

• •

If $r=r_{1}+r_{2}$, then $n=n_{1}+n_{2}$, where $n_{i}=r_{i}[p_{x}/x]$ for $i\in\{1,2\}$. Then, if $n\xrightarrow{\;\alpha\;}n^{\prime}$, then $n_{1}\xrightarrow{\;\alpha\;}n^{\prime}$ or $n_{2}\xrightarrow{\;\alpha\;}n^{\prime}$, so $r_{1}\xRightarrow{\;\alpha\;}r^{\prime}$ or $r_{2}\xRightarrow{\;\alpha\;}r^{\prime}$, implying $r\xRightarrow{\;\alpha\;}r^{\prime}$ and we are done by the inductive hypothesis; the remaining cases are similar.

• •

If $r=r_{1}{\otimes}r_{2}$, then $n=n_{1}{\otimes}n_{2}$, where $n_{i}=r_{i}[p_{x}/x]$, for $i\in\{1,2\}$. The remaining argument is similar to the above.

• •

If $r=r_{1}{\oplus}r_{2}$, then $n=n_{1}{\oplus}n_{2}$, where $n_{i}=r_{i}[p_{x}/x]$, for $i\in\{1,2\}$. The remaining argument is similar to the above. ∎

As Lemma A.10 demonstrates, the unfolding relation is a kind of bisimulation for System N — although we do not define such a notion here. It is not hard to see that this relation is reflexive and transitive.

Corollary A.11**.**

If $n$ is an unfolding of $r$, then for every finite trace $s$,

1. (1)

if $n\xRightarrow{\;s\;}_{N}n^{\prime}$, then $r\xRightarrow{\;s\;}_{N}r^{\prime}$, where $n^{\prime}$ is an unfolding of $r^{\prime}$. 2. (2)

Furthermore, if $r\xRightarrow{\;s\;}_{N}r^{\prime}$, then $n\xRightarrow{\;s\;}_{N}n^{\prime}$, where $n^{\prime}$ is an unfolding of $r^{\prime}$.

Proof.

By straightforward induction on $s$. ∎

Lemma A.12**.**

For every closed monitor $n$,

1. (1)

$n\xrightarrow{\;\alpha\;}_{O}n^{\prime}$* if and only if $n\xrightarrow{\;\alpha\;}_{N}n^{\prime}$;* 2. (2)

if $n\xrightarrow{\;\tau\;}_{O}n^{\prime}$, then $n\xrightarrow{\;\tau\;}_{N}n^{\prime\prime}$, where $n^{\prime}$ is an unfolding of $n^{\prime\prime}$; 3. (3)

if $n\xrightarrow{\;\tau\;}_{N}n^{\prime\prime}$, then $n\xrightarrow{\;\tau\;}_{O}n^{\prime}$, where $n^{\prime}$ is an unfolding of $n^{\prime\prime}$.

Proof.

Immediate from the rules. ∎

Corollary A.13**.**

For every $n,r$, where $n$ is closed and an unfolding of $r$,

1. (1)

if $n\xrightarrow{\;\alpha\;}_{O}n^{\prime}$, then $r\xRightarrow{\;\alpha\;}_{N}r^{\prime}$, where $n^{\prime}$ is an unfolding of $r^{\prime}$; 2. (2)

if $r\xrightarrow{\;\alpha\;}_{N}r^{\prime}$, then $n\xrightarrow{\;\alpha\;}_{O}n^{\prime}$ where $n^{\prime}$ is an unfolding of $r^{\prime}$; 3. (3)

if $n\xrightarrow{\;\tau\;}_{O}n^{\prime}$, then $r\xRightarrow{\;\;}_{N}r^{\prime}$, where $n^{\prime}$ is an unfolding of $r^{\prime}$; 4. (4)

if $r\xrightarrow{\;\tau\;}_{N}r^{\prime}$, then $n\xRightarrow{\;\;}_{O}n^{\prime}$, where $n^{\prime}$ is an unfolding of $n^{\prime\prime}$.

Proof.

A consequence of Lemmata A.10 and A.12. ∎

Lemma A.14**.**

For every closed monitor $m$, $m\xRightarrow{\;s\;}_{O}v$ if and only if $m\xRightarrow{\;s\;}_{N}v$.

Proof.

Specifically, we prove that the more general claim that if $m$ is an unfolding of $r$, then $m\xRightarrow{\;s\;}_{O}v$ if and only if $r\xRightarrow{\;s\;}_{N}v$. We prove each direction separately. If $m\xRightarrow{\;s\;}_{O}v$, then there is an explicit trace $e$ that agrees with $s$ on the external actions, such that $m\xrightarrow{\;e\;}_{O}v$. Using induction on $e$, the first part of Lemma A.10, and Corollary A.13, it is not hard to prove that $r\xRightarrow{\;s\;}v$. The other direction is similar. ∎

Corollary A.15**.**

If $m$ is reactive for System O, then it is also reactive for System N.

Proof.

From Corollary A.13 and straightforward induction on the number of transitions to reach a monitor in $\textsf{reach}(m)$. ∎

A.4. Monitor Transformations

To prove Proposition 3.6, we use the following lemmata.

Lemma A.16**.**

• •

If $m=n{\oplus}n^{\prime}$ and $m\xRightarrow{\;\alpha\;}$, then either $m\xRightarrow{\;\;}\textsf{no}$, or $n\xRightarrow{\;\alpha\;}$ and $n^{\prime}\xRightarrow{\;\alpha\;}$.

• •

If $m=n{\otimes}n^{\prime}$ and $m\xRightarrow{\;\alpha\;}$, then either $m\xRightarrow{\;\;}\textsf{yes}$, or $n\xRightarrow{\;\alpha\;}$ and $n^{\prime}\xRightarrow{\;\alpha\;}$.

Proof.

We prove the first case, as the second one is similar. If $m\xRightarrow{\;\alpha\;}q$, then we can assume that $m(\xrightarrow{\;\tau\;})^{k}\xrightarrow{\;\alpha\;}q$. We prove the claim by induction on $k$. The case for $k=0$ is immediate from rule mPar. If $m\xrightarrow{\;\tau\;}m^{\prime}(\xrightarrow{\;\tau\;})^{k}\xrightarrow{\;\alpha\;}q$, then one of the following rules was used:

**mTauL or mTauR: **

In this case, we are done by the inductive hypothesis.

**mVrE: **

In this case, $n=n^{\prime}=\textsf{end}\xRightarrow{\;\alpha\;}\textsf{end}$.

**mVrC1: **

In this case, without loss of generality, $n=\textsf{yes}\xRightarrow{\;\alpha\;}\textsf{yes}$ and $n^{\prime}=m^{\prime}\xRightarrow{\;\alpha\;}q$.

**mVrC2: **

In this case, without loss of generality, $m^{\prime}=\textsf{no}$ and therefore, $m\xRightarrow{\;\;}\textsf{no}$. ∎

Definition A.4.

We can define that $n$ is an immediate submonitor of $m$ recursively: $m$ is a immediate submonitor of $m$, and the immediate submonitors of $m$ are also immediate submonitors of $\alpha.m$, $\textsf{rec}\,x.m$, $m+n$, and $n+m$.

Lemma A.17**.**

Let $n$ be an immediate submonitor of a reactive monitor $m$. Then, for every $n^{\prime}$ for which $n\longrightarrow n^{\prime}$, $n^{\prime}$ is reactive.

Proof.

The proof is by induction on $l(m)-l(n)$ and the base case is $m=n$, which is trivial. If $m^{\prime}=\alpha.n$ is an immediate submonitor of $m$, then $m^{\prime}\xrightarrow{\;\alpha\;}n$, so by the inductive hypothesis, $n$ is reactive and $n^{\prime}\in\textsf{reach}(n)$, so $n^{\prime}$ is also reactive. The case is similar for $m^{\prime}=\textsf{rec}\,x.n\xrightarrow{\;\tau\;}n$: by the inductive hypothesis, $n$ is reactive and $n^{\prime}\in\textsf{reach}(n)$, so $n^{\prime}$ is also reactive. If $m^{\prime}=n+m^{\prime\prime}$ or $m^{\prime}=m^{\prime\prime}+n$, and $m^{\prime}$ is an immediate submonitor of $m$, then, $n\longrightarrow n^{\prime}$ implies that $m^{\prime}\longrightarrow n^{\prime}$ and we are done by the inductive hypothesis. ∎

• Proposition 3.6

*For every reactive parallel monitor $m$, there is an alternating automaton that accepts $L_{a}(m)$ and one that accepts $L_{r}(m)$. *

Proof.

For completeness of exposition, we describe here, as well, the process of constructing an alternating automaton that accepts $L_{a}(m)$ — the case for $L_{r}(m)$ is similar. The automaton for $m$ is $A_{m}=(Q,\textsc{Act},m,\delta,F)$, where

• •

$Q$ is the set of submonitors of $m$;

• •

$F=\{n\in Q\mid n\text{ accepts }\varepsilon\}$;

• •

Let for every $S\subseteq Q$, $\delta_{0}(q,\alpha)(S)=1$ iff $q\in F$; $\delta$ is the closure of $\delta_{0}$ under the following conditions. For every $S\subseteq Q$:

• –

if $n\in S$, then $\delta(\alpha.n,\alpha)(S)=1$;

• –

if $\delta(n,\alpha)(S)=1$ or $\delta(n^{\prime},\alpha)(S)=1$, then $\delta(n+n^{\prime},\alpha)(S)=1$;

• –

if $\delta(n,\alpha)(S)=1$ or $\delta(n^{\prime},\alpha)(S)=1$, and $n\xRightarrow{\;\alpha\;}$ and $n^{\prime}\xRightarrow{\;\alpha\;}$, then $\delta(n{\oplus}n^{\prime},\alpha)(S)=1$;

• –

if $\delta(n,\alpha)(S)=1$ and $\delta(n^{\prime},\alpha)(S)=1$, then $\delta(n{\otimes}n^{\prime},\alpha)(S)=1$;

• –

if $\delta(m_{x},\alpha)(S)=1$, then $\delta(p_{x},\alpha)(S)=\delta(x,\alpha)(S)=1$.

We consider the parallel extension of a set $S$ of monitors in $Q$, which is the smallest set $S^{+}$ such that $S\subseteq S^{+}$, and if $n,n^{\prime}\in S^{+}$, then $n{\otimes}n^{\prime}\in S^{+}$, and if $n\in S^{+}$, then $n{\oplus}n^{\prime},n^{\prime}{\oplus}n\in S^{+}$. We prove the following claims:

Claim 1:

If $\delta(n,\alpha)(S)=1$, then $\exists q\in(S\cup F)^{+}.n\xRightarrow{\;\alpha\;}q$. By induction on the closure conditions for $\delta$. The base case is that $\delta_{0}(n,\alpha)=1$, which implies that $n\xRightarrow{\;\;}\textsf{yes}\xrightarrow{\;\alpha\;}\textsf{yes}\in F$. The remaining cases are straightforward.

Claim 2:

If $\delta^{*}(n,s)(F)=1$, then $\delta^{*}(n,sr)(F)=1$. We observe that $\delta^{*}(n,s)(S)$ is monotone with respect to $S$ (i.e., if $S\subseteq S^{\prime}$ and $\delta^{*}(n,s)(S)=1$, then $\delta^{*}(n,s)(S^{\prime})=1$). The claim follows by a straightforward induction on $s$.

Claim 3:

If $n_{1}\xRightarrow{\;s\;}\textsf{yes}$ and $n_{1}{\oplus}n_{2}$ is reactive, then $n_{1}{\oplus}n_{2}\xRightarrow{\;s\;}\textsf{yes}$. The proof is by induction on $s$. If $s=\varepsilon$, then $n_{1}\xRightarrow{\;\;}\textsf{yes}$, which implies that $n_{1}{\oplus}n_{2}\xRightarrow{\;s\;}\textsf{yes}{\oplus}n_{2}\xrightarrow{\;\tau\;}\textsf{yes}$. If $s=\alpha r$, then $n_{1}\xRightarrow{\;\alpha\;}n^{\prime}\xRightarrow{\;r\;}\textsf{yes}$. Since $n_{1}{\oplus}n_{2}$ is reactive, there is some $q$ such that $n_{1}{\oplus}n_{2}\xRightarrow{\;\alpha\;}q$. Therefore, by Lemma A.16, either $n_{1}{\oplus}n_{2}\xRightarrow{\;\;}\textsf{yes}$, or there is some $q^{\prime}$, such that $n_{2}\xRightarrow{\;\alpha\;}q^{\prime}$. Therefore, $n_{1}{\oplus}n_{2}\xRightarrow{\;\alpha\;}n_{1}^{\prime}{\oplus}q^{\prime}$, and we are done by the inductive hypothesis.

Claim 4:

If every $n\in S$ accepts $s$, then every reactive $n\in S^{+}$ accepts $s$. The proof is by induction on the construction of $n$ from monitors in $S$. If $n\in S$, then by our assumptions, $n$ accepts $s$. If $n=n_{1}{\otimes}n_{2}$ where $n_{1},n_{2}\in S^{+}$, then by the inductive hypothesis, $n_{1},n_{2}\xRightarrow{\;s\;}\textsf{yes}$; using the rules for parallel monitors and induction on $s$, we can complete the proof. If $n=n_{1}{\oplus}n_{2}$ where $n_{1}\in S^{+}$, then by the inductive hypothesis, $n_{1}\xRightarrow{\;s\;}\textsf{yes}$. Then, the proof is complete by Claim 3.

Using the above claims, we now prove that $m$ accepts $s$ if and only if $\delta^{*}(m,s)(F)=1$. We prove each implication separately for the submonitors of $m$.

We first prove that if $n$ accepts $s$, then $\delta^{*}(n,s)(F)=1$.

By Claim 2, we can assume that $s$ is minimal such that $n\xRightarrow{\;s\;}\textsf{yes}$. If $n$ accepts $s$, then there is an explicit trace $e$ that agrees with $s$ on the external actions, such that $n\xrightarrow{\;e\;}\textsf{yes}$. Thus, we prove that for every explicit trace $e$, if $s$ is a finite trace that agrees with $e$ on the external actions, $n\xrightarrow{\;e\;}\textsf{yes}$, and $s$ is minimal such that $n\xRightarrow{\;s\;}\textsf{yes}$, then $\delta^{*}(n,s)(F)=1$. We prove this claim by induction on $e$:

**Case $e\in\{\tau\}^{*}$:: **

Then $n$ accepts $\varepsilon$, so by the definition of $F$, $\delta^{*}(n,s)(F)=1$.

**Case $e\notin\{\tau\}^{*}$ and $n=n_{1}{\otimes}n_{2}$:: **

Let $s=\alpha r$. Since $n\xrightarrow{\;e\;}\textsf{yes}$, by Lemma A.6, there are explicit traces $e_{1},e_{2}$ that agree with $e$ (and with $s$) on the external actions and are strictly shorter than $e$, such that $n_{1}\xrightarrow{\;e_{1}\;}\textsf{yes}$ and $n_{2}\xrightarrow{\;e_{2}\;}\textsf{yes}$. By the inductive hypothesis, $\delta^{*}(n_{1},s)(F)=\delta^{*}(n_{2},s)(F)=1$. Let $S=\{n^{\prime\prime}\mid\delta^{*}(n^{\prime\prime},r)(F)=1\}$; by the definition of $\delta^{*}$,  $\delta(n_{1},\alpha)(S)=\delta(n_{2},\alpha)(S)=\delta^{*}(n_{1},s)(F)=1$, and thus, by the closure properties of $\delta$, we have that $\delta^{*}(n,s)(F)=\delta(n,\alpha)(S)=1$.

**Case $e\notin\{\tau\}^{*}$ and $n=n_{1}{\oplus}n_{2}$, : **

let $s=\alpha r$. Since $n\xrightarrow{\;e\;}\textsf{yes}$, by Lemma A.6, (without loss of generality) there is an explicit trace $e_{1}$ that agrees with $e$ (and with $s$) on the external actions and is strictly shorter than $e$, such that $n_{1}\xrightarrow{\;e_{1}\;}\textsf{yes}$. Therefore, $n_{1}\xRightarrow{\;\alpha\;}$, and by the minimality of $s$ and Lemma A.7, $n_{2}\xRightarrow{\;\alpha\;}$. By the inductive hypothesis, $\delta^{*}(n_{1},s)(F)=1$. Let $S=\{n^{\prime\prime}\mid\delta^{*}(n^{\prime\prime},r)(F)=1\}$; by the definition of $\delta^{*}$, we have that $\delta(n_{1},\alpha)(S)=\delta^{*}(n_{1},s)(F)=1$. Thus, by the closure properties of $\delta$, we can conclude that $\delta^{*}(n,s)(F)=\delta(n,\alpha)(S)=1$.

**Case $e=\tau f$ and $s=\alpha r$:: **

Then $n\xrightarrow{\;\tau\;}n^{\prime}$ for some $n^{\prime}\xrightarrow{\;f\;}\textsf{yes}$ that agrees with $s$ on the external actions. By the inductive hypothesis, $\delta^{*}(n^{\prime},s)(F)=1$. We prove by induction on the derivation of $n\xrightarrow{\;\tau\;}n^{\prime}$ that $\delta^{*}(n,s)(F)=1$:

**Case $n\xrightarrow{\;\tau\;}n^{\prime}$ was derived by rule mRecF or mRecB:: **

Then either $n=p_{x}$ and $n=m_{x}$, or $n=x$ and $n^{\prime}=p_{x}$. Let $S=\{n^{\prime\prime}\mid\delta^{*}(n^{\prime\prime},r)(F)=1\}$. Since $\delta^{*}(n^{\prime},s)(F)=1$, by the definition of $\delta^{*}$, we have that $\delta(n^{\prime},\alpha)(S)=\delta^{*}(n^{\prime},s)(F)=1,$ and therefore, by the closure conditions of $\delta$, we can conclude that $\delta^{*}(n,s)(F)=\delta(n,\alpha)(S)=1.$

**Case $n\xrightarrow{\;\tau\;}n^{\prime}$ was derived by mTauL, mVrE, mVrC1, mVrC2, mVrD1, or mVrD2:: **

Then we are in the case of $n=n_{1}{\odot}n_{2}$, which was handled above.

**Case $n\xrightarrow{\;\tau\;}n^{\prime}$ was derived by rule mSelL or mSelR:: **

Then $n=n_{1}+n_{2}$ and $n_{1}\xrightarrow{\;\tau\;}n^{\prime}$ or $n_{2}\xrightarrow{\;\tau\;}n^{\prime}$. By the inductive hypothesis (for the derivation of $n\xrightarrow{\;\tau\;}n^{\prime}$), $\delta^{*}(n_{1},s)(F)=1$ or $\delta^{*}(n_{2},s)(F)=1$, and similarly to the previous cases, from the closure conditions of $\delta$, $\delta^{*}(n,s)(F)=1$.

**Final case $e=\alpha f$ and $s=\alpha r$,: **

where $r$ agrees with $f$ on the external actions: Then $n\xrightarrow{\;\alpha\;}n^{\prime}$ for some $n^{\prime}\xrightarrow{\;r\;}\textsf{yes}$. By the inductive hypothesis, $\delta^{*}(n^{\prime},r)(F)=1$. By the definition of $\delta^{*}$, we have that $\delta^{*}(n,\alpha r)(F)=\delta(n,\alpha)(S)$, where $S=\{q\in Q\mid\delta^{*}(q,r)(F)=1\}$. We observe that $n^{\prime}\in S$. We now prove, by induction on the derivation of $n\xrightarrow{\;\alpha\;}n^{\prime}$ from the rules of Figs. 2 and 3, that $\delta^{*}(n,\alpha r)(F)=1$, or, equivalently, that $\delta(n,\alpha)(S)=1$.

**The base case is that $n\xrightarrow{\;\alpha\;}n^{\prime}$ is produced by rule mAct or mVerd:: **

Then, $n=n^{\prime}=\textsf{yes}$ or $n=\alpha.n^{\prime}$. If $n=\textsf{yes}$, then $n\in F$, and by the definition of $\delta_{0}$, we have that $\delta(n,\alpha)(S)=1$. If $n=\alpha.n^{\prime}$, then, since $n^{\prime}\in S$, by the first closure condition, we infer that $\delta(n,\alpha)(S)=1$.

**Case $n\xrightarrow{\;\alpha\;}n^{\prime}$ is produced by rule mSeL or mSeR:: **

Then the argument is similar to the analogous case for $n\xrightarrow{\;\tau\;}n^{\prime}$ above.

**Case $n\xrightarrow{\;\alpha\;}n^{\prime}$ is produced by rule mPar:: **

Then $n=n_{1}{\odot}n_{2}$, which has been handled above.

For the other direction,

we prove that for every immediate submonitor $n$ of a reactive submonitor $m^{\prime}$, if $\delta^{*}(n,s)(F)=1$, then $n$ accepts $s$. Since $m$ is reactive, this is enough to complete the proof. We prove that $n$ accepts $s$, by induction on $s$.

**Case $\delta^{*}(n,\varepsilon)(F)=1$:: **

Then $n\in F$, and thus, $n$ accepts $\varepsilon$.

**Case $\delta^{*}(n,\alpha r)(F)=1$:: **

Then $\delta(n,\alpha)(S)=1$, where $S=\{n^{\prime}\mid\delta^{*}(n^{\prime},r)(F)=1\}$. Therefore, either $\delta_{0}(n,\alpha)(S)=1$, or $\delta(n,\alpha)(S)=1$ can be derived from the closure conditions for $\delta$; therefore, we can use induction on this derivation of $\delta(n,\alpha)(S)=1$. We observe that, from the inductive hypothesis, for every $n^{\prime}\in S$, $n^{\prime}$ accepts $r$. By Claim 4, for every reactive $n^{\prime}\in S^{+}$, $n^{\prime}$ accepts $r$.

**The base case is $\delta_{0}(n,\alpha)(S)=1$:: **

In this case $n\in F$, and thus, $n$ accepts $\varepsilon$ and all its extensions, including $s$.

**Case $n=\alpha.n^{\prime}$, where $n^{\prime}\in S$:: **

Then $n\xrightarrow{\;\alpha\;}n^{\prime}$ and $n^{\prime}$ accepts $r$; by Lemma A.17, $n^{\prime}$ is reactive, therefore, by the inductive hypothesis, $n^{\prime}$ accepts $r$, and so $n$ accepts $s$.

**Case $n=n_{1}+n_{2}$, where $\delta(n_{1},\alpha)(S)=1$ or $\delta(n_{2},\alpha)(S)=1$,: **

then $n_{1},n_{2}$ are also immediate submonitors of $m^{\prime}$, so by the inductive hypothesis, $n_{1}\xRightarrow{\;\alpha r\;}\textsf{yes}$ or $n_{2}\xRightarrow{\;\alpha r\;}\textsf{yes}$, and by Lemma A.5, $n\xRightarrow{\;\alpha r\;}\textsf{yes}$.

**Case $n=x$ or $n=p_{x}$ and $\delta(m_{x},\alpha)(S)=1$:: **

Then in either case, since $x\xrightarrow{\;\tau\;}p_{x}\xrightarrow{\;\tau\;}m_{x}$, by Lemma A.17, $m_{x}$ is reactive, and therefore by the inductive hypothesis, $m_{x}\xRightarrow{\;\alpha r\;}\textsf{yes}$, but $x\xrightarrow{\;\tau\;}p_{x}\xrightarrow{\;\tau\;}m_{x}\xRightarrow{\;\alpha r\;}\textsf{yes}$, and the proof is thus complete.

**Case $n=m_{1}{\oplus}m_{2}$, where $\delta(n_{1},\alpha)(S)=1$ or $\delta(n_{2},\alpha)(S)=1$, and $m_{1}\xRightarrow{\;\alpha\;}$ and $m_{2}\xRightarrow{\;\alpha\;}$:: **

Then by Claim 1 and rule mPar, there is some $m_{1}{\oplus}m_{2}\xRightarrow{\;\alpha\;}m_{1}^{\prime}{\oplus}m_{2}^{\prime}$, where $m_{1}^{\prime}\in S^{+}$ or $m_{2}^{\prime}\in S^{+}$ — therefore, also $m_{1}^{\prime}{\oplus}m_{2}^{\prime}\in S^{+}$. By Lemma A.17, $m_{1}^{\prime}{\oplus}m_{2}^{\prime}$ is reactive. Hence, from the observation above about $S$ and $S^{+}$, $m_{1}^{\prime}{\oplus}m_{2}^{\prime}$ accepts $r$, and thus $m_{1}{\oplus}m_{2}$ accepts $s$.

**The case for $n=m_{1}{\oplus}m_{2}$: **

is similar. ∎

Appendix B Linear-Time Monitorability

We now present the omitted proofs of Sec. 4.

B.1. Complete Monitoring

• Proposition 4.1

If $m$ is sound and complete for $\varphi$ then

1. (1)

$m\simeq_{\text{ver}}n$* implies $n$ is sound and complete for $\varphi$.* 2. (2)

$m$* is a sound and complete monitor for $\varphi^{\prime}$ implies $\llbracket\varphi\rrbracket_{\textsc{L}}=\llbracket\varphi^{\prime}\rrbracket_{\textsc{L}}$*

Proof.

For the first clause, we need to prove soundness and completeness for $n$.

For soundness, Def. 4.1, assume $\textbf{rej}(n,t)$, i.e., $\exists\;p,s\cdot\textbf{rej}(n,p,s)$ and $s$ is a prefix of $t$. By Def. 3.3 and Lem. 3.3, it follows that $n\xRightarrow{\;s\;}\textsf{no}$. By $m\simeq_{\text{ver}}n$ we know that $m\xRightarrow{\;s\;}\textsf{no}$ which, in turn, implies that $\textbf{rej}(m,t)$. Since $m$ is sound (and complete) for $\varphi$, it must be the case that $t\not\in\llbracket\varphi\rrbracket$, which is the result we want. The case for $\textbf{acc}(n,t)$ is analogous.

The argument for completeness, Def. 4.1, is similar. Pick a trace $t\in\llbracket\varphi\rrbracket$. Since $m$ is complete for $\varphi$, we prove that $\textbf{acc}(m,t)$. Using the fact that $m\simeq_{\text{ver}}n$, Def. 3.3 and Lem. 3.3, we can then deduce that $\textbf{acc}(n,t)$ which is the required result. The case for $t\not\in\llbracket\varphi\rrbracket$ is analogous.

For the second clause, pick a $t\in\llbracket\varphi\rrbracket_{\textsc{L}}$ without loss of generality. By completeness, Def. 4.1, $\textbf{acc}(m,t)$, and by soundness, Def. 4.1, $t\in\llbracket\varphi^{\prime}\rrbracket_{\textsc{L}}$. ∎

We now present the proof demonstrating the complete-monitorability of the syntactic fragment HML from Def. 4.3. To prove Prop. 4.3, we first show that all the synthesised monitors $\textsf{m}(\varphi)$ are reactive, as defined in Def. 3.4.

• Lemma 4.2.

For all $\varphi\in\textsc{HML}$, $\textsf{m}(\varphi)$ is reactive.

Proof.

The proof proceeds by structural induction on $\varphi$. The cases for $\mathsf{tt}$,$\mathsf{ff}$,$\mathbf{\langle}A\mathbf{\rangle}\psi$ and $\mathbf{[}A\mathbf{]}\psi$ are immediate. For the case of $\psi_{1}\mathbf{\wedge}\psi_{2}$, we know from Def. 4.4 that $\textsf{m}(\psi_{1}\mathbf{\wedge}\psi_{2})=\textsf{m}(\psi_{1}){\otimes}\textsf{m}(\psi_{2})$. By the inductive hypothesis we know that both $\textsf{m}(\psi_{1})$ and $\textsf{m}(\psi_{2})$ are reactive and, by mPar of Fig. 3, it follows that $\textsf{m}(\psi_{1}){\otimes}\textsf{m}(\psi_{2})$ is reactive as well. The case for $\psi_{1}\mathbf{\vee}\psi_{2}$ is analogous. ∎

• Proposition 4.3

For all $\varphi\in\textsc{HML}$, $\textsf{m}(\varphi)$ is a sound and complete monitor for $\varphi$.

Proof.

For soundness, Def. 4.1, we need to show that $(i)$ $\textbf{rej}(\textsf{m}(\varphi),t)$ implies $t\not\in\llbracket\varphi\rrbracket$ and $(ii)$ $\textbf{acc}(\textsf{m}(\varphi),t)$ implies $t\in\llbracket\varphi\rrbracket$. We proceed by structural induction on $\varphi$, and the main cases are:

**Case $\varphi_{1}\mathbf{\wedge}\varphi_{2}$ and $\varphi_{1}\mathbf{\vee}\varphi_{2}$:: **

By Def. 4.4 we know that $\textsf{m}(\varphi_{1}\mathbf{\wedge}\varphi_{2})=\textsf{m}(\varphi_{1}){\otimes}\textsf{m}(\varphi_{2})$. If $\textbf{rej}(\textsf{m}(\varphi_{1}){\otimes}\textsf{m}(\varphi_{2}),t)$, by Def. 3.3, there exist $p,s$ such that $s$ is a prefix of $t$ and $\textbf{rej}(\textsf{m}(\varphi_{1}){\otimes}\textsf{m}(\varphi_{2}),p,s)$. Using Def. 3.3 and Lem. 3.3 we know that $(\textsf{m}(\varphi_{1}){\otimes}\textsf{m}(\varphi_{2}))\triangleleft\,p\xRightarrow{\;s\;}\textsf{no}\triangleleft\,p^{\prime}$ for some $p^{\prime}$. By Lem. A.5, this implies that either $\textsf{m}(\varphi_{1})\triangleleft\,p\xRightarrow{\;s\;}\textsf{no}\triangleleft\,p^{\prime}$ or $\textsf{m}(\varphi_{2})\triangleleft\,p\xRightarrow{\;s\;}\textsf{no}\triangleleft\,p^{\prime}$, which means that either $\textbf{rej}(\textsf{m}(\varphi_{1}),t)$ or $\textbf{rej}(\textsf{m}(\varphi_{2}),t)$. By the I.H., we deduce that either $t\not\in\llbracket\varphi_{1}\rrbracket$ or $t\not\in\llbracket\varphi_{2}\rrbracket$ which is enough to conclude that $t\not\in\llbracket\varphi_{1}\mathbf{\wedge}\varphi_{2}\rrbracket$. If $\textbf{acc}(\textsf{m}(\varphi_{1}){\otimes}\textsf{m}(\varphi_{2}),t)$, then by Def. 3.3, Lems. 3.3 and A.5 and the I.H. we obtain $t\in\llbracket\varphi_{1}\rrbracket$ and $t\in\llbracket\varphi_{2}\rrbracket$, and therefore we conclude $t\in\llbracket\varphi_{1}\mathbf{\wedge}\varphi_{2}\rrbracket$. The case for $\varphi_{1}\mathbf{\vee}\varphi_{2}$ is analogous.

**Case $\mathbf{[}A\mathbf{]}\varphi$ and $\mathbf{\langle}A\mathbf{\rangle}\varphi$:: **

In the case of $\mathbf{[}A\mathbf{]}\varphi$, by Def. 4.4 we know that $\textsf{m}(\mathbf{[}A\mathbf{]}\varphi)=A.{\textsf{m}(\varphi)}+\overline{A}\textsf{.}\textsf{yes}$. If $\textbf{rej}(A.{\textsf{m}(\varphi)}+\overline{A}\textsf{.}\textsf{yes},t)$ then there exist $p,s$ such that $s$ is a prefix of $t$ and $\textbf{rej}(A.{\textsf{m}(\varphi)}+\overline{A}\textsf{.}\textsf{yes},p,s)$. From Defs. 3.3 and 3.3 we know that $A.{\textsf{m}(\varphi)}+\overline{A}\textsf{.}\textsf{yes}\xRightarrow{\;s\;}\textsf{no}$ and, from the structure of the monitor and Lem. A.5, it must be the case that $A.{\textsf{m}(\varphi)}\xRightarrow{\;s\;}\textsf{no}$. This means that $s=\alpha r$ where $\alpha\in A$ and $\textsf{m}(\varphi)\xRightarrow{\;r\;}\textsf{no}$, which in turn implies that $t=\alpha u$ and $\textbf{rej}(\textsf{m}(\varphi),u)$. By the I.H., $\textbf{rej}(\textsf{m}(\varphi),u)$ implies that $u\not\in\llbracket\varphi\rrbracket$ which suffices to conclude that $t=\alpha u\not\in\llbracket\mathbf{[}A\mathbf{]}\varphi\rrbracket$. If $\textbf{acc}(A.{\textsf{m}(\varphi)}+\overline{A}\textsf{.}\textsf{yes},t)$, then by Def. 3.3, Lems. 3.3 and A.5 we know that either $A.{\textsf{m}(\varphi)}\xRightarrow{\;s\;}\textsf{yes}$ or $\overline{A}\textsf{.}\textsf{yes}\xRightarrow{\;s\;}\textsf{yes}$ for some $s$ is a prefix of $t$. In the latter case, we deduce that $t=\alpha u$ for some $\alpha,u$ where $\alpha\not\in A$, which trivially implies that $t\in\llbracket\mathbf{[}A\mathbf{]}\varphi\rrbracket$. In the former case, we know that $t=\alpha u$ for some $\alpha,u$ where $\alpha\in A$ and $\textbf{acc}(\textsf{m}(\varphi),u)$ which, by the I.H., implies that $u\in\llbracket\varphi\rrbracket$ and hence $t\in\llbracket\mathbf{[}A\mathbf{]}\varphi\rrbracket$. The case for $\mathbf{\langle}A\mathbf{\rangle}\varphi$ is similar.

For completeness, Def. 4.1, we need to show that $(i)$ violation-completeness, i.e., $t\not\in\llbracket\varphi\rrbracket$ implies $\textbf{rej}(\textsf{m}(\varphi),t)$ and $(ii)$ satisfaction-completeness, i.e., $t\in\llbracket\varphi\rrbracket$ implies $\textbf{acc}(\textsf{m}(\varphi),t)$. Again, we proceed by structural induction on $\varphi$, and the main cases are:

**Case $\varphi_{1}\mathbf{\wedge}\varphi_{2}$ and $\varphi_{1}\mathbf{\vee}\varphi_{2}$:: **

If $t\not\in\llbracket\varphi_{1}\mathbf{\wedge}\varphi_{2}\rrbracket$, then $t\not\in\llbracket\varphi_{1}\rrbracket$ or $t\not\in\llbracket\varphi_{2}\rrbracket$. Without loss of generality, assume the former, i.e., $t\not\in\llbracket\varphi_{1}\rrbracket$. By the I.H., we have $\textbf{rej}(\textsf{m}(\varphi_{1}),t)$ which, by Defs. 3.3 and 3.3 means that there exists a prefix $s$of $t$such that $\textsf{m}(\varphi_{1})\xRightarrow{\;s\;}\textsf{no}$. Since, $\textsf{m}(\varphi_{1}\mathbf{\wedge}\varphi_{2})=\textsf{m}(\varphi_{1}){\otimes}\textsf{m}(\varphi_{2})$, by Lem. A.5, we conclude that $\textbf{rej}(\textsf{m}(\varphi_{1}\mathbf{\wedge}\varphi_{2}),t)$. The proof for $t\in\llbracket\varphi_{1}\mathbf{\wedge}\varphi_{2}\rrbracket$ follows a similar structure, using the fact that both $t\in\llbracket\varphi_{1}\rrbracket$ or $t\in\llbracket\varphi_{2}\rrbracket$. The case for $\varphi_{1}\mathbf{\vee}\varphi_{2}$ is analogous.

**Case $\mathbf{[}A\mathbf{]}\varphi$ and $\mathbf{\langle}A\mathbf{\rangle}\varphi$:: **

If $t\not\in\llbracket\mathbf{[}A\mathbf{]}\varphi\rrbracket$ then, by Fig. 1, it must be the case that $t=\alpha u$ for some $\alpha\in A$ and $u\not\in\llbracket\varphi\rrbracket$. By the I.H., we know that $\textbf{rej}(\textsf{m}(\varphi),u)$, from which one can then conclude that $\textbf{rej}(A.{\textsf{m}(\varphi)}+\overline{A}\textsf{.}\textsf{yes},t)$ where $\textsf{m}(\mathbf{[}A\mathbf{]}\varphi)=A.{\textsf{m}(\varphi)}+\overline{A}\textsf{.}\textsf{yes}$, via Lems. 3.3 and A.5. If $t\in\llbracket\mathbf{[}A\mathbf{]}\varphi\rrbracket$ then, by Fig. 1, it must be one of two cases. Either $t=\alpha u$ where $\alpha\not\in A$, which implies that $\textbf{acc}(\textsf{m}(\mathbf{[}A\mathbf{]}\varphi),t)$, since $\textsf{m}(\mathbf{[}A\mathbf{]}\varphi)=A.{\textsf{m}(\varphi)}+\overline{A}\textsf{.}\textsf{yes}$. Else $t=\alpha u$ where $\alpha\in A$ and $u\in\llbracket\varphi\rrbracket$. By I.H., we deduce that $\textbf{acc}(\textsf{m}(\varphi),u)$, and by Lems. 3.3 and A.5 we are able to construct an acceptance computation for $A.{\textsf{m}(\varphi)}+\overline{A}\textsf{.}\textsf{yes}$, hence $\textbf{acc}(\textsf{m}(\mathbf{[}A\mathbf{]}\varphi),t)$. The case for $\mathbf{\langle}A\mathbf{\rangle}\varphi$ is similar. ∎

We now procede to give the proof for the maximality of HML from Def. 4.3. The following are technical lemmata leading up to Lem. 4.5.

Lemma B.1**.**

For each $m\in\textsc{RMon}$:

1. (1)

If $m$ is a syntactically deterministic monitor, then $\textsf{noR}(m)$ is also syntactically deterministic. 2. (2)

If $m$ is a reactive and syntactically deterministic monitor, then $\textsf{noR}(m)$ is also reactive.

Proof.

By structural induction on $m$. ∎

Lemma B.2**.**

Suppose that the syntactically deterministic monitor $\textsf{rec}\,x.m$ is sound and complete for some formula $\varphi$ and that $\textsf{rec}\,x.m\xRightarrow{\;s\;}v$ for some finite trace $s$. Then $m\xRightarrow{\;s\;}v$.

Proof.

From \textsf{rec}\,x.m\xrightarrow{\;\tau\;}m[\raisebox{2.15277pt}{\small\textsf{rec},x.m}\!/\!\mbox{\smallx}]\xRightarrow{\;s\;}v and Lem. A.3 we have the following two cases to consider.

1. (1)

Assume that there exists some $m^{\prime}$ such that $m\xRightarrow{\;s\;}m^{\prime}$ and m^{\prime}[\raisebox{2.15277pt}{\small\textsf{rec},x.m}\!/\!\mbox{\smallx}]=v. This immediately yields the claim, since m^{\prime}[\raisebox{2.15277pt}{\small\textsf{rec},x.m}\!/\!\mbox{\smallx}]=v can only hold if $m^{\prime}=v$. 2. (2)

Assume that there exist $s_{1},s_{2}$ and $m^{\prime}$ where $s=s_{1}s_{2}$ (and $s_{2}\neq\epsilon$) and $m\xRightarrow{\;s_{1}\;}m^{\prime}=x$ (because $\textsf{rec}\,x.m$ is syntactically deterministic) and $\textsf{rec}\,x.m\xRightarrow{\;s_{2}\;}v$. Stated otherwise, we have

[TABLE]

We show that we can reach a contradiction, and therefore this case cannot occur.

If $s_{1}=\varepsilon$, then for some $k>0$ $\textsf{rec}\,x.m(\xrightarrow{\;\tau\;})^{k}\textsf{rec}\,x.m$, and therefore for all $k>0$, $\textsf{rec}\,x.m(\xrightarrow{\;\tau\;})^{k}$. By Lem. B.5, we then have that for all $n$, if $m\xRightarrow{\;\;}n$ then $\forall\alpha\cdot n\centernot{\xrightarrow{\;\alpha\;}}$, and therefore $s_{2}=\varepsilon$, which is a contradiction. Therefore, $s_{1}$ must be non-empty.

Consider the trace $s_{1}^{\omega}$. We must have either $s_{1}^{\omega}\in\llbracket\varphi\rrbracket_{\textsc{L}}$ or $s_{1}^{\omega}\not\in\llbracket\varphi\rrbracket_{\textsc{L}}$; without loss of generality, assume the former. Since $\textsf{rec}\,x.m$ is sound and complete for $\varphi$, $\textsf{rec}\,x.m\xrightarrow[]{\;e\;}\mathrel{\mkern-14.0mu}\rightarrow\textsf{yes}$ for some $e\neq\varepsilon$ where $\lceil e\rceil$ is a prefix of $s_{1}$. By Lem. 3.1, this yields that $\textsf{rec}\,x.m\xRightarrow{\;s_{1}\;}\textsf{yes}$, and by Lem. 3.9, it must be the case that $\textsf{rec}\,x.m\simeq_{\text{ver}}\textsf{yes}$, and therefore $\textsf{rec}\,x.m\xRightarrow{\;\;}\textsf{yes}$, and by Cor. B.8, $x=\textsf{yes}$, which is also a contradiction. ∎

• Lemma 4.5.

If $m$ is a syntactically deterministic monitor that is sound and complete $\varphi$, then $\textsf{noR}(m)$ is also a sound and complete monitor for $\varphi$.

Proof.

Using Prop. 4.1, the required result follows if we can show that $m\simeq_{\text{ver}}\textsf{noR}(m)$.

In one direction, we have to show that, for $v\in\left\{\textsf{yes},\textsf{no}\right\}$, $\textsf{noR}(m)\xRightarrow{\;s\;}v$ implies $m\xRightarrow{\;s\;}v$. We proceed by structural induction on the string $e$ where $\textsf{noR}(m)\xrightarrow[]{\;e\;}\mathrel{\mkern-14.0mu}\rightarrow v$ and $\lceil e\rceil=s$.

**Case $e=\varepsilon$:: **

$\textsf{noR}(m)=v$ which implies that $m=\textsf{rec}\,x_{1}.\cdots\textsf{rec}\,x_{n}.v$ by Def. 4.5. We therefore obtain $m\xrightarrow[]{\;{\tau^{n}}\;}\mathrel{\mkern-14.0mu}\rightarrow v$, since $\lceil{\tau^{n}}\rceil=\lceil\varepsilon\rceil=\varepsilon$.

**Case $e=\mu e^{\prime}$:: **

By Lem. B.1(1) and Def. 4.5, since $\textsf{noR}(m)$ is a syntactically deterministic regular monitor and it does not contain any recursion, $\mu=\alpha$ for some $\alpha\in\textsc{Act}$. Thus we know that $s=\alpha r$ for some $r$. There are three subcases to consider.

**Case $\textsf{noR}(m)=\textsf{no}$ or $\textsf{noR}(m)=\textsf{yes}$:: **

The proof is analogous to that of the base case.

**Case $\textsf{noR}(m)=\textsf{end}$:: **

By Lem. 3.1, this would contradict $\textsf{noR}(m)\xrightarrow[]{\;e\;}\mathrel{\mkern-14.0mu}\rightarrow v$ for $v\in\left\{\textsf{yes},\textsf{no}\right\}$.

**Case $\textsf{noR}(m)=\sum_{\alpha\in A}\alpha.{m_{\alpha}}$:: **

From the structure of the monitor $\textsf{noR}(m)$, we deduce that

[TABLE]

Again, from the structure the monitor $\textsf{noR}(m)$ and the fact that $m$ is syntactically deterministic (Def. 3.8), we use Def. 4.5 to conclude that

[TABLE]

Now, from Eq. 12, we can derive $m\xrightarrow[]{\;{\tau^{n}\alpha}\;}\mathrel{\mkern-14.0mu}\rightarrow n_{\alpha}$ where, clearly, $\lceil\tau^{n}\alpha\rceil=\alpha$. By Eq. 13, $m_{\alpha}\xrightarrow[]{\;e^{\prime}\;}\mathrel{\mkern-14.0mu}\rightarrow v$ of Eq. 11 and the inductive hypothesis we obtain that $n_{\alpha}\xRightarrow{\;r\;}v$. Thus, we deduce that $m\xRightarrow{\;\alpha r\;}v$ as required.

For the other direction, we have to show that, for $v\in\left\{\textsf{yes},\textsf{no}\right\}$, $m\xRightarrow{\;s\;}v$ implies $\textsf{noR}(m)\xRightarrow{\;s\;}v$. Again, we proceed by structural induction on $e$ where $m\xrightarrow[]{\;e\;}\mathrel{\mkern-14.0mu}\rightarrow v$ and $\lceil e\rceil=s$.

**Case $e=\varepsilon$:: **

Trivially true, since $m=v$ implies that $\textsf{noR}(m)=v$ by Def. 4.5.

**Case $e=\mu e^{\prime}$:: **

We have two subcases to consider:

**Case $\mu=\tau$:: **

By Def. 3.8 we know that $m=\textsf{rec}\,x.n$ for some $n$. By Lem. B.2, we deduce that $n\xRightarrow{\;s\;}v$. By the inductive hypothesis we obtain $\textsf{noR}(n)\xRightarrow{\;s\;}v$. The required results follows by Def. 4.5, since $\textsf{noR}(m)=\textsf{noR}(\textsf{rec}\,x.n)=\textsf{noR}(n)$, and thus $\textsf{noR}(m)\xRightarrow{\;s\;}v$.

**Case $\mu=\alpha$:: **

By Def. 3.8 we deduce that $m=\sum_{\alpha\in A}\alpha.{m_{\alpha}}$ where $m_{\alpha}\xrightarrow[]{\;e^{\prime}\;}\mathrel{\mkern-14.0mu}\rightarrow v$. By Def. 4.5 we know that $\textsf{noR}(m)=\sum_{\alpha\in A}\alpha.{\textsf{noR}(m_{\alpha})}$, where we can derive $\sum_{\alpha\in A}\alpha.{\textsf{noR}(m_{\alpha})}\xrightarrow{\;\alpha\;}\textsf{noR}(m_{\alpha})$. The required result follows from $m_{\alpha}\xrightarrow[]{\;e^{\prime}\;}\mathrel{\mkern-14.0mu}\rightarrow v$ and the inductive hypothesis, from which we obtain $\textsf{noR}(m_{\alpha})\xRightarrow{\;r\;}v$ where $\lceil e^{\prime}\rceil=r$ and $\alpha r=s$. ∎

The following lemmata relate to properties of the formula synthesis function of Def. 4.7.

Corollary B.3**.**

For any $m\in\textsc{FMon}$, $\textsf{f}(m)\in\textsc{HML}$ ∎

• Lemma 4.6.

Any reactive monitor $m\in\textsc{FMon}$ is a sound and complete monitor for $\textsf{f}(m)$.

Proof.

We treat soudness and completeness spearately and proceed by induction on the structure of $m$. The main case is when $m=\sum_{\alpha\in\textsc{Act}}\alpha.{m_{\alpha}}$ where $\textsf{f}(m)=\bigwedge_{\alpha\in\textsc{Act}}\mathbf{[}\alpha\mathbf{]}\textsf{f}(m_{\alpha})$.

**Soundness:: **

Pick a $t$. From the structure of the monitor $m$, $\textbf{rej}(m,t)$ implies that $t=\alpha u$ for some $\alpha$ and $u$ where $\textbf{rej}(m_{\alpha},u)$. By the inductive hypothesis we know that $u\not\in\llbracket\textsf{f}(m_{\alpha})\rrbracket_{\textsc{L}}$ which implies that $t$ violates $\textsf{f}(m)$ since $t=\alpha u\not\in\llbracket\bigwedge_{\alpha\in\textsc{Act}}\mathbf{[}\alpha\mathbf{]}\textsf{f}(m_{\alpha})\rrbracket_{\textsc{L}}=\llbracket\textsf{f}(m)\rrbracket_{\textsc{L}}$. The argument for $\textbf{acc}(m,t)$ is analogous where we note that, since $t=\alpha u$, any subformula $\mathbf{[}\beta\mathbf{]}\textsf{f}(m_{\beta})$ where $\beta\neq\alpha$ is satisfied trivially by $t$.

**Completeness:: **

Pick a $t$; it must be of the form $t=\alpha u$ If $t\not\in\llbracket\bigwedge_{\alpha\in\textsc{Act}}\mathbf{[}\alpha\mathbf{]}\textsf{f}(m_{\alpha})\rrbracket_{\textsc{L}}$ then it must be because $u\not\in\llbracket\textsf{f}(m_{\alpha})\rrbracket_{\textsc{L}}$. By the inductive hypothesis, we obtain that $\textbf{rej}(m_{\alpha},u)$ which in turn implies that $\textbf{rej}(\sum_{\alpha\in\textsc{Act}}\alpha.{m_{\alpha}},\alpha t)$. The case for $t\in\llbracket\bigwedge_{\alpha\in\textsc{Act}}\mathbf{[}\alpha\mathbf{]}\textsf{f}(m_{\alpha})\rrbracket_{\textsc{L}}$ is analogous. ∎

Prop. 4.7 also makes use of the following technical lemma stating that a deterministic monitor that is complete with respect to some formula must necessarily be reactive.

Lemma B.4**.**

If $m$ is a deterministic complete monitor for some formula $\varphi$, then it must be reactive.

Proof.

Let $n\in\textsf{reach}(m)$ and let $\alpha\in\textsc{Act}$. By Def. 3.4, it suffices to prove that $n\xRightarrow{\;\alpha\;}$. Since, $n\in\textsf{reach}(m)$, there must be some $s\in\textsc{Act}^{*}$, such that $m\xRightarrow{\;s\;}n$. Let $t=s\alpha u$ for some $u$. Since $m$ is complete for $\varphi$, there is a verdict $v$ and a finite prefix $r$ of $t$, such that $m\xRightarrow{\;r\;}v$. If $r$ is a prefix of $s$, then by Lem. 3.1, $m\xRightarrow{\;s\;}v$, and therefore by Lem. 3.9, $n\xRightarrow{\;\;}v\xrightarrow{\;\alpha\;}v$. If $s\alpha$ is a prefix of $r$, then $r=s\alpha s^{\prime}$ for some $s^{\prime}$ and for some $m^{\prime}$, $m\xrightarrow{\;s\;}m^{\prime}\xrightarrow{\;\alpha s^{\prime}\;}v$. Therefore, by Lem. 3.9, $n\simeq_{\text{ver}}m^{\prime}$, so $n\xrightarrow{\;\alpha s^{\prime}\;}v$, yielding that $n\xRightarrow{\;\alpha\;}$. ∎

We are now in a position to give a proof of maximality for HML. We actually give two proofs: the first one is constructive as reported in Sec. 4.1, whereas the other one is stronger (albeit non-constructive) and shows that this expressivity result holds for any logic, not just recHML.

• Proposition 4.7

(Maximality for HML). * For any $\varphi\in\textsc{recHML}$ if $\varphi$ is complete-monitorable, then there exists $\psi\in\textsc{HML}$ such that $\llbracket\varphi\rrbracket_{\textsc{L}}=\llbracket\psi\rrbracket_{\textsc{L}}$.*

Proof.

Pick any $\varphi\in\textsc{recHML}$ that is complete-monitorable. By Def. 4.2, there exists a monitor $m$ that is sound and complete for $\varphi$. By Prop. 3.8 and Prop. 3.11, there exists a syntactically deterministic regular monitor $m^{\prime}$ that is verdict-equivalent to $m$. By Prop. 4.1, monitor $m^{\prime}$ is also sound and complete for $\varphi$. Moreover, by Lem. B.4, monitor $m^{\prime}$ must also be reactive. By Lem. 4.5 and Lem. B.1, there exists a reactive recursion-free deterministic regular monitor $m^{\prime\prime}\in\textsc{FMon}$ that is verdict-equivalent to $m^{\prime}$. Again, by Prop. 4.1, monitor $m^{\prime\prime}$ is also sound and complete for $\varphi$.

Now, by Lem. 4.6, $m^{\prime\prime}$ is sound and complete for $\textsf{f}(m^{\prime\prime})$ as well. By Cor. B.3, we know that $\textsf{f}(m^{\prime\prime})\in\textsc{HML}$. Thus, by Prop. 4.1 we conclude that $\llbracket\varphi\rrbracket_{\textsc{L}}=\llbracket\textsf{f}(m^{\prime\prime})\rrbracket_{\textsc{L}}$ as required. ∎

Remark*.*

The proof of Prop. 4.7 is constructive. We are able to prove (albeit in a non-constructive manner) an even stronger result with respect to complete monitoring for an arbitrary logic that is defined over traces. This increases the importance of the logic identified in Def. 4.3 with the linear-time interpretation of Fig. 1. $\hfill\qed$

• Theorem 4.8

Let $m$ be a monitor from a monitoring system with the following two properties:

1. (1)

verdicts are irrevocable, that is, if $m$ accepts (respectively, rejects) a finite trace $s$, then it accepts (respectively, rejects) all its extensions, and 2. (2)

$m$* accepts (respectively, rejects) a trace $t$ if, and only if, it accepts (respectively, rejects) some finite prefix $s$ of $t$.*

For any property $\varphi$ with a trace interpretation (not necessarily syntactically represented using recHML), if $m$ is sound and complete for $\varphi$ then $\varphi$ can be expressed via the syntactic fragment HML of Def. 4.3.

Proof.

A monitor, irrespective of its syntactic structure, is a computational entity that reaches a verdict after a finite sequence of observations/actions: at this point verdicts are irrevocable meaning that further actions observed would not change the status of the monitor.

Let $m$ be such a monitor that is sound and complete for $\varphi$. Let $L_{a}(m)=\{s\in\textsc{Act}^{*}\mid m$ accepts $s\}$ and $L_{r}(m)=\{s\in\textsc{Act}^{*}\mid m$ rejects $s\}$. Due to soundness, $L_{a}(m)\cap L_{r}(m)=\emptyset$. Now, let

[TABLE]

We observe that both $L_{a}(m)$ and $L_{r}(m)$ are suffix-closed, meaning that if a finite trace is in $L_{a}(m)$ or $L_{r}(m)$, then so are all of its finite extensions. Therefore, $L_{a}(m)=\{sr\in\textsc{Act}^{*}\mid s\in L_{a}(m)\}$ and $L_{r}(m)=\{sr\in\textsc{Act}^{*}\mid s\in L_{r}(m)\}$. We can define $s.n$ recursively thus: $\varepsilon.n=n$ and $\alpha s.n=\alpha.(s.n)$. If both $\min L_{a}(m)$ and $\min L_{r}(m)$ are finite, then we can define regular monitor

[TABLE]

and it is not hard to see that $n$ accepts and rejects exactly the same traces as $m$: if $m$ rejects $t$, then it rejects a finite prefix $s$ of $t$, so $s\in L_{r}(m)$, and therefore $s=rr^{\prime}$ for some $r\in\min L_{r}(m)$, which is then rejected by $n$. The other direction and the case for acceptance are similar.

Therefore, it suffices to prove that $\min L_{a}(m)\cup\min L_{r}(m)$ is finite. If $\varepsilon\in\min L_{a}(m)\cup\min L_{r}(m)$, then we can immediately see that $\min L_{a}(m)\cup\min L_{r}(m)=\{\varepsilon\}$, which is a finite set. Otherwise, let $L^{\prime}=\{s\mid\exists\alpha\in\textsc{Act}.~{}s\alpha\in\min L_{a}(m)\cup\min L_{r}(m)\}$. We can observe that $m$ can neither accept nor reject $s\in L^{\prime}$, because otherwise, without loss of generality, $s\in L_{a}(m)$, so if $s\alpha\in\min L_{a}(m)$, then $s\alpha$ is not minimal in $L_{a}(m)$ and we have a contradiction, while if $s\alpha\in\min L_{r}(m)$, then $s\alpha\in L_{a}(m)\cap L_{r}(m)$, which is also a contradiction. Therefore $L^{\prime}\subseteq L$, where $L\subseteq\textsc{Act}^{*}$ is the set of finite traces that $m$ does not accept or reject. Therefore, it suffices to prove that $L$ is finite, which we proceed to do.

To reach a contradiction, we assume that $L$ is infinite. Let $T=(L,\longrightarrow,\textsc{Act})$ be the tree-LTS where for every $\alpha\in\textsc{Act}$ and all $s,r$, $s\xrightarrow{\;\alpha\;}r$ if and only if $r=s\alpha$. As we have established above, $m$ does not accept or reject $\varepsilon$, therefore $\varepsilon\in L$. It is not hard to see that for every $s,r\in\textsc{Act}^{*}$, if $\varepsilon\xrightarrow{\;s\;}r$, then $s=r$, by easy induction on $s$. Similarly, if $s\in L$, then $\varepsilon\xrightarrow{\;s\;}s$. Since Act is finite, $T$ is finitely-brancing, and therefore, by König’s Lemma, since $L$ is infinite, it must be the case that there is an infinite path (trace) $t$ in $T$ from $\varepsilon$. For every finite prefix $s$ of $t$, $\varepsilon\xrightarrow{\;s\;}s$, and therefore, $s\in L$. Therefore, $m$ neither accepts nor rejects $t$, which is a contradiction, because $m$ is complete for $\varphi$. ∎

Lemma B.5**.**

For any deterministic monitor $m$, if $m\xrightarrow{\;\tau\;}m_{1}$ and $m\xrightarrow{\;\mu\;}m_{2}$, then $\mu=\tau$ and $m_{1}=m_{2}$.

Proof.

From Def. 3.8, if $m\xrightarrow{\;\tau\;}$, then $m=\textsf{rec}\,x.n$ for some $n$, and thus the only transition $m$ can perform is $m\xrightarrow{\;\tau\;}n[m/X]$. ∎

Corollary B.6**.**

If $m$ is deterministic, and $m\xrightarrow[]{\;e\;}\mathrel{\mkern-14.0mu}\rightarrow m_{1}$ and $m\xrightarrow[]{\;e\;}\mathrel{\mkern-14.0mu}\rightarrow m_{2}$, then $m_{1}=m_{2}$. $\hfill\qed$

Corollary B.7**.**

If $m$ is deterministic and $m\xRightarrow{\;\;}v$, and $m\xRightarrow{\;\;}n\xrightarrow{\;\alpha\;}$, then $n=v$. $\hfill\qed$

Proof.

Let $k,k^{\prime}\geq 0$ be such that $m(\xrightarrow{\;\tau\;})^{k}v$ and $m(\xrightarrow{\;\tau\;})^{k^{\prime}}n.$ If $k^{\prime}<k$, then by Cor. B.6,

[TABLE]

But then, $n\xrightarrow{\;\tau\;}$ because $k-k^{\prime}\geq 1$ and $n\xrightarrow{\;\alpha\;}$ by our assumptions, and by Lem. B.5, $\tau=\alpha$, which is a contradiction. Therefore, $k\leq k^{\prime}$, and by Cor. B.6, $m\ (\xrightarrow{\;\tau\;})^{k}\ v\ (\xrightarrow{\;\tau\;})^{k^{\prime}-k}\ n$, and by Lem. 3.1, $n=v$. ∎

Corollary B.8**.**

If $m$ is deterministic and $m\xRightarrow{\;\;}v$, and $m\xRightarrow{\;s\;}n$, where $s\neq\varepsilon$, then $n=v$. $\hfill\qed$

Proof.

A consequence of Cors. B.7 and 3.1. ∎

B.2. The PSPACE-hardness of maxHML

Here we prove that satisfiability for maxHML is PSPACE-hard. The reduction that we use is from the one-variable, diamond-free fragment of $D\oplus_{\subseteq}K4$, which is PSPACE-complete (Achilleos, 2016).

$D\oplus_{\subseteq}K4$ is a modal logic with two modalities, $[1]$ and $[2]$, based on a serial transition relation $\xrightarrow{\;1\;}$ (i.e., $\forall x\exists y.x\xrightarrow{\;1\;}y$) and a transitive transition relation $\xrightarrow{\;2\;}$ (i.e., $\forall x,y,z.(x\xrightarrow{\;2\;}y\xrightarrow{\;2\;}z\Rightarrow x\xrightarrow{\;2\;}z)$), such that $\xrightarrow{\;1\;}\subseteq\xrightarrow{\;2\;}$. Given a set of propositional variables Prop, $D\oplus_{\subseteq}K4$ is interpreted over Kripke structures of the form $(W,(\xrightarrow{\alpha})_{\alpha\in\{1,2\}},V)$, where $W$ is a non-empty set of states, the transition relations satisfy the above-mentioned properties, and $V:W\to 2^{\textsf{Prop}}$ maps states to sets of propositional variables. Here, we focus on the one-variable, diamond-free fragment of $D\oplus_{\subseteq}K4$, and therefore $\textsf{Prop}=\{p\}$ and the syntax of the fragment is given by the following grammar:

[TABLE]

The semantics of $D\oplus_{\subseteq}K4$ is defined in terms of a satisfaction relation $\models$, where $M,w\models\varphi$ means that $\varphi$ is satisfied at state $w$ of $M$, in a similar way to the branching-time semantics $\llbracket-\rrbracket_{\textsc{B}}$ for recHML, with the additional condition that $M,w\models p$ if and only if $p\in V(w)$. Constants $\mathsf{tt},\mathsf{ff}$ can be either included to the syntax or constructed as $p\vee\neg p$ and $p\land\neg p$, respectively.

Let $\alpha,\beta\in\textsc{Act}$, where $\alpha\neq\beta$. We can define the mapping from formulae without diamond modalities and that use only one propositional variable $p$ that maps $\varphi$ to

[TABLE]

where $\varphi^{t}$ is such that $p^{t}=\mathbf{\langle}\beta\mathbf{\rangle}\mathsf{tt}$, it commutes with the boolean operators, and

[TABLE]

The construction of $trans(\varphi)$ ensures that it can only be satisfied by traces of the form $(\alpha+\beta\alpha)^{\omega}$. In such a trace, a following $\beta$ action marks the satisfaction of propositional variable $p$, so states-transitions are represented by $\alpha$ actions. As such, in the translation above, we use greatest fixed points (least fixed points would have worked too) to allow the modalities for $1$ to skip any occurrences of $\beta$ and only be affected by the occurrences of $\alpha$. The transition relation for $2$ can simply be the transitive closure of the one for $1$, and therefore in the translation, the $2$ modalities are allowed to skip any finite prefix and activate right after any $\alpha$ occurrence.

Lemma B.9**.**

For every formula $\varphi$ from the one-variable, diamond-free fragment of $D\oplus_{\subseteq}K4$, $\varphi$ is satisfiable if and only if $trans(\varphi)$ is satisfiable over Trc.

Proof.

Given a trace $t\in(\alpha+\beta\alpha)^{\omega}$, let $M_{t}=(W,(\xrightarrow{\alpha})_{\alpha\in\{1,2\}},V)$ be a Kripke structure, where $W$ is the set of finite prefixes of $t$ that do not end with $\beta$, $s\xrightarrow{\;1\;}r$ iff $r=s\alpha$ or $r=s\beta\alpha$, and $V(p)=\{s\in W\mid s\beta\alpha\in W\}$.

Given a Kripke structure $M=(W,(\xrightarrow{\alpha})_{\alpha\in\{1,2\}},V)$ and state $w\in W$, fix a path $w_{0}w_{1}w_{2}\cdots$ in $M$, where $w=w_{0}$; $t_{M,w}=s^{W,w}_{0}s^{W,w}_{1}s^{W,w}_{2}\cdots$, where if $w_{i}\in V(p)$, then $s^{W,w}_{i}=\beta\alpha$, and $s^{W,w}_{i}=\alpha$ otherwise.

It is not too hard to observe that the following hold for all $\varphi$ of $D\oplus_{\subseteq}K4$, $t$, $M$, and $w$:

1. (1)

$t\in\llbracket trans(\varphi)\rrbracket_{\textsc{L}}$ if and only if $t$ is of the form $(\alpha+\beta\alpha)^{\omega}$ and $t\in\llbracket\varphi^{t}\rrbracket_{\textsc{L}}$, by the definition of $trans(\varphi)$; 2. (2)

$M,w\models p$ if and only if $t_{M,w}\in\llbracket\mathbf{\langle}\beta\mathbf{\rangle}\mathsf{tt}\rrbracket_{\textsc{L}}$, by the construction of $t_{M,w}$; 3. (3)

$t\in(\alpha+\beta\alpha)^{\omega}\cap\llbracket\mathbf{\langle}\beta\mathbf{\rangle}\mathsf{tt}\rrbracket_{\textsc{L}}$ if and only if $M_{t},\varepsilon\models p$; 4. (4)

$M,w\models[1]\psi$ if and only if $t_{M,w}\in\llbracket\max X.([\beta]X\land[\alpha]\psi^{t})\rrbracket_{\textsc{L}}$; 5. (5)

$t\in(\alpha+\beta\alpha)^{\omega}\cap\llbracket\max X.([\beta]X\land[\alpha]\psi^{t})\rrbracket_{\textsc{L}}$ if and only if $M_{t},\varepsilon\models[1]\psi$; 6. (6)

$M,w\models[2]\psi$ if and only if $t_{M,w}\in\llbracket\max X.([\beta]X\land[\alpha]X\land[\alpha]\psi^{t})\rrbracket_{\textsc{L}}$; 7. (7)

$t\in(\alpha+\beta\alpha)^{\omega}\cap\llbracket\max X.([\beta]X\land[\alpha]X\land[\alpha]\psi^{t})\rrbracket_{\textsc{L}}$ if and only if $M_{t},\varepsilon\models[2]\psi$.

From these observations, it is not hard to conclude, by induction on $\varphi$, that for every $\varphi$ of $D\oplus_{\subseteq}K4$, if $M,w\models\varphi$, then $t_{M,w}\in\llbracket trans(\varphi)\rrbracket_{\textsc{L}}$. Furthermore, if $t\in\llbracket trans(\varphi)\rrbracket_{\textsc{L}}$, then by the first observation, $t\in(\alpha+\alpha\beta)^{\omega}$ and $t\in\llbracket\varphi^{t}\rrbracket_{\textsc{L}}$. Therefore, it suffices to prove that for all subformulae $\psi$ of $\varphi$ and $su=t$, where $s$ does not end with $\beta$, if $u\in\llbracket\psi^{t}\rrbracket_{\textsc{L}}$, then $M,s\models\psi$. This can be done by induction on $\psi$, using the observations above. ∎

Then, the PSPACE-hardness of maxHML follows as a corollary of Lemma B.9.

B.3. Tight Complete Monitoring

In the following, we use the notations $\bigodot_{\alpha\in A}m_{\alpha}$ and $m_{1}{\odot}\cdots{\odot}m_{i}{\odot}\cdots{\odot}m_{k}$ to denote a combination of monitors using the parallel operator ${\odot}$ since the particular way the monitors are combined does not matter. Furthermore, since we are dealing with reactive monitors—and, as a consequence of Prop. 3.6, the parallel operators are associative with respect to verdict-equivalence—any way we combine the monitors with ${\odot}$ will reach the same verdict for the same (finite) trace.

• Lemma 4.9.

If $\varphi\in\textsc{HML}$ is slim and $\llbracket\varphi\rrbracket_{\textsc{L}}=\emptyset$ (resp., $\llbracket\varphi\rrbracket_{\textsc{L}}=\textsc{Trc}$), then $\varphi=\mathsf{ff}$ (resp., $\varphi=\mathsf{tt}$).

Proof.

We prove the contrapositive statement, that if $\varphi\neq\mathsf{ff}$, then there is some $t\in\llbracket\varphi\rrbracket_{\textsc{L}}$. The proof is by induction on $\varphi$. The case for $\mathsf{tt}$ is immediate. If $\varphi\equiv\bigwedge_{\alpha\in A}\mathbf{[}\alpha\mathbf{]}\varphi_{\alpha}$, then we have two cases.

**Case $A=\textsc{Act}$:: **

Then there must be some $\alpha\in A$, such that $\varphi_{\alpha}\neq\mathsf{ff}$. By the inductive hypothesis, there is some $t\in\llbracket\varphi_{\alpha}\rrbracket_{\textsc{L}}$, and therefore, $\alpha t\in\llbracket\varphi\rrbracket_{\textsc{L}}$, which completes the proof.

**Case $A\neq\textsc{Act}$:: **

Then there is some $\alpha\notin A$, and therefore, $\alpha^{\omega}\in\llbracket\varphi\rrbracket_{\textsc{L}}$, which completes the proof.

If $\varphi\equiv\bigvee_{\alpha\in A}\mathbf{\langle}\alpha\mathbf{\rangle}\varphi_{\alpha}$, then $A\neq\emptyset$. Let $\alpha\in A$. Since $\varphi$ is slim, $\varphi_{\alpha}\neq\mathsf{ff}$ and by the inductive hypothesis there is some $t\in\llbracket\varphi_{\alpha}\rrbracket_{\textsc{L}}$. Therefore, $\alpha t\in\llbracket\varphi\rrbracket_{\textsc{L}}$, which completes the proof. ∎

• Lemma 4.10.

If $\varphi$ is a slim HML formula, then $m(\varphi)$ is tight.

Proof.

By Prop. 4.3, $t\notin\llbracket\varphi\rrbracket_{L}$ implies that there is a finite prefix $s$ of $t$ such that $m(\varphi)\xRightarrow{\;s\;}\textsf{no}$. We prove, by induction on $s$, that if $\forall t.\textbf{rej}(m,st)$, then $m\xRightarrow{\;s\;}\textsf{no}$ (the case for acceptance is symmetric). If $s=\varepsilon$, then by Lemma 4.3, for every trace $t$, $t\notin\llbracket\varphi\rrbracket_{L}$, thus by Lemma 4.9, $\varphi=\mathsf{ff}$, and therefore $m(\varphi)=\textsf{no}$. Since $\textsf{no}\xRightarrow{\;\;}\textsf{no}$, we are done. If $s=\beta r$, if $\varphi\neq\mathsf{tt},\mathsf{ff}$, then we have two cases:

• •

If $\varphi\equiv\bigwedge_{\alpha\in B}\mathbf{[}\alpha\mathbf{]}\varphi_{\alpha}$, then $\beta\in B$, $r\notin\llbracket\varphi_{\beta}\rrbracket_{L}$, and

[TABLE]

Therefore, using the inductive hypothesis and rule mVrC1,

[TABLE]

• •

If $\varphi\equiv\bigvee_{\alpha\in D}\mathbf{\langle}\alpha\mathbf{\rangle}\varphi_{\alpha}$, then

[TABLE]

If $\beta\notin D$, then $m(\varphi)\xrightarrow{\beta}\bigoplus_{\alpha\in D}\textsf{no}\Rightarrow\textsf{no}\xRightarrow{\;r\;}\textsf{no}$. If $\beta\in D$, then, using the inductive hypothesis and rule mVrD1,

[TABLE]

and the proof is complete. ∎

• Proposition 4.12

(HML normalisation). * For every formula $\varphi\in\textsc{HML}$, there exists $k\leq l(\varphi)$ such that $\varphi=\varphi_{0}\Rrightarrow_{L}\varphi_{1}\Rrightarrow_{L}\ldots\Rrightarrow_{L}\varphi_{k}=\psi$ where $\psi$ is slim and $\llbracket\varphi\rrbracket_{\textsc{L}}=\llbracket\psi\rrbracket_{\textsc{L}}$. *

Proof.

We observe that if $\varphi$ is not slim, then one of its subformulas is not in a form that can be produced by the grammar of Def. 4.9, and therefore it must have the form of one of the left-hand-side formulas from Fig. 4. Therefore, for the proposition it suffices to prove for each of these equivalences that it is sound and that the left-hand-side has a smaller length than the right-hand-side, which ensures that the rewriting of formulae terminates after at most $l(\varphi)$ substitutions. The cases for Eqs. 1 and 2 are immediate. The remaining cases are also not that hard to handle, and we describe the representative case of Eq. 7.

We can observe that $\bigwedge_{\alpha\in C}\chi_{\alpha}$ and $\bigvee_{\alpha\in C}\chi_{\alpha}$ represent respectively a sequence of $|C|$ conjunctions and disjunctions. Therefore, $l(\bigvee_{\alpha\in C}\chi_{\alpha})=|C|-1+\sum_{\alpha\in C}l(\chi_{\alpha})$. As such,

[TABLE]

[TABLE]

because $A\neq\emptyset$. To prove that Eq. 7 is sound, we observe that $t\in\llbracket\bigwedge_{\alpha\in A}\mathbf{[}\alpha\mathbf{]}\varphi_{\alpha}\land\bigvee_{\alpha\in B}\mathbf{\langle}\alpha\mathbf{\rangle}\psi_{\alpha}\rrbracket_{\textsc{L}}$ if and only if $t\in\llbracket\bigwedge_{\alpha\in A}\mathbf{[}\alpha\mathbf{]}\varphi_{\alpha}\rrbracket_{\textsc{L}}$ and $t\in\llbracket\bigvee_{\alpha\in B}\mathbf{\langle}\alpha\mathbf{\rangle}\psi_{\alpha}\rrbracket$ if and only if $t=\alpha u$ and $\alpha\in A\Rightarrow u\in\llbracket\varphi_{\alpha}\rrbracket_{\textsc{L}}$ and $\alpha\in B$ and $u\in\llbracket\mathbf{\langle}\alpha\mathbf{\rangle}\psi_{\alpha}\rrbracket_{\textsc{L}}$ if and only if $t=\alpha u$ and $\alpha\in B\setminus A$ and $u\in\llbracket\mathbf{\langle}\alpha\mathbf{\rangle}\psi_{\alpha}\rrbracket_{\textsc{L}}$, or $\alpha\in A\cap B$ and $u\in\llbracket\mathbf{\langle}\alpha\mathbf{\rangle}\psi_{\alpha}\rrbracket_{\textsc{L}}$ if and only if $t\in\llbracket\bigvee_{\alpha\in A\cap B}\mathbf{\langle}\alpha\mathbf{\rangle}(\varphi_{\alpha}\land\psi_{\alpha})\lor\bigvee_{\alpha\in B\setminus A}\mathbf{\langle}\alpha\mathbf{\rangle}\psi_{\alpha}\rrbracket_{\textsc{L}}$. ∎

B.4. Partially-Complete Monitoring

A useful measure for guarded formulae is $ms(\varphi)$ that measures the longest distance from the root of the syntax tree of $\varphi$ to either a constant $\mathsf{tt},\mathsf{ff}$, or to a modality.

Definition B.1 (Measure for guarded recHML formulae).

[TABLE]

• Proposition 4.14

For any $\varphi\in\textsc{maxHML}\cup\textsc{minHML}$, $\textsf{m}(\varphi)$ is reactive.

Proof.

The proof is by straightforward induction on $ms(\varphi)$, using the fact that $\varphi$ is guarded, and that therefore for the case of $\varphi=\max X.\psi$, $ms(\psi[\varphi/X])<ms(\varphi)$. ∎

• Proposition 4.15

For every $\varphi\in\textsc{maxHML}$, $\textsf{m}(\psi)$ is a sound and violation-complete monitor for $\varphi$. For every $\varphi\in\textsc{minHML}$, $\textsf{m}(\psi)$ is a sound and satisfaction-complete monitor for $\varphi$.

Proof.

We prove the lemma for the maxHML fragment; the proof for minHML is dual. For soundness, we need to show that if $\textbf{rej}(\textsf{m}(\varphi),t)$ (resp., $\textbf{acc}(\textsf{m}(\varphi),t)$) then $t\notin\llbracket\varphi\rrbracket$ (resp., $t\in\llbracket\varphi\rrbracket_{\textsc{L}}$). We here show the case for rejection; the case for acceptance is symmetric.

If $\textbf{rej}(\textsf{m}(\varphi),t)$ then there is an explicit trace $e$ that agrees with a prefix of $t$ on external actions, such that $\textsf{m}(\varphi)\xrightarrow[]{\;e\;}\mathrel{\mkern-14.0mu}\rightarrow\textsf{no}$. By structural induction on $e$, we prove that for every $e$ and $t$, if $\textsf{m}(\varphi)\xrightarrow[]{\;e\;}\mathrel{\mkern-14.0mu}\rightarrow\textsf{no}$ and $\lceil e\rceil$ is a prefix of $t$, then $t\notin\llbracket\varphi\rrbracket_{\textsc{L}}$.

**Case $e=\varepsilon$:: **

$\textsf{m}(\varphi)=\textsf{no}$ and thus, $\varphi=\mathsf{ff}$ where $t\notin\llbracket\mathsf{ff}\rrbracket_{\textsc{L}}$ holds trivially.

**Case $e=\mu e^{\prime}$:: **

We take cases for $\varphi$. Since $\varphi$ is closed, we do not consider the case for $\varphi=X$.

**Case $\varphi=\mathsf{ff}$:: **

Immediate.

**Case $\varphi=\mathsf{tt}$:: **

We have $\textsf{m}(\mathsf{tt})=\textsf{yes}$ and Lem. 3.1 ensures that the premise $\textsf{m}(\mathsf{tt})=\textsf{yes}\xrightarrow[]{\;e\;}\mathrel{\mkern-14.0mu}\rightarrow\textsf{no}$ cannot ever hold.

**Case $\varphi=\mathbf{[}A\mathbf{]}\varphi$:: **

By Def. 4.12, we have $\textsf{m}(\mathbf{[}A\mathbf{]}\varphi)=A.{\textsf{m}(\varphi)}+\overline{A}\textsf{.}\textsf{yes}$. This monitor cannot take a $\tau$-transition, so it must be the case that $\mu=\alpha$. Therefore , it must be the case that $t=\alpha t^{\prime}$ where $\alpha\in A$ and $\textsf{m}(\mathbf{[}A\mathbf{]}\varphi)\xrightarrow{\;\alpha\;}\textsf{m}(\varphi)\xrightarrow[]{\;e^{\prime}\;}\mathrel{\mkern-14.0mu}\rightarrow\textsf{no}$ for some $e^{\prime}$ such that $\lceil e^{\prime}\rceil$ is a prefix of $t^{\prime}$. From the IH, $t^{\prime}\notin\llbracket\varphi\rrbracket_{\textsc{L}}$, and thus, by $\alpha\in A$, we obtain $t\notin\llbracket\mathbf{[}A\mathbf{]}\varphi\rrbracket_{\textsc{L}}$.

**Case $\varphi=\mathbf{\langle}A\mathbf{\rangle}\varphi$:: **

By Def. 4.12, we have $\textsf{m}(\mathbf{\langle}A\mathbf{\rangle}\varphi)=A.{\textsf{m}(\varphi)}+\overline{A}\textsf{.}\textsf{no}$. Similar to the previous case, if $\textsf{m}(\mathbf{\langle}A\mathbf{\rangle}\varphi)\xrightarrow[]{\;\mu e^{\prime}\;}\mathrel{\mkern-14.0mu}\rightarrow\textsf{no}$, then $\mu=\alpha$ and $t=\alpha t^{\prime}$ where

• **•: **

either $\alpha\notin A$, which immediately gives us $t\notin\llbracket\mathbf{\langle}A\mathbf{\rangle}\varphi\rrbracket_{\textsc{L}}$;

• **•: **

or $\alpha\in A$ where $\textsf{m}(\varphi)\xrightarrow[]{\;e^{\prime}\;}\mathrel{\mkern-14.0mu}\rightarrow\textsf{no}$. By the IH, we obtain $t^{\prime}\notin\llbracket{\varphi}\rrbracket_{\textsc{L}}$ and thus $t\notin\llbracket\mathbf{\langle}A\mathbf{\rangle}\varphi\rrbracket_{\textsc{L}}$.

**Case $\varphi=\mathsf{max}\,X.\psi$:: **

$\textsf{m}(\varphi)=\textsf{rec}\,x.\textsf{m}(\psi)$ so $e=\tau e^{\prime}$ and $\textsf{m}(\varphi)\xrightarrow{\tau}\textsf{m}(\psi)[\textsf{rec}\,x.\textsf{m}(\psi)/x]\xrightarrow[]{\;e^{\prime}\;}\mathrel{\mkern-14.0mu}\rightarrow\textsf{no}$. Noting that $\textsf{m}(\psi)[\textsf{rec}\,x.\textsf{m}(\psi)/x]=\textsf{m}(\psi[\max X\psi/X])$, and since $\lceil e^{\prime}\rceil$ is a prefix of $t$, by the inductive hypothesis, $t\notin\llbracket\psi[\mathsf{max}\,X.\psi/X]\rrbracket_{\textsc{L}}=\llbracket\varphi\rrbracket_{\textsc{L}}$.

**Cases $\varphi_{1}\mathbf{\wedge}\varphi_{2}$ and $\varphi_{1}\mathbf{\vee}\varphi_{2}$:: **

We proceed by induction on the number of boolean connectives in the formula. If $\varphi$ has no boolean connectives, this is handled by one of the previous cases. If $\varphi=\psi_{1}\land\psi_{2}$ then $\textsf{m}(\varphi)=\textsf{m}(\psi_{1}){\otimes}\textsf{m}(\psi_{2})$. From Lem. 3.5, $\textbf{rej}(\textsf{m}(\psi_{1}){\otimes}\textsf{m}(\psi_{2}),t)$ if and only if either $\textbf{rej}(\textsf{m}(\psi_{1}),t)$ or $\textbf{rej}(\textsf{m}(\psi_{2}),t)$. By the inductive hypothesis, this is the case only if $t\notin\llbracket\psi_{1}\rrbracket_{\textsc{L}}$ or $t\notin\llbracket\psi_{2}\rrbracket_{\textsc{L}}$, and therefore $t\notin\llbracket\varphi\rrbracket_{\textsc{L}}$. The case for $\lor$ is similar.

For completeness: we need to show that if $t\notin\llbracket\varphi\rrbracket_{\textsc{L}}$ (resp., $t\in\llbracket\varphi\rrbracket_{\textsc{L}}$) then $\textbf{rej}(\textsf{m}(\varphi),t)$ (resp., $\textbf{acc}(\textsf{m}(\varphi),t)$). Again, we prove the case for rejection since the case for acceptance is symmetric.

Since $\varphi$ is closed, we can assume that each formula variable $X$ appears in the scope of a unique greatest-fixed-point operator $\max X$. We assume a mapping $un(-)$ of variables that appear in $\varphi$ to subformulae of $\varphi$, such that for every $X$, $un(X)=\max X.\psi$ for some $\psi$. We can extend the definition of monitor synthesis from Def. 4.12 to also apply on pairs $(\psi,S)$, where $\psi\in\textsc{maxHML}$ and $S$ is a set of formula variables that appear in $\varphi$, by altering the case for $X$, so that

[TABLE]

We observe that $\textsf{m}(\psi,\emptyset)=\textsf{m}(\psi)$. Therefore, to complete the proof of completeness, it suffices to prove that for all (possibly open) subformulae of $\varphi$, if $S$ is the set of free variables in $\psi$ and $t\notin\llbracket\psi,\rho\rrbracket_{\textsc{L}}$ for some environment $\rho$ such that for all $X\in S$, $\rho(X)$ is the set of traces that $\textsf{m}(X,S)$ does not reject, then $\textsf{m}(\psi,S)$ rejects $t$. We proceed to prove this claim by induction on $\psi$.

**cases $\psi\in\{X,\mathsf{ff},\mathsf{tt}\}$:: **

immediate.

**case $\psi=\mathbf{[}A\mathbf{]}\psi^{\prime}$:: **

Note that $t\notin\llbracket\mathbf{[}A\mathbf{]}\psi^{\prime},\rho\rrbracket_{\textsc{L}}$ if and only if $t=\alpha t^{\prime}$, $\alpha\in A$, and $t^{\prime}\notin\llbracket\psi^{\prime},\rho\rrbracket_{\textsc{L}}$. By the IH, $t^{\prime}\notin\llbracket\psi^{\prime},\rho\rrbracket_{\textsc{L}}$ implies that $\textsf{m}(\psi^{\prime},S)$ rejects $t^{\prime}$. As a result, the monitor $\textsf{m}(\mathbf{[}A\mathbf{]}\psi^{\prime},S)=A.{\textsf{m}(\psi^{\prime},S)}+\overline{A}\textsf{.}\textsf{yes}$ rejects $t$.

**case $\psi=\mathbf{\langle}A\mathbf{\rangle}\psi^{\prime}$:: **

$t\notin\llbracket\mathbf{\langle}A\mathbf{\rangle}\psi^{\prime},\rho\rrbracket_{\textsc{L}}$ if and only if either $t=\alpha t^{\prime}$ and $\alpha\notin A$, or else $t^{\prime}\notin\llbracket{\psi^{\prime}},\rho\rrbracket_{\textsc{L}}$. In the former case $\textsf{m}(\psi,S)$ clearly rejects $t$; in the later case, by the IH we know that $\textsf{m}(\psi^{\prime},S)$ rejects $t^{\prime}$, in which case $\textsf{m}(\mathbf{\langle}A\mathbf{\rangle}\psi^{\prime},S)=A.{\textsf{m}(\psi^{\prime},S)}+\overline{A}\textsf{.}\textsf{no}$ rejects $t$.

**cases $\psi=\psi_{1}\vee\psi_{2}$ and $\psi_{1}\land\psi_{2}$:: **

We proceed by induction on the number of boolean connectives. The case without boolean connectives is handled by one of the previous cases. If $\psi=\psi_{1}\wedge\psi_{2}$, then $\textsf{m}(\psi)=\textsf{m}(\psi_{1}){\otimes}\textsf{m}(\psi_{2})$. If $t\notin\llbracket\psi\rrbracket_{\textsc{L}}$, then it must be the case that either $t\notin\llbracket\psi_{1}\rrbracket_{\textsc{L}}$ or $t\notin\llbracket\psi_{2}\rrbracket_{\textsc{L}}$. By the IH we obtain either $\textbf{rej}(\textsf{m}(\psi_{1}),t)$ or $\textbf{rej}(\textsf{m}(\psi_{2}),t)$. Therefore, from Props. 4.14 and 3.5, $\textbf{rej}(\textsf{m}(\psi^{\prime}_{1},S){\otimes}\textsf{m}(\psi^{\prime}_{2},S),t)$. The disjunctive case is similar.

**case $\psi=\mathsf{max}\,X.\psi^{\prime}$:: **

From Fig. 1, $t\in\llbracket\psi,\rho\rrbracket_{\textsc{L}}$ if and only if there is some set of traces $T$, such that $t\in T$ and $T\subseteq\llbracket\psi^{\prime},\rho[X\mapsto T]\rrbracket_{\textsc{L}}$. Let $T$ be the set of traces not rejected by $\textsf{m}(\psi,S)$. By the IH, for every trace $t^{\prime}$,

[TABLE]

By Def. 4.12, we have $\textsf{m}(\mathsf{max}\,X.\psi^{\prime},S)=\textsf{rec}\,x.\textsf{m}(\psi^{\prime},S)$ where every transition sequence must therefore start as \textsf{rec}\,x.\textsf{m}(\psi^{\prime},S)\xrightarrow{\;\tau\;}\textsf{m}(\psi^{\prime},S)[\raisebox{2.15277pt}{\small\textsf{m}(\psi,S)}\!/\!\mbox{\smallx}]. We also have that \textsf{m}(\psi^{\prime},S)[\raisebox{2.15277pt}{\small\textsf{m}(\psi,S)}\!/\!\mbox{\smallx}]=\textsf{m}(\psi^{\prime},S\cup\{X\}). This means that, if $t^{\prime}\notin\llbracket\psi^{\prime},\rho[X\mapsto T]\rrbracket_{\textsc{L}}$, then \textsf{m}(\psi^{\prime},S)[\raisebox{2.15277pt}{\small\textsf{m}(\psi,S)}\!/\!\mbox{\smallx}] rejects $t^{\prime}$, which in turn yields that $\textsf{m}(\psi,S)$ rejects $t^{\prime}$, which is the result that we want. Therefore, for every trace $t^{\prime}$,

[TABLE]

hence $T\subseteq\llbracket\psi^{\prime},\rho[X\mapsto T]\rrbracket_{\textsc{L}}$. If $m(\psi,S)$ does not reject $t$, then $t\in T$ and thus, $t\in\llbracket\psi,\rho\rrbracket_{\textsc{L}}$; in other words, if $t\notin\llbracket\psi,\rho\rrbracket_{\textsc{L}}$, then $m(\psi,S)$ rejects $t$. ∎

The following definition, Def. B.2, lead up to Lem. 4.16, which handles the discrepancies between our synthesis functions.

Definition B.2.

For parallel monitor $m$, we define $\textsf{red}(m)$ recursively on $m$, such that $\textsf{red}(m)=m$ for $m=\textsf{yes},\textsf{no},x$, it commutes with the parallel composition operators, $\textsf{red}(m+n)=\textsf{red}(m){\otimes}\textsf{red}(n)$, $\textsf{red}(\textsf{end})=\textsf{yes}$, and $\textsf{red}({A.m})={A.\textsf{red}(m)+\overline{A}.\textsf{yes}}$. $\hfill\qed$

Lemma B.10**.**

For every $m$, $\textsf{m}(\textsf{f}(m))=\textsf{red}(m)$.

Proof.

By straightforward induction on $m$. ∎

• Lemma 4.16.

$\textsf{m}(\textsf{f}(m))$* rejects the same traces as $m$.*

Proof.

From Lem. B.10, $\textsf{m}(\textsf{f}(m))=\textsf{red}(m)$. We can decompose $\textsf{red}(-)$ to three separate operators, $\textsf{red}_{e}(-)$, $\textsf{red}_{+}(-)$, and $\textsf{red}_{a}(-)$ that respectively replace end with yes, $+$ with ${\otimes}$, and $A.n$ with $A.\textsf{red}_{a}(n)+\overline{A}.\textsf{yes}$, and commute with all other monitor operations and leave other constants unchanged. We can see that $\textsf{red}(m)=\textsf{red}_{a}(\textsf{red}_{+}(\textsf{red}_{e}(m)))$. Thus, it suffices to prove that for all $m$ and $o\in\{e,+,a\}$, $\textsf{red}_{o}(m)$ rejects the same finite traces as $m$. But this can be proven by straightforward induction on the finite trace. ∎

B.5. Tight Partially-Complete Monitoring

• Lemma 4.19.

Let $m$ be a deterministic regular monitor, where $\sum_{\alpha\in\textsc{Act}}\alpha.\textsf{no}$, $\textsf{rec}\,x.\textsf{no}$, $\sum_{\alpha\in\textsc{Act}}\alpha.\textsf{yes}$, and $\textsf{rec}\,x.\textsf{yes}$ do not occur as submonitors. Then, $m$ is tight.

Proof.

Let $m$ be a deterministic regular monitor, where $\sum_{\alpha\in\textsc{Act}}\alpha.\textsf{no}$, $\textsf{rec}\,x.\textsf{no}$, $\sum_{\alpha\in\textsc{Act}}\alpha.\textsf{yes}$, and $\textsf{rec}\,x.\textsf{yes}$ do not occur as submonitors, and let $s$ be such that $m$ rejects $st$ for every $t$. We prove that $m\xRightarrow{\;s\;}\textsf{no}$. For this, we use the alternative monitor rules that were introduced in Subsection 3.3 and the following auxiliary lemma.

Lemma** ((Aceto et al., 2016)).**

In a transition-sequence $m\xRightarrow{s}x$, such that $x$ is bound in $m$ and $m$ is deterministic, $p_{x}$ must appear.

Let $n$ be such that $m\xRightarrow{\;s\;}n$. We prove that if $n\neq\textsf{no}$, then there is some $t$ that $n$ does not reject, and this suffices due to Lemma 3.9. We use induction on $n$. If $n$ is a verdict, then the proof is complete. If $n=x$, then $n$ can only transition to $p_{x}$; but then, by the lemma, there are some $s_{1}s_{2}=s$, such that $s_{2}\neq\varepsilon$ and $m\xRightarrow{\;s_{1}\;}p_{x}\xRightarrow{\;s_{2}\;}n=x\xrightarrow{\;\tau\;}p_{x}$, and therefore $n$ does not reject $s_{2}^{\omega}$. If $n=\sum_{\alpha\in A}[\alpha]m_{\alpha}$, then if $\beta\notin A$, $n$ does not reject $\beta t$, therefore we assume that $A=\textsc{Act}$. If $n$ rejects all traces, then so do all of $m_{\alpha}$, and therefore by the inductive hypothesis, $n=\sum_{\alpha\in\textsc{Act}}[\alpha]\textsf{no}$, which contradicts the lemma’s assumptions. Finally, if $n=\textsf{rec}\,x.n^{\prime}$, then by the inductive hypothesis, either $n$ does not reject all traces, or $n^{\prime}=\textsf{no}$, which is a contradiction. ∎

Appendix C Monitorability Across Semantics

We now present the omitted proofs of Sec. 5.

C.1. The Finfinite Domain

• Lemma 5.3.

For all $\varphi\in\textsc{recHML}$, $\llbracket\varphi\rrbracket_{\textsc{F}}\cap\textsc{Trc}=\llbracket\varphi\rrbracket_{\textsc{L}}$

Proof.

Given an environment $\sigma$ on finfinite traces, let $\sigma^{\prime}$ be the restriction of $\sigma$ on Trc. Then, we can prove by induction on $\varphi$ that $t\in\llbracket\varphi,\sigma\rrbracket_{\textsc{F}}$ if and only if $t\in\llbracket\varphi,\sigma^{\prime}\rrbracket_{\textsc{L}}$, for all $\sigma$ and $t$. ∎

C.2. Monitorability over Finfinite Traces

• Lemma 5.4.

Over finfinite traces, if $m$ is sound and complete for $\varphi$, then $\varphi$ is equivalent to either $\mathsf{tt}$ or to $\mathsf{ff}$.

Proof.

If $m$ is complete for $\varphi$, then it must either accept or reject $\varepsilon$ and thus all of its extensions, that is all finfinite traces. If $m$ is also sound, then $\varphi$ is equivalent to $\mathsf{tt}$ or $\mathsf{ff}$. ∎

To facilitate some of the proofs to follow, we define $ms(\varphi)$ to measure the distance from the root of the syntax tree of $\varphi$ to either a constant $\mathsf{tt},\mathsf{ff}$, or to a modality.

Definition C.1.

[TABLE]

• Lemma 5.5.

For all $s\in\textsc{Act}^{*}$ and $g\in\textsc{fTrc}$, if $\varphi\in\textsc{unHML}$ and $sg\in\llbracket\varphi\rrbracket_{\textsc{F}}$, then $s\in\llbracket\varphi\rrbracket_{\textsc{F}}$; if $\varphi\in\textsc{exHML}$ and $s\in\llbracket\varphi\rrbracket_{\textsc{F}}$, then $sg\in\llbracket\varphi\rrbracket_{\textsc{F}}$.

Proof.

We prove the lemma for the case of $\varphi\in\textsc{unHML}$, as the case of $\varphi\in\textsc{exHML}$ is dual, and, as usual, we assume that $\varphi$ is a guarded formula. We use induction on $ms(\varphi)+|s|$. Let $sg\in\llbracket\varphi\rrbracket_{\textsc{F}}$. We proceed by a case analysis on the form of $\varphi$. The interesting cases are the ones for $\varphi=[A]\psi$ and $\varphi=\max X.\psi$. If $\varphi=[A]\psi$, then, if $s=\alpha s^{\prime}$ for some $\alpha\in A$, then $sg=\alpha s^{\prime}g$, so it must be the case that $s^{\prime}g\in\llbracket\psi\rrbracket_{\textsc{F}}$, therefore by the inductive hypothesis, $s^{\prime}\in\llbracket\psi\rrbracket_{\textsc{F}}$, so $s\in\llbracket\varphi\rrbracket_{\textsc{F}}$; otherwise, immediately by the finfinite semantics, $s\in\llbracket\varphi\rrbracket_{\textsc{F}}$. If $\varphi=\max X.\psi$, then $\llbracket\varphi\rrbracket_{\textsc{F}}=\llbracket\psi[\varphi/X]\rrbracket_{\textsc{F}}$ and since $\varphi$ is guarded, $ms(\llbracket\psi[\varphi/X]\rrbracket_{\textsc{F}})<\llbracket\varphi\rrbracket_{\textsc{F}}$, so the proof is complete by the inductive hypothesis. ∎

Definition C.2.

We say that $\varphi$ is propositionally inconsistent if $\varphi=\mathsf{ff}$, or $\varphi=\varphi_{1}\land\varphi_{2}$ and one of $\varphi_{1},\varphi_{2}$ is propositionally inconsistent, or $\varphi=\varphi_{1}\lor\varphi_{2}$ and both of $\varphi_{1},\varphi_{2}$ are propositionally inconsistent, or $\varphi=\max X.\varphi_{1}$ or $\varphi=\min X.\varphi_{1}$, and $\varphi_{1}$ is propositionally inconsistent. We can dually define that $\varphi$ is a propositional tautology.

Lemma C.1**.**

If a guarded (closed) $\varphi\in\textsc{unHML}$ is equivalent to $\mathsf{ff}$ under finfinite semantics, then it is propositionally inconsistent. If a guarded (closed) $\varphi\in\textsc{exHML}$ is equivalent to $\mathsf{tt}$ under finfinite semantics, then it is a propositional tautology.

Proof.

We prove by induction on $ms(\varphi)$ that if $\varphi$ is not propositionally inconsistent, then $\varepsilon\in\llbracket\varphi\rrbracket_{\textsc{F}}$. The cases for $\varphi=\mathsf{ff}$ or $\varphi=\mathsf{tt}$ are vacuous or trivial. If $\varphi=[A]\psi$, then by definition, $\varepsilon\in\llbracket\varphi\rrbracket_{\textsc{F}}$. If $\varphi=\max X.\psi$, then, since $\varphi$ is not propositionally inconsistent, neither is $\psi[\varphi/X]$; but $ms({\psi[\varphi/X]})<ms(\varphi)$, and by the inductive hypothesis $\varepsilon\in\llbracket\psi[\varphi/X]\rrbracket_{\textsc{F}}=\llbracket\varphi\rrbracket_{\textsc{F}}$. We can similarly prove that if $\varphi$ is not a propositional tautology, then $\varepsilon\notin\llbracket\varphi\rrbracket_{\textsc{F}}$. ∎

Lemma C.2**.**

If $\varphi$ is propositionally inconsistent, then $\textsf{m}(\varphi)\;\xRightarrow{\;\;}\;\textsf{no}$.

Proof.

Straightforward induction on $ms(\varphi)$, using Lems. A.5, A.6 and 4.15. ∎

• Proposition 5.6

Given a closed formula $\varphi\in\textsc{unHML}$, $\textsf{m}(\varphi)$ is sound and violation-complete for $\varphi$ over finfinite traces. For $\varphi\in\textsc{exHML}$, $\textsf{m}(\varphi)$ is sound and satisfaction-complete for $\varphi$ over finfinite traces.

Proof.

Let $\varphi\in\textsc{unHML}$ — the case for $\varphi\in\textsc{exHML}$ is similar. The proof for Soundness is the same as in the proof of Prop. 4.15. To prove Completeness, if $g\notin\llbracket\varphi\rrbracket_{\textsc{F}}$, then we have two cases. The first is that $g\in\textsc{Trc}$, in which case, by Lem. 5.3, $g\notin\llbracket\varphi\rrbracket_{\textsc{L}}$, and therefore, by Prop. 4.15, $\textsf{m}(\psi)$ rejects $g$. The second case is that $g\in\textsc{Act}^{*}$, in which case we use induction on $g$. The base case is that $g=\varepsilon$, which, by Lem. 5.5, implies that $\varphi$ is equivalent to $\mathsf{ff}$, which in turn, by Lems. C.1 and C.2, implies that $\textsf{m}(\varphi)$ rejects $\varepsilon$. For $g=\alpha s$, we use induction on $ms(\varphi)$. The cases for $\varphi=\mathsf{tt}$ or $\mathsf{ff}$ are immediate. Since $\varphi$ is closed, $\varphi\neq X$. If $\varphi=[A]\psi$, then $\textsf{m}(\varphi)=A.\textsf{m}(\psi)+\bar{A}.\textsf{yes}$, $\alpha\in A$ and $s\notin\llbracket\psi\rrbracket_{\textsc{F}}$, and by the inductive hypothesis on $g$, $\textsf{m}(\psi)$ rejects $s$, therefore $\textsf{m}(\varphi)$ rejects $g$. If $\varphi=[\beta]\psi$, then it is satisfied by $g$. The boolean operator cases follow from Lems. A.5 and 4.2. Finally, if $\varphi=\max X.\psi$, then $\textsf{m}(\varphi)=\textsf{rec}\,x.\textsf{m}(\psi)$ and $\textsf{m}(\psi[\varphi/X])=\textsf{m}(\psi)[\textsf{m}(\varphi)/x]$; but then, because of guardedness, $ms({\psi[\varphi/X]})<ms(\varphi)$, so by the inductive hypothesis on $ms(\varphi)$, since $\varphi$ is equivalent to $\psi[\varphi/X]$, $\textsf{m}({\psi[\varphi/X]})=\textsf{m}(\psi)[\textsf{m}(\varphi)/x]$ rejects $g$. As $\textsf{m}(\varphi)\xrightarrow{\;\tau\;}\textsf{m}(\psi)[\textsf{m}(\varphi)/x]$, $\textsf{m}(\varphi)$ rejects $g$ too.

∎

Lemma C.3**.**

If $p$ represents $\alpha g$ and $p\longrightarrow q$, then $q$ represents $g$.

Proof.

If $p\longrightarrow q$, then $p\xrightarrow{\;\alpha\;}q$. If $q\xRightarrow{\;s\;}$, then $p\xRightarrow{\;\alpha s\;}$, so $s$ is a prefix of $g$. If $q(\longrightarrow)^{k}q^{\prime}$ and $q(\longrightarrow)^{k}q^{\prime\prime}$, then $p(\longrightarrow)^{k+1}q^{\prime}$ and $p(\longrightarrow)^{k+1}q^{\prime\prime}$, so $q^{\prime}=q^{\prime\prime}$. ∎

• Lemma 5.7.

If $p$ represents $g$, then $g\in\llbracket\varphi\rrbracket_{\textsc{F}}$ iff $p\in\llbracket\varphi\rrbracket_{\textsc{B}}$.

Proof.

Given an environment $\sigma$ for finfinite traces, let $\sigma_{B}$ be an environment on processes, such that for every $X$,

[TABLE]

given an environment $\rho$ on processes, we can similarly define

[TABLE]

We prove that if $g\in\llbracket\varphi,\sigma\rrbracket_{\textsc{F}}$, then $p\in\llbracket\varphi,\sigma_{B}\rrbracket_{\textsc{B}}$, by induction on $\varphi$. The cases for $\varphi=\mathsf{tt},\mathsf{ff},X$, and the boolean operators are immediate. The cases for $\varphi=\mathbf{\langle}\alpha\mathbf{\rangle}\psi$ or $\varphi=\mathbf{[}\alpha\mathbf{]}\psi$ follow from Lem. C.3. If $\varphi=\max X.\psi$ and $g\in\llbracket\varphi\rrbracket_{\textsc{F}}$, then there is some $T\subseteq\llbracket\psi,\sigma[X\mapsto T]\rrbracket_{\textsc{F}}$ with $g\in T$. Let $T^{\prime}=\{q\mid q$ represents some $h\in T\}$. We can see that $p\in T^{\prime}$ and by the inductive hypothesis, $T^{\prime}\subseteq\llbracket\psi,(\sigma[X\mapsto T])_{B}\rrbracket_{\textsc{B}}=\llbracket\psi,\sigma_{B}[X\mapsto T^{\prime}]\rrbracket_{\textsc{B}}$, which implies that $p\in\llbracket\varphi,\sigma_{B}\rrbracket_{\textsc{B}}$. If $\varphi=\min X.\psi$, then $\forall T.(\llbracket\psi,\sigma[X\mapsto T]\rrbracket_{\textsc{F}}\subseteq T\Rightarrow g\in T)$. If for a set of processes $R$, $\llbracket\psi,\sigma_{B}[X\mapsto R]\rrbracket_{\textsc{B}}\subseteq R$, then due to the monotonicity of $\psi$, for $R_{t}$ the set of trace-processes from $R$ and $R^{\prime}=\{h\mid h$ is represented by some $p\in R\}$, $\llbracket\psi,(\sigma[X\mapsto R^{\prime}])_{B}\rrbracket_{\textsc{B}}=\llbracket\psi,\sigma_{B}[X\mapsto R_{t}]\rrbracket_{\textsc{B}}\subseteq R$. By the inductive hypothesis, if $q$ represents $h$, then $h\in\llbracket\psi,\sigma[X\mapsto R^{\prime}]\rrbracket_{\textsc{F}}$ implies that $q\in\llbracket\psi,(\sigma[X\mapsto R^{\prime}])_{B}\rrbracket_{\textsc{B}}$, and therefore, $q\in R$, yielding that $h\in R^{\prime}$. Therefore, $g\in R^{\prime}$, and so $p\in R$. Thus, we proved that $\forall R.(\llbracket\psi,\sigma_{B}[X\mapsto R]\rrbracket_{\textsc{B}}\subseteq R\Rightarrow p\in R)$, and thus, $p\in\llbracket\varphi\rrbracket_{\textsc{B}}$.

We can similarly prove that if $p\in\llbracket\varphi,\rho\rrbracket_{\textsc{B}}$, then $g\in\llbracket\varphi,\rho_{L}\rrbracket_{\textsc{F}}$. ∎

C.3. Monitorable Formulae across Semantics

Lemma C.4**.**

*If $\varphi\in\textsc{recHML}$ has a sound and violation-complete (resp., satisfaction-complete) regular or reactive parallel monitor over infinite traces, then there is some $\psi\in\textsc{sHML}$ (resp., $\psi\in\textsc{cHML}$) that is equivalent to $\varphi$ over infinite traces. *

Proof.

Let $m$ be a sound and violation-complete regular or reactive parallel monitor for $\varphi$ over finfinite traces. By Proposition 3.8, there is a regular monitor $n$ that is verdict-equivalent to $m$, so it is also sound and violation-complete for $\varphi$. From Thm. 5.1 there is a formula $\psi\in\textsc{sHML}$, such that $n$ is sound and violation-complete for $\psi$ over all LTSs, including the LTS of trace-processes. Since $n$ is sound and violation-complete for $\psi$ on trace processes, $p_{g}\in\llbracket\psi\rrbracket_{\textsc{B}}$ is equivalent to claiming that $n$ does not reject any trace that $p_{g}$ can produce. However, this is equivalent to saying that $n$ does not reject $t$, which is equivalent to $t\in\llbracket\varphi\rrbracket_{\textsc{L}}$. By Lems. 5.7 and 5.3, $t\in\llbracket\psi\rrbracket_{\textsc{L}}$ iff $p_{t}\in\llbracket\psi\rrbracket_{\textsc{B}}$, and the proof is complete. The case for a satisfaction-complete monitor is similar. ∎

• Proposition 5.9

If $\varphi\in\textsc{unHML}$ (resp., $\varphi\in\textsc{exHML}$), then there is some $\psi\in\textsc{sHML}$ (resp., $\psi\in\textsc{cHML}$) that is equivalent to $\varphi$ over finfinite traces.

Proof.

If $\varphi\in\textsc{unHML}$ (resp., $\varphi\in\textsc{exHML}$), then from Prop. 5.6, there is a monitor $m$ that is sound and violation-complete (resp., satisfaction-complete) for $\varphi$ over finfinite traces. From Prop. 5.8, $\varphi$ is then equivalent to a formula in sHML (resp., cHML). ∎

• Proposition 5.10

If $\varphi\in\textsc{maxHML}$ (resp., $\varphi\in\textsc{minHML}$), then there is some $\psi\in\textsc{sHML}$ (resp., $\psi\in\textsc{cHML}$) that is equivalent to $\varphi$ over infinite traces.

Proof.

sHML is just maxHML without disjunctions or $\mathbf{\langle}\alpha\mathbf{\rangle}$-operators. We first show that on infinite linear semantics, $\mathbf{\langle}A\mathbf{\rangle}\varphi$ can be rewritten as $\mathbf{[}\overline{A}\mathbf{]}\mathsf{ff}\wedge\mathbf{[}A\mathbf{]}\varphi$. Indeed, if $t\in\llbracket\mathbf{\langle}A\mathbf{\rangle}\varphi\rrbracket_{\textsc{L}}$ then $t=\alpha u$ for some $\alpha\in A$ and $u\in\llbracket\varphi\rrbracket_{\textsc{L}}$. Then $t\in\llbracket\mathbf{[}\overline{A}\mathbf{]}\mathsf{ff}\wedge\mathbf{[}A\mathbf{]}\varphi\rrbracket_{\textsc{L}}$. Conversely, if $t\notin\llbracket\mathbf{\langle}A\mathbf{\rangle}\varphi\rrbracket_{\textsc{L}}$ then $t=\alpha u$ and either $\alpha\notin A$ or $u\notin\llbracket\varphi\rrbracket_{\textsc{L}}$. In either case, $t\notin\llbracket\mathbf{[}\overline{A}\mathbf{]}\mathsf{ff}\wedge\mathbf{[}A\mathbf{]}\varphi\rrbracket_{\textsc{L}}$.

This gives up a formula in unHML. From Prop. 5.8, this formula is then equivalent to a sHML formula over finfinite traces. From Lem. 5.3 this equivalence also holds over infinite traces. ∎

• Lemma C.5.

If $p\in\llbracket\varphi\rrbracket_{\textsc{B}}$ for $\varphi\in\textsc{sHML}$, and $p$ subsumes $p^{\prime}$, then $p^{\prime}\in\llbracket\varphi\rrbracket_{\textsc{B}}$. Dually, if $p\notin\llbracket\varphi\rrbracket_{\textsc{B}}$ for $\varphi\in\textsc{cHML}$, and $p$ subsumes $p^{\prime}$ then $p^{\prime}\notin\llbracket\varphi\rrbracket_{\textsc{B}}$.

Proof.

Let $p\in\llbracket\varphi\rrbracket_{\textsc{B}}$ for $\varphi\in\textsc{sHML}$, and suppose that $p$ subsume $p^{\prime}$. We claim that $p^{\prime}\in\llbracket\varphi\rrbracket_{\textsc{B}}$. Indeed, assume towards a contradiction, that $p^{\prime}\notin\llbracket\varphi\rrbracket_{\textsc{B}}$. Since $\varphi\in\textsc{sHML}$, from Thm. 5.1 there is a monitor $m$ that is sound and violation-complete for $\varphi$ with respect to the branching-time semantics. As $m$ is violation-complete for $\varphi$ and $p^{\prime}$ does not satisfy $\varphi$, we have that $\textbf{rej}(m,p^{\prime},s)$ for some $s$, that is $m\triangleleft\,p^{\prime}\xRightarrow{\;s\;}\textsf{no}\triangleleft\,q^{\prime}$. Then by unzipping (Lem. 3.3) $m\xRightarrow{\;s\;}\textsf{no}$ and $p^{\prime}\xRightarrow{\;s\;}q^{\prime}$. Since $p$ subsumes $p^{\prime}$, $p\xRightarrow{\;s\;}q$ for some process $q$. Then, from Lem. 3.4 $m\triangleleft\,p\xRightarrow{\;s\;}\textsf{no}\triangleleft\,q$, i.e., $\textbf{rej}(m,p,s)$, which contradicts the soundness of $m$ for $\varphi$. The case of $\varphi\in\textsc{cHML}$ is obtained by duality. ∎

Definition C.3.

We say that a process $p$ subsumes a process $p^{\prime}$ if $p$ produces all the finfinite traces that $p^{\prime}$ produces.

Lemma C.5**.**

If $p\in\llbracket\varphi\rrbracket_{\textsc{B}}$ for $\varphi\in\textsc{sHML}$, and $p$ subsumes $p^{\prime}$, then $p^{\prime}\in\llbracket\varphi\rrbracket_{\textsc{B}}$. Dually, if $p\notin\llbracket\varphi\rrbracket_{\textsc{B}}$ for $\varphi\in\textsc{cHML}$, and $p$ subsumes $p^{\prime}$ then $p^{\prime}\notin\llbracket\varphi\rrbracket_{\textsc{B}}$.

• Proposition 5.11

For a process $p$ and a formula $\varphi\in\textsc{sHML}$, the following are equivalent:

1. (1)

$p\in\llbracket\varphi\rrbracket_{\textsc{B}}$** 2. (2)

If $p$ produces a finfinite trace $g$, then $g\in\llbracket\varphi\rrbracket_{\textsc{F}}$

Proof.

**Direction (1) implies (2): **

Assume $p\in\llbracket\varphi\rrbracket_{\textsc{B}}$ and that $p$ produces a finfinite trace $g$. Then $p$ subsumes the trace-process $p_{g}$. From Lem. C.5, $p_{g}\in\llbracket\varphi\rrbracket_{\textsc{B}}$. Since $p_{g}$ is a trace process, from Lem. 5.7, $g\in\llbracket\varphi\rrbracket_{\textsc{F}}$.

**Direction (2) implies (1): **

Assume that $p\notin\llbracket\varphi\rrbracket_{\textsc{B}}$. Let $g$ be a trace produced by $p$. Again, $p$ subsumes $p_{g}$, and from Lem. C.5 $p_{g}\notin\llbracket\varphi\rrbracket_{\textsc{B}}$. Since $p_{g}$ is a trace process, from Lem. 5.7, $g\notin\llbracket\varphi\rrbracket_{\textsc{F}}$. ∎