The Cost of Monitoring Alone

TL;DR

This paper analyzes the size complexity involved in transforming parallel monitors into regular and deterministic monitors for infinite trace properties, revealing tight double and triple-exponential bounds.

Contribution

It establishes tight bounds on the exponential blowup in monitor size when converting between different monitoring systems and logic fragments.

Findings

Transforming parallel to regular monitors incurs double-exponential size increase.

Deterministic monitor translation causes a triple-exponential blowup.

Bounds are proven to be tight for these transformations.

Abstract

We compare the succinctness of two monitoring systems for properties of infinite traces, namely parallel and regular monitors. Although a parallel monitor can be turned into an equivalent regular monitor, the cost of this transformation is a double-exponential blowup in the syntactic size of the monitors, and a triple-exponential blowup when the goal is a deterministic monitor. We show that these bounds are tight and that they also hold for translations between corresponding fragments of Hennessy-Milner logic with recursion over infinite traces.

Equations

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

$$\mid ⟨\alpha ⟩\phi$$

$$[[\mathsf{tt},\rho ]]$$

$$[[{\phi }_1\wedge {\phi }_2,\rho ]]$$

$$[[[\alpha ]\phi ,\rho ]]$$

$$[[\mathsf{min}X.\phi ,\rho ]]$$

$$[[\mathsf{max}X.\phi ,\rho ]]$$

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

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

$$\displaystyle\texttt{Regular monitor rules:}\hrulefill\penalty-10000\hskip 20.00003pt plus 0.5fil minus 5.0pt\penalty-10000\hskip 20.00003pt plus 0.5fil minus 5.0pt\inference[\textsc{Act}]{}{\alpha.{m}\;\xrightarrow{\;\alpha\;}\;m}\penalty 50\hskip 20.00003pt plus 0.5fil minus 5.0pt\inference[\textsc{RecF}]{}{\textsf{rec}\,x.m\;\xrightarrow{\;\tau\;}\;m}\penalty 50\hskip 20.00003pt plus 0.5fil minus 5.0pt\inference[\textsc{RecB}]{}{x\;\xrightarrow{\;\tau\;}\;p_{x}}\penalty-10000\hskip 20.00003pt plus 0.5fil minus 5.0pt\inference[\textsc{SelL}]{m\;\xrightarrow{\;\mu\;}\;m^{\prime}}{m+n\;\xrightarrow{\;\mu\;}\;m^{\prime}}\penalty 50\hskip 20.00003pt plus 0.5fil minus 5.0pt\inference[\textsc{SelR}]{n\;\xrightarrow{\;\mu\;}\;n^{\prime}}{m+n\;\xrightarrow{\;\mu\;}\;n^{\prime}}\penalty 50\hskip 20.00003pt plus 0.5fil minus 5.0pt\inference[\textsc{Ver}]{}{v\;\xrightarrow{\;\alpha\;}\;v}\penalty-10000\hskip 20.00003pt plus 0.5fil minus 5.0pt\penalty-10000\hskip 20.00003pt plus 0.5fil minus 5.0pt\hrulefill\texttt{Parallel tracing rules:}\hrulefill\penalty-10000\hskip 20.00003pt plus 0.5fil minus 5.0pt\penalty-10000\hskip 20.00003pt plus 0.5fil minus 5.0pt\inference[\textsc{Par}]{m\;\xrightarrow{\;\alpha\;}\;m^{\prime}&n\;\xrightarrow{\;\alpha\;}\;n^{\prime}}{m{\odot}n\;\xrightarrow{\;\alpha\;}\;m^{\prime}{\odot}n^{\prime}}\quad\inference[\textsc{TauL}]{m\;\xrightarrow{\;\tau\;}\;m^{\prime}}{m{\odot}n\;\xrightarrow{\;\tau\;}\;m^{\prime}{\odot}n}\quad\penalty-10000\hskip 20.00003pt plus 0.5fil minus 5.0pt\penalty-10000\hskip 20.00003pt plus 0.5fil minus 5.0pt\texttt{Parallel evaluation rules:}\hrulefill\penalty-10000\hskip 20.00003pt plus 0.5fil minus 5.0pt\penalty-10000\hskip 20.00003pt plus 0.5fil minus 5.0pt\inference[\textsc{VrE}]{}{\textsf{end}{\odot}\textsf{end}\xrightarrow{\;\tau\;}\textsf{end}}\penalty 50\hskip 20.00003pt plus 0.5fil minus 5.0pt\inference[\textsc{VrC1}]{}{{{\textsf{yes}{\otimes}m}\xrightarrow{\;\tau\;}{m}}}\penalty 50\hskip 20.00003pt plus 0.5fil minus 5.0pt\inference[\textsc{VrC2}]{}{{{\textsf{no}{\otimes}m}\xrightarrow{\;\tau\;}{\textsf{no}}}}\penalty-10000\hskip 20.00003pt plus 0.5fil minus 5.0pt\penalty-10000\hskip 20.00003pt plus 0.5fil minus 5.0pt\inference[\textsc{VrD1}]{}{{{\textsf{no}{\oplus}m}\xrightarrow{\;\tau\;}{m}}}\penalty 50\hskip 20.00003pt plus 0.5fil minus 5.0pt\inference[\textsc{VrD2}]{}{{{\textsf{yes}{\oplus}m}\xrightarrow{\;\tau\;}{\textsf{yes}}}}$$

$$m_{\tau }$$

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

$$\stackrel{\tau }{\to }(m_{\tau }\otimes (a.\text{yes}+b.\text{yes}))\otimes (a.\text{yes}+b.\text{yes})⟶\cdots$$

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

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

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

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

$$L_V^k=\{u\#w\#v\$w\mid u,v\in \{0,1,\#{\}}^{\ast },w\in \{0,1{\}}^k\}.$$

$$W=\left\{a_{1}\alpha_{1}\cdots a_{k}\alpha_{k}\in\{0,1\}^{(l+1)\cdot k}\bigm{|}\begin{tabular}[]{l}for all $1\leq i\leq k,~{}\alpha_{i}\in\{0,1\}$ and\\ $a_{i}\in\{0,1\}^{l}$, and $a_{1}\cdots a_{k}\in\{0,1\}^{l}!$\end{tabular}\right\}.$$

$$L_A^k=\{u\#w\#v\$u^{\prime }\#w^{\prime }\#\$v^{\prime }\mid u,v^{\prime }\in {\Sigma }_{\$}^{\ast },u^{\prime },v\in {\Sigma }^{\ast },w,w^{\prime }\in W,\text{ and }w\equiv w^{\prime }\}.$$

$$ski{p}_{\#}(m)$$

$$nex{t}_{\#}(m)$$

$$nex{t}_{\$}(m)$$

$$skip\_last(m)$$

$$all:=\otimes \{\text{rec}x.(\{0,1{\}}^{l+1}.x\oplus s.\{0,1\}.\text{yes})\mid s\in \{0,1{\}}^l\};$$

$$no\_more(s):=\text{rec}x.\left(\#.\text{yes}+(\{0,1{\}}^l\setminus \{s\}).\{0,1\}.x\right);$$

$$unique:=\text{rec}x.\left(\#.\text{yes}+\left(\{0,1{\}}^{l+1}.x\otimes \sum _{s\in \{0,1{\}}^l}s.\{0,1\}.no\_more(s)\right)\right);\text{ and}$$

$$perm:=all\otimes unique.$$

$$find(s):=\text{rec}x.(s.\text{yes}+(\{0,1{\}}^{l+1}\setminus \{s\}).x).$$

$$match(s):=nex{t}_{\$}(skip\_last(find(s))).$$

$$matching:=$$

$$m_A^k:=$$

$$|m|\geq\left(\big{(}2^{2^{k-1}}-1\big{)}!\right)^{2}=2^{\Omega\big{(}2^{2^{k-1}+k}\big{)}}.$$

$$smaller$$

$$last$$

$$m_U$$

$$\delta (q,\alpha )=\{\begin{array}{ll}\{q_0^a,q_0^r\}& \text{for }q=q_0,\alpha =\epsilon ,\\ {\delta }_o(q,\alpha )& \text{for }q\in Q_o,\alpha \in \text{textsc}Act\cup \{\epsilon \},o\in \{a,r\},\\ \{f\}& \text{for }q\in F_a,\alpha =♡,\\ \{f\}& \text{for }q\in F_r,\alpha =♠,\\ \{f\}& \text{for }q=f,\\ \varnothing & \text{otherwise.}\end{array}$$

$$t_i=\#enc(w_0)\#enc(w_1)\#\cdots \#enc(w_{|C_i|})\#,$$

Full text

1 Introduction

Runtime Verification is a lightweight verification technique where a computational entity that we call a monitor is used to observe a system run in order to verify a given property. That property, which we choose to formalize in Hennessy-Milner logic with recursion (recHML) [13], can be a potential property of either the system [12, 2], or of the current system run, encoded as a trace of events [5] — see also, for example, [14, 10, 8] for earlier work on the monitoring of trace properties, mainly formalized on LTL.

To address the case of verifying trace properties, the authors introduced in [5] a class of monitors that can generate multiple parallel components that analyse the same system trace. These were called parallel monitors. When some of them reach a verdict, they can combine these verdicts into one. In the same paper, it was determined that this monitoring system has the same monitoring power as its restriction to a single monitoring component, as it was used in [12, 2], called regular monitors. However, the cost of the translation from the more general monitoring system to this fragment, as given in [5], is doubly exponential with respect to the syntactic size of the monitors. Furthermore, if the goal is a deterministic regular monitor [4, 3], then the resulting monitor is quadruply-exponentially larger than the original, parallel one, in [5].

In this paper, we show that the double-exponential cost for translating from parallel to equivalent regular monitors is tight. Furthermore, we improve the translation cost from parallel monitors to equivalent deterministic monitors to a triple exponential, and we show that this bound is tight. We define monitor equivalence in two ways, the first one stricter than the second. For the first definition, two monitors are equivalent when they reach the same verdicts for the same finite traces, while for the second one it suffices to reach the same verdicts for the same infinite traces. We prove the upper bounds for a transformation that gives monitors that are equivalent with respect to the stricter definition, while we prove the lower bounds with respect to transformations that satisfy the coarser definition. Therefore, our bounds hold for both definitions of monitor equivalence. This treatment allows us to derive stronger results, which yield similar bounds for the case of logical formulae, as well.

In [5], we show that, when interpreted over traces, mxHML, the fragment of recHML that does not use least fixed points, is equivalent to the syntactically smaller safety fragment sHML. That is, every mxHML formula can be translated to a logically equivalent sHML formula. Similarly to the aforementioned translation of monitors, this translation of formulae results in a formula that that is syntactically at most doubly-exponentially larger than the original formula. We show that this upper bound is tight.

The first four authors have worked on the complexity of monitor transformations before in [4, 3], where the cost of determinizing monitors is examined. Similarly to [4, 3], in [5], but also in this paper, we use results and techniques from Automata Theory and specifically about alternating automata [9, 11].

In Sec. 2, we introduce the necessary background on monitors and recHML on infinite traces, as these were used in [5]. In Sec. 3, we describe the monitor translations that we mentioned above, and we provide upper bounds for these, which we prove to be tight in Sec. 4. In Sec. 5, we extrapolate these bounds to the case where we translate logical formulae, from mxHML to sHML. In Sec. 6, we conclude the paper. Omitted proofs can be found in the appendix.

2 Preliminaries

Monitors are expected to monitor for a specification, which, in our case, is written in recHML. We use the linear-time interpretation of the logic recHML, as it was given in [5]. According to that interpretation, formulae are interpreted over infinite traces.

2.1 The model and the logic

We assume a finite set of actions

$\alpha,\beta,\ldots\in\textsc{Act}$ with distinguished silent action $\tau$. We also assume that $\tau\not\in\textsc{Act}$ and that $\mu\in\textsc{Act}\cup\left\{\tau\right\}$, and refer to the actions in Act as visible actions (as opposed to the silent action $\tau$). The metavariables $t,u\in\textsc{Trc}=\textsc{Act}^{\omega}$ range over (infinite) sequences of visible actions, which abstractly represent system runs. We also use the metavariable $T\subseteq\textsc{Trc}$ to range over sets of traces. We often need to refer to finite traces, denoted as $s,r\in\textsc{Act}^{\ast}$, to represent objects such as a finite prefix of a system run, or to traces that may be finite or infinite (finfinite traces, as they were called in [5]), denoted as $g,h\in\textsc{Act}^{\ast}\cup\textsc{Act}^{\omega}$. A trace (resp., finite trace, resp., finfinite trace) with action $\alpha$ at its head is denoted as $\alpha t$ (resp., $\alpha s$, resp., $\alpha g$). Similarly a trace with a prefix $s$ is written $st$.

The logic recHML [13, 7] assumes a countable set LVar (with $X\in\textsc{LVar}$) of logical variables, and is defined as the set of closed formulae generated by the grammar of Fig. 1. Apart from the standard constructs for truth, falsehood, conjunction and disjunction, the logic is equipped with possibility and necessity modal operators labelled by visible actions, together with recursive formulae expressing 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.

We interpret recHML formulae over traces, using an interpretation function $\llbracket-\rrbracket$ that maps formulae to sets of traces, relative to an environment $\rho:\textsc{LVar}\to 2^{\textsc{Trc}}$, which intuitively assigns to each variable $X$ the set of traces that are assumed to satisfy it, as defined in Fig. 1. The semantics of a closed formula $\varphi$ is independent of the environment $\rho$ and is simply written $\llbracket\varphi\rrbracket$. Intuitively, $\llbracket\varphi\rrbracket$ denotes the set of traces satisfying $\varphi$. For a formula $\varphi$, we use $l(\varphi)$ to denote the length of $\varphi$ as a string of symbols.

2.2 Two monitoring systems

We now present two monitoring systems, parallel and regular monitors, that were introduced in [12, 2, 5]. A monitoring system is a Labelled Transition System (LTS) based on Act, the set of actions, that is comprised of the monitor states, or monitors, and a transition relation. The set of monitor states, Mon, and the monitor transition relation, $\longrightarrow\subseteq(\textsc{Mon}\times(\textsc{Act}\cup\left\{\tau\right\})\times\textsc{Mon})$, are defined in Fig. 2. There and elsewhere, ${\odot}$ ranges over both parallel operators ${\oplus}$ and ${\otimes}$. When discussing a monitor with free variables (an open monitor) $m$, we assume it is part of a larger monitor $m^{\prime}$ without free variables (a closed monitor), where every variable $x$ appears at most once in a recursive operator. Therefore, we assume an injective mapping from each monitor variable $x$ to a unique monitor $p_{x}$, of the form $\textsf{rec}\,x.m$ that is a submonitor of $m^{\prime}$.

The suggestive notation $m\xrightarrow{\;\mu\;}n$ denotes $(m,\mu,n)\in\longrightarrow$; we also write $m\not\!\xrightarrow{\;\mu\;}$ to denote $\neg(\exists n.\;m\xrightarrow{\;\mu\;}n)$. We employ the usual notation for weak transitions and write $m\xRightarrow{\quad}n$ in lieu of $m(\xrightarrow{\;\tau\;})^{\ast}n$ and $m\xRightarrow{\;\mu\;}n$ for $m\xRightarrow{\quad}\cdot\xrightarrow{\;\mu\;}\cdot\xRightarrow{\quad}n$. We write sequences of transitions $m\xRightarrow{\alpha_{1}}\cdots\xRightarrow{\alpha_{k}}m_{k}$ as $m\xRightarrow{\;s\;}m_{k}$, where $s=\alpha_{1}\cdots\alpha_{k}$. The monitoring system of parallel monitors is defined using the full syntax and all the rules from Fig. 2; regular monitors are parallel monitors that do not use the parallel operators ${\otimes}$ and ${\oplus}$. Regular monitors were defined and used already in [2] and [12], while parallel monitors were defined in [5]. We observe that the rules RecF and RecB are not the standard recursion rules from [2] and [12], but they are equivalent to those rules [5, 1] and more convenient for our arguments.

A transition $m\xrightarrow{\;\alpha\;}n$ denotes that the monitor in state $m$ can analyse the (visible) 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. Rule Par 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. 2 also allow $\tau$-transitions for the reconfiguration of parallel compositions of monitors. For instance, rules VrC1 and VrC2 describe the fact that, in conjunctive parallel compositions, whereas yes verdicts are uninfluential, no verdicts supersede the verdicts of other monitors (Fig. 2 omits the obvious symmetric rules). The dual applies for yes and no verdicts in a disjunctive parallel composition, as described by rules VrD1 and VrD2 (again, we omit the obvious symmetric rules). Rule VrE applies to both forms of parallel composition and consolidates multiple inconclusive verdicts. Finally, rules TauL and its omitted dual TauR are contextual rules for these monitor reconfiguration steps.

Definition 1 (Acceptance and Rejection)

We say that $m$ rejects (resp., accepts) $s\in\textsc{Act}^{*}$ when $m\xRightarrow{\;s\;}\textsf{no}$ (resp., $m\xRightarrow{\;s\;}\textsf{yes}$). We similarly say that $m$ rejects (resp., accepts) $t\in\textsc{Act}^{\omega}$ if $m$ rejects (resp., accepts) some prefix of $t$.

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 $\sum_{i\in I}m_{i}$ to denote any 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. For each $j\in I$, $m_{j}$ is called a summand of $\sum_{i\in I}m_{i}$ (and the term $\sum_{i\in I}m_{i}$ is called a sum of $m_{j}$). The regular monitors in Fig. 2 have an important property, namely that their state space, i.e., the set of reachable states, is finite (see Remark 1). On the other hand, parallel monitors can be infinite-state, but they are convenient when one synthesizes monitors. However, the two monitoring systems are equivalent (see Prop. 2). For a monitor $m$, $\textsf{reach}(m)$ is the set of monitor states reachable through a transition sequence from $m$.

Lemma 1 (Verdict Persistence, [12, 5])

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

Lemma 2

Every submonitor of a closed regular monitor $m$ can only transition to submonitors of $m$.

Remark 1

An immediate consequence of Lem. 2 is that regular monitors are finite-state. This is not the case for parallel monitors, in general. For example, consider parallel monitor $m_{\tau}=\textsf{rec}\,x.(x{\otimes}(a.\textsf{yes}+b.\textsf{yes}))$. We can see that there is a unique sequence of transitions that can be made from $m_{\tau}$:

[TABLE]

One basic requirement that we maintain on monitors is that they are not allowed to give conflicting verdicts for the same trace.

Definition 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}$.

We identify a useful monitor predicate that allows us to neatly decompose the behaviour of a parallel monitor in terms of its constituent sub-monitors.

Definition 3 (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}$.

The following lemma states that parallel monitors behave as expected with respect to the acceptance and rejection of traces as long as the constituent submonitors are reactive.

Lemma 3 ([5])

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$.*

The following example, which stems from [5], indicates why the assumption that $m_{1}$ and $m_{2}$ are reactive is needed in Lem. 3.

Example 1

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. 2, $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.

In general, we are interested in reactive parallel monitors, and the parallel monitors that we use will have this property.

2.3 Automata, Languages, Equivalence

In [5], we describe how to transform a parallel monitor to a verdict equivalent regular one. This transformation goes through alternating automata [9, 11]. For our purposes, we only need to define nondeterministic and deterministic automata.

Definition 4 (Finite Automata)

A nondeterminitic finite automaton (NFA) is a quintuple $A=(Q,\textsc{Act},q_{0},\delta,F)$, where $Q$ is a finite set of states, Act is a finite alphabet (here it coincides with the set of actions), $q_{0}$ is the starting state, $F\subseteq Q$ is the set of accepting, or final states, and $\delta\subseteq Q\times\textsc{Act}\times Q$ is the transition relation. An NFA is deterministic (DFA) if $\delta$ is a function from $Q\times\textsc{Act}$ to $Q$.

Given a state $q\in Q$ and a symbol $\alpha\in\textsc{Act}$, $\delta$ returns a set of possible states where the NFA can transition, and we typically use $q^{\prime}\in\delta(q,\alpha)$ instead of $(q,\alpha,q^{\prime})\in\delta$. We extend the transition relation to $\delta^{*}:Q\times\textsc{Act}^{*}\to 2^{Q}$, so that $\delta^{*}(q,\varepsilon)=\{q\}$ and $\delta^{*}(q,\alpha s)=\bigcup\{\delta^{*}(q^{\prime},s)\mid q^{\prime}\in\delta(q,\alpha)\}$. We say that the automaton accepts $s\in\textsc{Act}^{*}$ when $\delta^{*}(q_{0},s)\cap F\neq\emptyset$, and that it recognizes $L\subseteq\textsc{Act}^{*}$ when $L$ is the set of strings accepted by the automaton.

Definition 5 (Monitor Language Recognition)

A monitor $m$ recognizes positively (resp., negatively) 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$ recognizes positively (resp., negatively) $L_{a}(m)$ (resp., $L_{r}(m)$). Similarly, we say that $m$ recognizes positively (resp., negatively) a set of infinite traces $L\subseteq\textsc{Act}^{\omega}$ when for every $t\in\textsc{Act}^{\omega}$, $t\in L$ if and only if $m$ accepts (resp., rejects) $t$.

Observe that, by Lem. 1, $L_{a}(m)$ and $L_{r}(m)$ are closed under finite extensions.

Lemma 4

The set of infinite traces that is recognized positively (resp., negatively) by $m$ is exactly $L_{a}(m)\cdot\textsc{Act}^{\omega}$ (resp., $L_{r}(m)\cdot\textsc{Act}^{\omega}$).

Proof

The lemma is a consequence of verdict persistence (Lem. 1). ∎

To compare different monitors, we use a notion of monitor equivalence from [4] that focusses on how monitors can reach verdicts.

Definition 6 (Verdict Equivalence)

Monitors $m$ and $n$ are verdict equivalent, denoted as $m\simeq_{\text{v}}n$, if $L_{a}(m)=L_{a}(n)$ and $L_{r}(m)=L_{r}(n)$.

One may consider the notion of verdict equivalence, as defined in Def. 6, to be too strict. After all, verdict equivalence is defined with respect to finite traces, so if we want to turn a parallel monitor into a regular or deterministic monitor, the resulting monitor not only needs to accept and reject the same infinite traces, but it is required to do so at the same time the original parallel monitor does. However, one may prefer to have a smaller, but not tight monitor, if possible, as long as it accepts the same infinite traces.

Definition 7 ($\omega$-Verdict Equivalence)

Monitors $m$ and $n$ are $\omega$-verdict equivalent, denoted as $m\simeq_{\omega}n$, if $L_{a}(m)\cdot\textsc{Act}^{\omega}=L_{a}(n)\cdot\textsc{Act}^{\omega}$ and $L_{r}(m)\cdot\textsc{Act}^{\omega}=L_{r}(n)\cdot\textsc{Act}^{\omega}$.

From Lem. 4 we observe that verdict equivalence implies $\omega$-verdict equivalence. The converse does not hold, because $\textsf{no}\simeq_{\omega}\sum\limits_{\alpha\in\textsc{Act}}\alpha.\textsf{no}$, but $\textsf{no}\not\simeq_{\text{v}}\sum\limits_{\alpha\in\textsc{Act}}\alpha.\textsf{no}$.

Definition 8 ([3])

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

Example 2

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

2.4 Synthesis

There is a tight connection between the logic from Sec. 2.1 and the monitoring systems from Sec. 2.2. Ideally, we would want to be able to synthesize a monitor from any formula $\varphi$, such that the monitor recognizes $\llbracket\varphi\rrbracket$ positively and $\textsc{Trc}\setminus\llbracket\varphi\rrbracket$ negatively. However, as shown in [5], neither goal is possible for all formulae. Instead, we identify the following fragments of recHML.

Definition 9 (MAX and MIN Fragments of recHML)

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

[TABLE]

Definition 10 (Safety and co-Safety Fragments of recHML)

The safety and co-safety fragments of recHML are, respectively, defined as:

[TABLE]

Theorem 2.1 (Monitorability and Maximality, [5])

For every $\varphi\in\textsc{mxHML}$ (resp., $\varphi\in\textsc{mnHML}$), there is a reactive parallel monitor $m$, such that $l(m)=O(l(\varphi))$ and $L_{r}(m)\cdot\textsc{Act}^{\omega}=\textsc{Act}^{\omega}\setminus\llbracket\varphi\rrbracket$ (resp., $L_{a}(m)\cdot\textsc{Act}^{\omega}=\llbracket\varphi\rrbracket$). 2. 2.

For every reactive parallel monitor $m$, there are $\varphi\in\textsc{mxHML}$ and $\psi\in\textsc{mnHML}$, such that $l(\varphi),l(\psi)=O(l(m))$, $L_{r}(m)\cdot\textsc{Act}^{\omega}=\textsc{Act}^{\omega}\setminus\llbracket\varphi\rrbracket$, and $L_{a}(m)\cdot\textsc{Act}^{\omega}=\llbracket\psi\rrbracket$. 3. 3.

For every $\varphi\in\textsc{sHML}$ (resp., $\varphi\in\textsc{cHML}$), there is a regular monitor $m$, such that $l(m)=O(l(\varphi))$ and $L_{r}(m)\cdot\textsc{Act}^{\omega}=\textsc{Act}^{\omega}\setminus\llbracket\varphi\rrbracket$ (resp., $L_{a}(m)\cdot\textsc{Act}^{\omega}=\llbracket\varphi\rrbracket$). 4. 4.

For every regular monitor $m$, there are $\varphi\in\textsc{sHML}$ and $\psi\in\textsc{cHML}$, such that $l(\varphi),l(\psi)=O(m)$, $L_{r}(m)\cdot\textsc{Act}^{\omega}=\textsc{Act}^{\omega}\setminus\llbracket\varphi\rrbracket$, and $L_{a}(m)\cdot\textsc{Act}^{\omega}=\llbracket\psi\rrbracket$.

We say that a logical fragment is monitorable for a monitoring system, such as parallel or regular monitors, when for each of the fragment’s formulae there is a monitor that detects exactly the satisfying or violating traces for that formula. One of the consequences of Thm. 2.1 is that the fragments defined in Defs. 9 and 10 are semantically the largest monitorable fragments of recHML for parallel and regular monitors, respectively. As we will see in Sec. 3, every parallel monitor has a verdict equivalent regular monitor (Props. 3 and 4), and therefore all formulae in mnHML and mxHML can be translated into equivalent cHML and sHML formulae respectively, as Thm. 5.1 later on demonstrates. However, Thm. 5.2 to follow shows that the cost of this translation is significant.

3 Monitor Transformations: Upper Bounds

In this section we explain how to transform a parallel monitor into a regular or deterministic monitor, and what is the cost, in monitor size, of this transformation. The various relevant transformations, including some from [3] and [9, 11], are summarized in Fig. 3, where each edge is labelled with the best-known worst-case upper bounds for the cost of the corresponding transformation in Fig. 3 (AFA abbreviates alternating finite automaton [9]). As we see in [4, 3] and in Sec. 4, these bounds cannot be improved significantly.

Proposition 1 ([5])

For every reactive parallel monitor $m$, there are an alternating automaton that recognizes $L_{a}(m)$ and one that recognises $L_{r}(m)$, with $O(l(m))$ states.

Proof

The construction from [5, Proposition 3.6] gives an automaton that has the submonitors of $m$ as states. The automaton’s transition function corresponds to the semantics of the monitor. ∎

Corollary 1** (Corollary 3.7 of [5])**

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

Proposition 2

For every reactive and closed parallel monitor $m$, there exists a verdict equivalent regular monitor $n$ such that $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. 1. From these NFAs, we can construct regular monitors $m_{R}^{a}$ and $m_{R}^{r}$, such that $m_{R}^{a}$ recognizes $L_{a}(m)$ positively and $m_{R}^{r}$ recognizes $L_{r}(m)$ negatively, and $l(m_{R}^{a}),l(m_{R}^{r})=2^{O\left(l(m)\cdot 2^{l(m)}\right)}$ [4, Theorem 2]. Therefore, $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 constructions from [5] include a determinization result, based on [3].

Theorem 3.1 (Corollary 3 of [4])

For every consistent closed regular monitor $m$, there is a deterministic monitor $n$ such that $n\simeq_{\text{v}}m$ and $l(n)=2^{2^{O(l(m))}}$.

Proposition 3 (Proposition 3.11 of [5])

For every consistent reactive and closed 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)}}}$.

However, the bound given by Prop. 3 for the construction of deterministic regular monitors from parallel ones is not optimal, as we observe below.

Proposition 4

For every consistent reactive and closed parallel monitor $m$, there is a deterministic monitor $n$ such that $n\simeq_{\text{v}}m$ and $l(n)={2^{2^{2^{O\left(l(m)\right)}}}}$.

In the following Sec. 4, we see that the upper bounds of Props. 2 and 4 are tight, even for monitors that can only accept or reject, and even when the constructed regular or deterministic monitor is only required to be $\omega$-verdict equivalent to the starting one, and not necessarily verdict equivalent, to the original parallel monitor. As we only need to focus on acceptance monitors, in the following we say that a monitor recognizes a language to mean that it recognizes the language positively.

4 Lower Bounds

We now prove that the transformations of Sec. 3 are optimal, by establishing the corresponding lower bounds. To this end, we introduce a family of suffix-closed languages L_{A}^{k}\subseteq\{0,1,e,\,#}^{*}$. Each$L_{A}^{k}is a variation of a language introduced in [[9](#bib.bib9)] to prove the2^{2^{o(n)}}$ lower bound for the transformation from an alternating automaton to a deterministic one. In this section, we only need to consider closed monitors, and as such, all monitors are assumed to be closed.

A variation of the language that was introduced in [9] is the following:

[TABLE]

An alternating automaton that recognizes $L_{V}^{k}$ can nondeterministically skip to the first occurrence of $w$ and then verify that, for every number $i$ between [math] and $k-1$, the $i$’th bit matches the $i$’th bit after the \$$ symbol. This verification can be done using up to O(k)$states, to count the position$i$of the bit that is checked. On the other hand, a DFA that recognizes$L_{V}^{k}$must remember all possible candidates for$w$that have appeared before$$$, and hence requires$2^{2^{k}}$states. We can also conclude that any NFA for$L_{V}^{k}$must have at least$2^{k}$ states, because a smaller NFA could be determinized to a smaller DFA.

A gap language

For our purposes, we use a similar family $L_{A}^{k}$ of suffix-closed languages, which are designed to be recognized by small parallel monitors, but such that each regular monitor recognizing $L_{A}^{k}$ must be “large”. We fix two numbers $l,k\geq 0$, such that $k=2^{l}$. First, we observe that we can encode every string $w\in\{0,1\}^{k}$ as a string $a_{1}\alpha_{1}a_{2}\alpha_{2}\cdots a_{k}\alpha_{k}\in\{0,1\}^{(l+1)\cdot k}$, where $a_{1}a_{2}\cdots a_{k}$ is a permutation of $\{0,1\}^{l}$ and, for all $i$, $\alpha_{i}\in\{0,1\}$. Then, $a_{i}\alpha_{i}$ gives the information that, for $j$ being the number with binary representation $a_{i}$, the $j$’th position of $w$ holds bit $\alpha_{i}$. Let

[TABLE]

Let $w,w^{\prime}\in W$, where $w=a_{1}\alpha_{1}a_{2}\alpha_{2}\cdots a_{k}\alpha_{k}$ and $w^{\prime}=b_{1}\beta_{1}b_{2}\beta_{2}\cdots b_{k}\beta_{k}$, and for $1\leq i\leq k$, $a_{i},b_{i}\in\{0,1\}^{l}$ and $\alpha_{i},\beta_{i}\in\{0,1\}$. We define $w\equiv w^{\prime}$ to mean that for every $i,j\leq k$, $a_{i}=b_{j}$ implies $\alpha_{i}=\beta_{j}$. Let $a=\alpha_{0}\ldots\alpha_{l-1}\in\{0,1\}^{l}$; then, $enc(a)=bin(0)\alpha_{0}\ldots bin(l-1)\alpha_{l-1}$ is the ordered encoding of $a$, where $bin(i)$ is the binary encoding of $i$. Then, $w\in W$ is called an encoding of $a$ if $w\equiv enc(a)$.

Let $\Sigma=\{0,1,\#\}$ and \Sigma_{\}=\Sigma\cup{$}$. Then,

[TABLE]

In other words, a finite trace is in $L_{A}^{k}$ exactly when it has a substring of the form \#w\#v\u^{\prime}#w^{\prime}#$$, where$w$and$w^{\prime}$are encodings of the same string and there is only one$$$between them. Intuitively,$#$is there to delimit bit-strings that may be elements of$W$, and$$$delimits sequences of such bit-strings. So, the language asks if there are two such consecutive sequences where the last bit-string of the second sequence comes from$W$and matches an element from the first sequence. We observe that$L_{A}^{k}$ is suffix-closed.

Lemma 5

$s\in L_{A}^{k}$* if and only if \forall t.~{}st\in L_{A}^{k}\cdot\Sigma_{\}^{\omega}$.*

Conventions

For the conclusions of Lem. 3 to hold, monitors need to be reactive. However, a reactive monitor can have a larger syntactic description than an equivalent non-reactive one, e.g., $\alpha.\textsf{yes}$ vs. $\alpha.\textsf{yes}+\beta.\textsf{end}+\gamma.\textsf{end}$, when $\textsc{Act}=\{\alpha,\beta,\gamma\}$. This last monitor is also verdict equivalent to $\alpha.\textsf{yes}+\textsf{end}$. In what follows, for brevity and clarity, whenever we write a sum $s$ of a monitor of the form $\alpha.m$, we will mean $s+\textsf{end}$, which is reactive, so it can be safely used with a parallel operator, and is verdict equivalent to $s$. We use set-notation for monitors: for $A\subseteq\textsc{Act}$, $A.m$ stands for $\sum_{\alpha\in A}\alpha.m$ (or $\sum_{\alpha\in A}\alpha.m+\textsf{end}$ under the above convention). Furthermore, we define $\{0,1\}^{0}.m=m$ and $\{0,1\}^{i+1}.m=0.\{0,1\}^{i}.m+1.\{0,1\}^{i}.m$. Notice that $l(\{0,1\}^{i}.m)=2^{i}\cdot l(m)+5\cdot(2^{i}-1)$. We can also similarly define $T.m$ for $T\subseteq\{0,1\}^{i}$.

Auxiliary monitors

We start by defining auxiliary monitors. Given a (closed) monitor $m$, let

[TABLE]

These monitors read the trace until they reach a certain symbol, and then they activate submonitor $m$. We can think that $skip_{\#}(m)$ nondeterministically skips to some occurrence of $\#$ that comes before the first occurrence of \$$; next_{#}(m)$and$next_{$}(m)$respectively skip to the next occurrence of$#$and$$$; and$skip_last(m)$skips to the last occurrence of$#$before the next occurrence of$#$$.

Lemma 6

$skip_{\#}(m)$* accepts $g$ iff there are $s$ and $h$, such that $s\#h=g$, $m$ accepts $h$, and $s\in\{0,1,\#\}^{*}$.*

The following lemmata are straightforward and explain how the remaining monitors defined above are used.

Lemma 7

$next_{\#}(m)$* accepts $g$ iff there are $s$ and $h$, such that $s\#h=g$, $m$ accepts $h$, and $s\in\{0,1\}^{*}$.*

Lemma 8

next_{\}(m)$* accepts$g$iff there are$s$and$h$, such that$s$h=g$,$m$accepts$h$, and$s\in{0,1,#}^{}$.

Lemma 9

$skip\_last(m)$* accepts $g$ iff there are $s,r$, and $h$, such that s\#r\#\h=g$,$m$accepts$r#$h$,$r\in{0,1}^{}$, and$s\in{0,1,#}^{}$.*

The following monitors help us ensure that a bit-string from $\{0,1\}^{(l+1)\cdot k}$ is actually a member of $W$. Monitor $all$ ensures that all bit positions appear in the bit-string; $no\_more(s)$ assures us that the bit position $s$ does not appear any more in the remainder of the bit-string; and $unique$ guarantees that each bit position appears at most once. Monitor $perm$ combines these monitors together.

[TABLE]

for $s\in\{0,1\}^{l}$,

[TABLE]

[TABLE]

[TABLE]

The purpose of $perm$ is to ensure that a certain block of bits before the appearance of the $\#$ symbol is a member of the set $W$: it accepts $w\#$ exactly when $w$ is a sequence of blocks of bits with length exactly $l+1$ (by $unique$) and for every $a\in\{0,1\}^{l}$ there is some $\alpha\in\{0,1\}$ such that $a\alpha$ is one of these blocks (by $all$), and that for each such $a$ only one block is of the form $a\alpha^{\prime}$ (by $unique$).

Lemma 10

$perm$* accepts $g$ iff $w\#$ is a prefix of $g$, for some $w\in W$.*

Lemma 11

$l(perm)={O(k^{2})}$.

Given a block $s$ of $l+1$ bits, monitor $find(s)$ accepts a sequence of blocks of $l+1$ bits $w$ exactly when $s$ is one of the blocks of $w$:

[TABLE]

Lemma 12

For $s\in\{0,1\}^{l+1}$, $find(s)$ accepts $g$ if and only if there is some $r\in(\{0,1\}^{l+1})^{*}$, such that $rs$ is a prefix of $g$.

For $s\in\{0,1\}^{l+1}$, $match(s)$ ensures that right before the second occurrence of \$$, there is a #w#$, where$w\in({0,1}^{l+1})^{+}$and$s$is a$(l+1)$-bit block in$w$.

[TABLE]

Lemma 13

For $s\in\{0,1\}^{l+1}$, $match(s)$ accepts $g$ if and only if there are r\r^{\prime}#w#$h=g$, such that$r,r^{\prime}\in\Sigma^{}$,$w\in{0,1}^{}$, and there is a prefix$w^{\prime}s$of$w$, such that$w^{\prime}\in({0,1}^{l+1})^{}$.*

Recognizing $L_{A}^{k}$ with a parallel monitor

We can now define a parallel acceptance-monitor of length $O(k^{2})$ that recognizes $L_{A}^{k}$. Monitor $matching$ ensures that every one of the consecutive blocks of $l+1$ bits that follow, also appears in the block of bits that appears right before the occurrence of \#\$$ that follows the next $$(and that there is no other$$$between these$$$and$#$$). Therefore, if what follows from the current position in the trace and what appears right before that occurrence of$#$$are elements$w,w^{\prime}$of$W$,$matching$ensures that$w\equiv w$. Then,$m_{A}^{k}$nondeterministically chooses an occurrence of$#$, it verifies that the block of bits that follows is an element$w$of$W$that ends with$#$, and that what follows is of the form$v$u^{\prime}#w^{\prime}#$v^{\prime}$, where$u^{\prime},v\in\Sigma^{*},\ w^{\prime}\in W,\ \text{ and }w\equiv w^{\prime}$, which matches the description of$L_{A}^{k}$.

[TABLE]

Lemma 14

$m_{A}^{k}$* recognizes $L_{A}^{k}$ and $l(m_{A}^{k})=O(k^{2})$.*

Proof

The lemma follows from this section’s previous lemmata and from counting the sizes of the various monitors that we have constructed. ∎

Lemma 15

If $m$ is a deterministic monitor that recognizes L_{A}^{k}\cdot\Sigma_{\}^{\omega}$, then

[TABLE]

Thm. 4.1 gathers our conclusions about $L_{A}^{k}$.

Theorem 4.1

For every $k>0$, $L_{A}^{k}$ is recognized by an alternating automaton of $O(k^{2})$ states and a parallel monitor of length $O(k^{2})$, but by no DFA with $2^{o(2^{k})}$ states and no deterministic monitor of length $2^{o(2^{2^{k-1}+k})}$. L_{A}^{k}\cdot\Sigma_{\}^{\omega}$is recognized by a parallel monitor of length$O(k^{2})$, but by no deterministic monitor of length$2^{o(2^{2^{k-1}+k})}$.

Proof

Lem. 14 informs us that there is a parallel monitor $m$ of length $O(k^{2})$ that recognizes $L_{A}^{k}$. Therefore, it also recognizes L_{A}^{k}\cdot\Sigma_{\}^{\omega}by [Lem. 1](#Thmlemma1). [Prop. 1](#Thmproposition1) tells us thatm$can be turned into an alternating automaton with$l(m)=O(k^{2})$states that recognizes$L_{A}^{k}. [Lem. 15](#Thmlemma15) yields that there is no deterministic monitor of length 2^{o(2^{2^{k-1}+k})}that recognizes that language. From [[4](#bib.bib4)], we know that if there were a DFA with2^{o(2^{k})}$states that recognizes$L_{A}^{k}$, then there would be a deterministic monitor of length$2^{2^{o(2^{k})}}$that recognizes$L_{A}^{k}$, which, as we argued, cannot exist. ∎

Hardness for regular monitors

Proposition 4.1 does not guarantee that the $2^{O(n\cdot 2^{n})}$ upper bound for the transformation from a parallel monitor to a nondeterministic regular monitor is tight. To prove a tighter lower bound, let $L_{U}^{k}$ be the language that includes all strings of the form \#w_{1}\#w_{2}\#\cdots\#w_{n}\w$where for$i=1,\ldots,n$,$w_{i}\in W$, and$w\in{0,1,#,$}^{*}$, and for every$i<n$,$w_{i}$encodes a string that is smaller than the string encoded by$w_{i+1}$, in the lexicographic order.

Lemma 16

$s\in L_{U}^{k}$* if and only if \forall t.~{}st\in L_{U}^{k}\cdot\Sigma_{\}^{\omega}$.*

We describe how $L_{U}^{k}$ can be recognized by a parallel monitor of size $O(k^{2})$. The idea is that we need to compare the encodings of two consecutive blocks of $l+1$ bits. Furthermore, a string is smaller than another if there is a position in these strings, where the first string has the value [math] and the second $1$, and for every position that comes before that position, the bits of the two strings are the same. We define the following monitors:

[TABLE]

Proposition 5

$m_{U}$* recognizes $L_{U}^{k}$ (and L_{U}^{k}\cdot\Sigma_{\}^{\omega}$) and$|m_{U}|=O(k^{2})$. Every regular monitor that recognizes$L_{U}^{k}$or$L_{U}^{k}\cdot\Sigma_{$}^{\omega}$must be of length$2^{\Omega(2^{k})}$.*

5 Logical Consequences

We now turn our attention back from the two monitoring systems to the corresponding logical fragments. We observe that the bounds that we have proved in the previous sections also apply when we discuss formula translations. A version of Thm. 5.1 was proven in [5], but without complexity bounds.

Theorem 5.1

For every $\varphi\in\textsc{mnHML}$ (resp., $\varphi\in\textsc{mxHML}$), there is some $\psi\in\textsc{cHML}$ (resp., $\psi\in\textsc{sHML}$), such that $l(\psi)=2^{O(l(m)\cdot 2^{l(m)})}$ and $\llbracket\varphi\rrbracket=\llbracket\psi\rrbracket$.

Proof

We prove the case for $\varphi\in\textsc{mnHML}$, as the case for $\varphi\in\textsc{mxHML}$ is similar. By Thm. 2.1, we know that there is a reactive parallel monitor $m$, such that $L_{a}(m)\cdot\textsc{Act}^{\omega}=\llbracket\varphi\rrbracket$ and $l(m)=O(l(\varphi))$. By Prop. 2, we know that there is a regular monitor $n$, such that $L_{a}(n)=L_{a}(m)$ and $l(n)=2^{O(l(m)\cdot 2^{l(m)})}$. We can then see that $l(n)=2^{O(l(\varphi)\cdot 2^{l(\varphi)})}$. According to Thm. 2.1, there is a formula $\psi\in\textsc{cHML}$, such that $\llbracket\psi\rrbracket=L_{a}(n)\cdot\textsc{Act}^{\omega}=L_{a}(m)\cdot\textsc{Act}^{\omega}=\llbracket\varphi\rrbracket$, and $l(\psi)=O(l(n))$, yielding that $l(\psi)=2^{O(l(\varphi)\cdot 2^{l(\varphi)})}$. ∎

The cost of the construction in the proof of Thm. 5.1 is due to the regularization of the monitor. Our lower bounds — and specifically Prop. 5 — demonstrate that this construction is optimal, because a better construction of $\psi$ from $\varphi$ would lower the cost of regularization via the synthesis functions.

Theorem 5.2

There is some $\varphi\in\textsc{mxHML}$, such that for every $\psi\in\textsc{sHML}$, if $\llbracket\varphi\rrbracket=\llbracket\psi\rrbracket$, then $l(\psi)=2^{\Omega\left(2^{\sqrt{l(\varphi)}}\right)}$.

Proof (Sketch)

Otherwise, we could regularize $m_{U}$ from Sec. 4 more efficiently than Prop. 5 allows, by first turning $m_{U}$ to $\varphi\in\textsc{mxHML}$, then to $\psi\in\textsc{sHML}$, and finally to a regular monitor $m$. The full proof is in the appendix. ∎

Remark 2

We observe that to prove Thm. 5.2, it was necessary to prove Prop. 5 for regular monitors that are $\omega$-verdict equivalent, and not just verdict equivalent, to $m_{U}$. The reason is that, in the proof of Thm. 5.2, the monitor $m$ that monitors for $\psi$ is $\omega$-verdict equivalent to $m_{U}$ and there is no guarantee that it is, in fact, verdict equivalent to $m_{U}$. $\hfill\squareforqed$

Remark 3

In [3], the authors define a deterministic fragment of sHML, which they then show to be equivalent to the full sHML. We can claim analogous bounds for translating formulae into this smaller fragment, using similar arguments to those used above. We omit a full exposition of this claim. $\hfill\squareforqed$

6 Conclusion

We determined the cost of turning a parallel monitor into an equivalent regular, or deterministic, monitor. As a result, we saw that, over infinite traces, mxHML is doubly-exponentially more succinct than sHML.

Regular monitors were introduced in [12] to monitor for sHML over processes. The cost of determinization of regular monitors was examined in [4, 3]. Aceto et al. in [6] used a similar determinization process on formulae in the context of enforcement.

In [5], we also synthesized tight monitors, which are monitors that reach a verdict as soon as they have analysed enough information from the trace, and not later. It is often important to reach a verdict as soon as possible, but it is also important to avoid burdening a monitored system with a very large monitor. Therefore, it would also be of interest to determine how much it costs to turn a parallel or regular monitor into a verdict-equivalent tight monitor. This is a topic that we leave for future work.

Appendix

This appendix gathers the omitted proofs from the main text of this paper.

Omitted Proofs from Sec. 3

Proof (of Cor. 1)

The alternating automaton that is constructed in the proof of Prop. 1 has at most as many states as there are submonitors in $m$ which, in turn, are no more than $l(m)$. To conclude, every alternating automaton with $k$ states can be converted into an NFA with at most $2^{k}$ states that recognises the same language [9, 11]. ∎

The following technical lemmata help in proving the improved upper bound in Prop. 4.

Lemma 17

Let $m$ be a regular monitor and $n$ a submonitor of $m$, such that $n$ is a sum of $\alpha.\textsf{yes}$ and of $\beta.\textsf{yes}$. Then, there is some $s\in\textsc{Act}^{*}$, such that $m$ accepts both $s\alpha$ and $s\beta$.

Proof

By straightforward induction on the construction of $m$ from $n$. ∎

Remark 4

Monitor $m_{\tau}$ from Remark 1 demonstrates that Lem. 17 does not hold for parallel monitors, and so does $\textsf{no}{\otimes}(a.\textsf{yes}+b.\textsf{yes})$. $\hfill\squareforqed$

Lemma 18

Let $m$ be a closed regular monitor that does not have any submonitor of the form $\textsf{rec}\,x.\textsf{yes}$, and let $m^{\prime}$ be a submonitor of $m$. If $m^{\prime}\xRightarrow{\;\;}\textsf{yes}$, then $m^{\prime}=\textsf{yes}$.

Proof

If $m^{\prime}\xRightarrow{\;\;}\textsf{yes}$, then $m^{\prime}\xrightarrow{\;\tau\;}^{k}\textsf{yes}$ for some $k\geq 0$. We prove that if $k>0$, then $\textsf{rec}\,x.\textsf{yes}$ is a submonitor of $m$. If $k=1$, then $m^{\prime}$ is a sum of $\textsf{rec}\,x.\textsf{yes}$, and so $\textsf{rec}\,x.\textsf{yes}$ is a submonitor of $m^{\prime}$, and therefore of $m$. If $m^{\prime}\xrightarrow{\;\tau\;}n$ and $n\xrightarrow{\;\tau\;}^{k-1}\textsf{yes}$, then by Lem. 2, $n$ is a submonitor of $m$, so $\textsf{rec}\,x.\textsf{yes}$ is a submonitor of $n$ by induction, and therefore of $m$. ∎

Proof (of Prop. 4)

We recall that, in the proof of Prop. 3 given in [5], the construction starts from a consistent reactive parallel monitor $m$ and turns it into two NFAs $A_{a}$ and $A_{r}$, such that $L(A_{a})=L_{a}(m)$, $L(A_{r})=L_{r}(m)$, and the number of states in $A_{a}$ and in $A_{r}$ is at most $2^{O(l(m))}$ (Cor. 1). Then, these automata can be turned into regular monitors $m_{a}$ and $m_{r}$, and we can conclude by determinizing $m^{a}_{R}+m^{r}_{R}$. To improve the upper bound for the construction, we determinize starting from the NFAs. Let $A_{a}=(Q_{a},\textsc{Act},\delta_{a},q_{0}^{a},F_{a})$ and $A_{r}=(Q_{r},\textsc{Act},\delta_{r},q_{0}^{r},F_{r})$.

We first construct a new NFA111For clarity, the construction of the NFA $N$ makes a mild use of $\varepsilon$-transitions., $N=(Q,\textsc{Act}\cup\{\heartsuit,\spadesuit,\varepsilon\},\delta,q_{0},F)$, such that: $Q=\{q_{0},f\}\sqcup Q_{a}\sqcup Q_{r}$, where $\sqcup$ stands for disjoint union; $F=\{f\}$; and

[TABLE]

It is not hard to see that the set of minimal traces in $L(N)$, with respect to the prefix order, is $\min L(N)=L(A_{a})\cdot\{\heartsuit\}~{}\cup~{}L(A_{r})\cdot\{\spadesuit\}$.

From [4, Theorem 2], there is a deterministic (closed) monitor $n^{\prime}$, such that $L_{a}(n^{\prime})=L(N)$ and $l(n^{\prime})=2^{2^{O(|Q|)}}=2^{2^{2^{O(l(m))}}}$. We observe that there cannot be a submonitor of $n^{\prime}$ that is a sum both of $\heartsuit.\textsf{yes}$ and of $\spadesuit.\textsf{yes}$ — otherwise, by Lem. 17, $L_{a}(m)\cap L_{r}(m)\neq\emptyset$, which is a contradiction, because $m$ is consistent. We further assume that $n^{\prime}$ has no submonitors of the form $\textsf{rec}\,x.\textsf{yes}$, $\textsf{rec}\,x.\textsf{no}$, as these can be replaced by yes and no, respectively, yielding an equivalent monitor. Let $n$ be the result of replacing in $n^{\prime}$ all maximal sums of $\heartsuit.\textsf{yes}$ by yes and of $\spadesuit.\textsf{yes}$ by no. In particular, there are monitor variables $x_{1},\ldots,x_{k},y_{1},\ldots,y_{l}$ that do not appear in $n^{\prime}$ and an open monitor $n_{o}(x_{1},\ldots,x_{k},y_{1},\ldots,y_{l})$, such that $n^{\prime}=n_{o}(s_{1},\ldots,s_{k},s^{\prime}_{1},\ldots,s^{\prime}_{l})$, where $s_{1},\ldots,s_{k}$ are (all the occurrences of) sums of $\heartsuit.\textsf{yes}$ in $n^{\prime}$, $s^{\prime}_{1},\ldots,s^{\prime}_{l}$ are (all the occurrences of) sums of $\spadesuit.\textsf{yes}$ in $n^{\prime}$, and $n=n_{o}(\textsf{yes},\ldots,\textsf{yes})$. We prove that $\min L_{a}(n^{\prime})=L_{a}(n)\cdot\{\heartsuit\}~{}\cup~{}L_{r}(n)\cdot\{\spadesuit\}$.

Let $w\in\min L_{a}(n^{\prime})$. Because $L_{a}(n^{\prime})=L(N)$, we know that $w\in L(N)$, and therefore $w\in L(A_{a})\cdot\{\heartsuit\}~{}\cup~{}L(A_{r})\cdot\{\spadesuit\}$. So, it is either the case that $w=w^{\prime}\heartsuit$ for $w^{\prime}\in L_{a}(A_{a})$, or that $w=w^{\prime}\spadesuit$ for $w^{\prime}\in L_{a}(A_{a})$ — w.l.o.g. we assume the first case. Therefore, $n^{\prime}\xRightarrow{\;w^{\prime}\heartsuit\;}\textsf{yes}$ and since $w\in\min L_{a}(n^{\prime})$, $n^{\prime}\centernot{\xRightarrow{\;w^{\prime}\;}}\textsf{yes}$. We demonstrate that $n\xRightarrow{\;w^{\prime}\;}\textsf{yes}$. Specifically, we prove by induction on an arbitrary submonitor $n^{\prime}_{o}=n^{\prime}_{o}(x_{1},\ldots,x_{k},y_{1},\ldots,y_{l})$ of $n_{o}(x_{1},\ldots,x_{k},y_{1},\ldots,y_{l})$ that if $n_{s}=n^{\prime}_{o}(s_{1},\ldots,s_{k},s^{\prime}_{1},\ldots,s^{\prime}_{l})\xRightarrow{\;w^{\prime}\heartsuit\;}\textsf{yes}$ and $n_{s}\centernot{\xRightarrow{\;w^{\prime}\;}}\textsf{yes}$ for some $w^{\prime}\in\textsc{Act}^{*}$, then $n_{y}=n^{\prime}_{o}(\textsf{yes},\ldots,\textsf{yes})\xRightarrow{\;w^{\prime}\;}\textsf{yes}$.

The base cases are:

$n^{\prime}_{o}$ is a verdict, which is immediate, because the claim’s assumptions cannot both hold; or $n^{\prime}_{o}=x_{i}$, in which case $n_{y}=\textsf{yes}$.

If for some $\alpha\in\textsc{Act}\cup\{\heartsuit,\spadesuit\}$, $n^{\prime}_{o}=\alpha.n^{\prime\prime}$

and $n_{s}\xRightarrow{\;w^{\prime}\heartsuit\;}\textsf{yes}$ and $n_{s}\centernot{\xRightarrow{\;w^{\prime}\;}}\textsf{yes}$, then there are two cases. In the first case, $\alpha=\heartsuit$. Then, as $w^{\prime}\in\textsc{Act}^{*}$, we have that $w^{\prime}=\varepsilon$, so $n^{\prime\prime}(s_{1},\ldots,s_{k},s^{\prime}_{1},\ldots,s^{\prime}_{l})\xRightarrow{\;\;}\textsf{yes}$, and by Lem. 18 ($n_{s}$ is a submonitor of $n^{\prime}$), $n^{\prime\prime}(s_{1},\ldots,s_{k},s^{\prime}_{1},\ldots,s^{\prime}_{l})=\textsf{yes}$, and therefore $n^{\prime}_{o}=\heartsuit.\textsf{yes}$, which contradicts our definitions. Otherwise, for $\alpha\neq\heartsuit$, $w^{\prime}=\alpha~{}w^{\prime\prime}$, and $n^{\prime\prime}(s_{1},\ldots,s_{k},s^{\prime}_{1},\ldots,s^{\prime}_{l})\xRightarrow{\;w^{\prime\prime}\heartsuit\;}\textsf{yes}$ and $n^{\prime\prime}(s_{1},\ldots,s_{k},s^{\prime}_{1},\ldots,s^{\prime}_{l})\centernot{\xRightarrow{\;w^{\prime\prime}\;}}\textsf{yes}$. By the inductive hypothesis, $n^{\prime\prime}(\textsf{yes},\ldots,\textsf{yes})\xRightarrow{\;w^{\prime\prime}\;}\textsf{yes}$, and therefore $n_{y}\xRightarrow{\;w^{\prime}\;}\textsf{yes}$.

If $n^{\prime}_{o}=n_{1}+n_{2}$

and $n_{s}\xRightarrow{\;w^{\prime}\heartsuit\;}\textsf{yes}$ and $n_{s}\centernot{\xRightarrow{\;w^{\prime}\;}}\textsf{yes}$, then we know that $n_{s}$ is not a sum of $\heartsuit.\textsf{yes}$. Therefore, w.l.o.g. $n_{1}(s_{1},\ldots,s_{k},s^{\prime}_{1},\ldots,s^{\prime}_{l})\xRightarrow{\;w^{\prime}\heartsuit\;}\textsf{yes}$ and $n_{1}(s_{1},\ldots,s_{k},s^{\prime}_{1},\ldots,s^{\prime}_{l})\centernot{\xRightarrow{\;w^{\prime}\;}}\textsf{yes}$, and we are done by the inductive hypothesis.

The case for $n^{\prime}_{o}=\textsf{rec}\,x.n^{\prime\prime}$

is more straightforward, as $n^{\prime}_{o}$ and $n^{\prime\prime}$ have the same weak transitions.

We now prove that if $w\in L_{a}(n)\cdot\{\heartsuit\}~{}\cup~{}L_{r}(n)\cdot\{\spadesuit\}$, then $w\in\min L_{a}(n^{\prime})$. Let $w\in L_{a}(n)\cdot\{\heartsuit\}$ (the case for $w\in L_{r}(n)\cdot\{\spadesuit\}$ is symmetric). Then there is a $w^{\prime}\in L_{a}(n)$, such that $w=w^{\prime}.\heartsuit$. Let $w^{\prime\prime}$ be the shortest prefix of $w^{\prime}$, such that $w^{\prime\prime}\in L_{a}(n)$. We observe that if $w^{\prime\prime}.\heartsuit\in\min L_{a}(n^{\prime})$, then $w^{\prime\prime}.\heartsuit\in\min L(N)$, and therefore $w^{\prime\prime}\in L(A_{a})$, yielding that $w^{\prime}\in L(A_{a})$, because $A_{a}$ is suffix-closed (by verdict-persistence, Lem. 1), and therefore $w=w^{\prime}.\heartsuit\in\min L_{a}(n^{\prime})$. Furthermore, if $w^{\prime\prime}.\heartsuit\in L_{a}(n^{\prime})$, we can see that $w^{\prime\prime}.\heartsuit\in\min L_{a}(n^{\prime})$, as $w^{\prime\prime}\in\textsc{Act}^{*}$. Thus, it suffices to prove that $w^{\prime\prime}.\heartsuit\in L_{a}(n^{\prime})$. By induction on the derivation, and due to the minimality of $w^{\prime\prime}$, we can see that either $n_{o}(x_{1},\ldots,x_{k},y_{1},\ldots,y_{l})\xRightarrow{\;w^{\prime\prime}\;}\textsf{yes}$, in which case $n^{\prime}\xRightarrow{\;w^{\prime\prime}\;}\textsf{yes}$, and therefore $n^{\prime}\xRightarrow{\;w^{\prime\prime}.\heartsuit\;}\textsf{yes}$, or $n_{o}(x_{1},\ldots,x_{k},y_{1},\ldots,y_{l})\xRightarrow{\;w^{\prime\prime}\;}x_{i}$ for some $x_{i}$, in which case $n^{\prime}\xRightarrow{\;w^{\prime\prime}\;}s^{\prime}_{i}$, where $s^{\prime}_{i}$ is $s_{i}$ after applying a number of steps substituting variables for monitors. As $s_{i}$ is a sum of $\heartsuit.\textsf{yes}$, so is $s^{\prime}_{i}$, therefore $s^{\prime}_{i}\xrightarrow{\;\heartsuit\;}\textsf{yes}$.

We just demonstrated that $\min L_{a}(n^{\prime})=L_{a}(n)\cdot\{\heartsuit\}~{}\cup~{}L_{r}(n)\cdot\{\spadesuit\}$. But we have also seen that $L_{a}(n^{\prime})=L(N)$ and that $\min L(N)=L(A_{a})\cdot\{\heartsuit\}~{}\cup~{}L(A_{r})\cdot\{\spadesuit\}$, and therefore $L_{a}(n)=L(A_{a})=L_{a}(m)$ and $L_{r}(n)=L(A_{r})=L_{r}(m)$, which is what we wanted to show. ∎

Omitted Proofs from Sec. 4

Proof (of Lem. 5)

The “only if” direction is immediate, and therefore we only show the “if” direction. Let $s$ be such that \forall t.~{}st\in L_{A}^{k}\cdot\Sigma_{\}^{\omega}$. From our assumptions about$s$,$s#^{\omega}\in L_{A}^{k}\cdot\Sigma_{$}^{\omega}$. According to the definition of$L_{A}^{k}$, there must be a finite prefix$r$of$s#^{\omega}$, such that$r\in L_{A}^{k}$and ends with$$$. Since the only symbol in$#^{\omega}$is$#$,$r$is a prefix of$s$. Therefore, since$L_{A}^{k}$is suffix-closed, we conclude that$s\in L_{A}^{k}$. ∎

Proof (of Lem. 6)

The “if” direction is straightforward, using Lem. 3. For the “only if” direction, notice that the $\#.m$ component of the monitor is the only component that can produce a yes verdict, and it activates at the occurrences of the $\#$ symbol. Therefore, if $skip_{\#}(m)$ accepts $g$, there must be some $s\#h=g$, such that $m$ accepts $h$. Let $s$ be minimal for this to happen.

We now prove by contradiction that $s\in\{0,1,\#\}^{*}$. If that is not the case, \$$ appears in s$, so there are$s_{1}$s_{2}=s$. When reading$s_{1}$$, all monitor components of$skip_{#}(m)$must fail (reach end), except the ones that have come from$#.m$. Therefore, we can split$g$as$s_{1}#h^{\prime}=g$, such that$m$accepts$h^{\prime}$, which is a contradiction, due to the assumed minimality of$s$. Therefore,$s\in{0,1,#}^{*}$. ∎

Hardness of $L_{A}^{k}$ for deterministic monitors

We introduce the notion of a simple trace. As Lem. 19 reveals, the cardinality of a set of simple traces gives a lower bound on the size of a regular monitor.

Definition 11

We call a derivation $m\xRightarrow{\;s\;}m^{\prime}$ simple, if rules RecB and Ver are not used in the proof of any transition of the derivation. We say that a trace s\in\Sigma_{\}^{*}$is simple for monitor$m$if there is a simple derivation$m\xRightarrow{;s;}m^{\prime}$. We say that a set of simple traces for$m$is simple for$m$.$\hfill\blacksquare$

Lemma 19 (Lemma 20 from [3])

Let $m$ be a regular monitor and $G$ a (finite) simple set of traces for $m$. Then, $l(m)\geq|G|$. ∎

The following Lems. 20 and 21 are variations of the Pumping Lemma for monitors.

Lemma 20 (Lemma 22 from [3])

Let $m\xRightarrow{\;s\;}n$, such that $m$ is regular and $s$ is not simple for $m$. Then, there are $s=s_{1}s_{2}s_{3}$, such that $|s_{2}|>0$ and for every $i\geq 0$, $m\xRightarrow{\;s_{1}s_{2}^{i}s_{3}\;}n$. ∎

Lemma 21 (Lemma 27 from [3])

Let $m\xRightarrow{\;s\;}m^{\prime}$, such that $s$ is not simple for $m$ and $m$ is deterministic (and regular). Then, there are $s=s_{1}s_{2}s_{3}$ and monitor $n$, such that $|s_{2}|>0$ and $m\xRightarrow{\;s_{1}\;}n\xRightarrow{\;s_{2}\;}n\xRightarrow{\;s_{3}\;}m^{\prime}$.

Fix a partition $\{C,D\}$ of $\{0,1\}^{k}$, such that $|C|=|D|=2^{k-1}$; let $K=2^{2^{k-1}}$. Let $P_{C}=C_{0}\cdots C_{K-2}$ be a permutation of $2^{C}\setminus\{\emptyset\}$, and $P_{D}=D_{0}\cdots D_{K-2}$ a permutation of $2^{D}\setminus\{\emptyset\}$. For every $0\leq i<K-1$, let

[TABLE]

where $w_{0}w_{1}\cdots w_{|C_{i}|}$ is a permutation of $C_{i}$ and

[TABLE]

where $w^{\prime}_{0}w^{\prime}_{1}\cdots w^{\prime}_{|D_{i}|}$ is a permutation of $D_{i}$. Thus, each $t_{i}$ and $s_{i}$ encodes a permutation of a distinct subset of $\{0,1\}^{k}$. Let

[TABLE]

and let

[TABLE]

Notice that $|T|=((K-1)!)^{2}$.

The following Lem. 22 characterizes trace $t_{K}$, as defined in Sec. 4, and is useful in the proof of Cor. 2, which follows immediately from it.

Lemma 22

If $f\neq g$ are prefixes of $t_{K}$, then there is some h\in\{0,1,\#,\}^{}$, such that$fh\in L_{A}^{k}$iff$gh\notin L_{A}^{k}$.*

Proof

We can assume that $f$ is a proper prefix of $g$. We have the following cases:

The symbol \$$ appears more times in g$than in$f$.

Then, for some $f^{\prime},g^{\prime}\in\Sigma^{*}$ and $0\leq i\leq j$:

• •

$f=f^{\prime}$ and (g=t_{0}\s_{0}$\cdots$s_{j}$g^{\prime}$or$g=t_{0}$s_{0}$\cdots$t_{j}$g^{\prime}$); or

• •

f=t_{0}\s_{0}$\cdots$t_{i}$f^{\prime}$and$g=t_{0}$s_{0}$\cdots$s_{j}$g^{\prime}$; or

• •

f=t_{0}\s_{0}$\cdots$s_{i}$f^{\prime}$and$g=t_{0}$s_{0}$\cdots$t_{j}$g^{\prime}$; or

• •

f=t_{0}\s_{0}$\cdots$t_{i}$f^{\prime}$and$g=t_{0}$s_{0}$\cdots$t_{j}$g^{\prime}$and$i<j$; or

• •

f=t_{0}\s_{0}$\cdots$s_{i}$f^{\prime}$and$g=t_{0}$s_{0}$\cdots$s_{j}$g^{\prime}$and$i<j$.

Then, for all these cases we can immediately see that there is some $w\in W$ that appears in one of $t_{i},s_{i},t_{j},s_{j}$, such that for h=\#w\#\$$, fh\in L_{A}^{k}$iff$gh\notin L_{A}^{k}$.

The symbol $\#$ appears more times in $g$ than in $f$, but $$$ does not.

Then, for some $f^{\prime},g^{\prime}\in\{0,1\}^{*}$,

[TABLE]

Then, for h=\#enc(w_{j})#$$,$gh\in L_{A}^{k}$and$fh\notin L_{A}^{k}$.

The symbols \,#$appear the same number of times in$g$and in$f$.

Then, for some $f^{\prime},g^{\prime}\in\{0,1\}^{*}$,

[TABLE]

and $|g^{\prime}|>0$. Therefore, $f^{\prime}g^{\prime}$ is a prefix of $enc(w_{i+1})$. Let $h_{0}$ be such that $f^{\prime}g^{\prime}h_{0}=enc(w_{i+1})$. Then, for h=h_{0}\#\#enc(w_{i+1})#$$,$gh\in L_{A}^{k}$and$fh\notin L_{A}^{k}$. ∎

Corollary 2

If $s\neq r$ are prefixes of $t_{K}$, then there is some t\in\Sigma_{\}^{\omega}$, such that$st\in L_{A}^{k}\cdot\Sigma_{$}^{\omega}$iff$rt\notin L_{A}^{k}\cdot\Sigma_{$}^{\omega}$.

Proof

By Lems. 22 and 5. ∎

Proposition 6

If $m$ is a deterministic regular monitor that recognizes L_{A}^{k}\cdot\Sigma_{\}^{\omega}$, then$t_{K}$is a simple trace for$m$.

Proof

If $t_{K}$ is not simple, then by Lem. 21, $t_{K}=s_{1}s_{2}s_{3}$, such that $|s_{2}|>0$ and there is a monitor $n$, such that $m\xRightarrow{\;s_{1}\;}n\xRightarrow{\;s_{2}\;}n$. But according to Cor. 2, there is some $t$, such that s_{1}t\in L_{A}^{k}\cdot\Sigma_{\}^{\omega}$iff$s_{1}s_{2}t\notin L_{A}^{k}\cdot\Sigma_{$}^{\omega}$. This is a contradiction, because$s_{1}t\in L_{A}^{k}\cdot\Sigma_{$}^{\omega}$iff$n$accepts$t\cdot\Sigma_{$}^{\omega}$iff$s_{1}s_{2}t\in L_{A}^{k}\cdot\Sigma_{$}^{\omega}$. ∎

Proof (of Lem. 15)

An immediate consequence of Props. 6 and 19. ∎

The hardness of regularization

Proof (of Prop. 5)

First, we sketch the proof of the first part of the proposition. We observe that $smaller$ accepts a trace $w_{1}\#w_{2}t$, where $w_{1},w_{2}\in W$, exactly when $w_{1}$ encodes a smaller sequence than $w_{2}$, with respect to the lexicographic ordering. Then, $m_{U}$ keeps reading blocks of bits between the $\#$ separators, while ensuring that each of these is an element of $W$ (using monitor $perm$), and that it either is the last such block of bits (using monitor $last$), or that it encodes a smaller sequence than the next one (using monitor $smaller$).

It now suffices to prove that, for any ordered sequence $a_{1}a_{2}\cdots a_{c}$ of strings from $\{0,1\}^{k}$, the finite trace $s=\#enc(a_{1})\#enc(a_{2})\#\cdots\#enc(a_{c})$ is simple for any regular monitor that accepts exactly the infinite extensions of $L_{U}^{k}$. If $s$ is not simple for $m$, then, according to Lemma 20, for every $m\xRightarrow{\;s\;}n$, there are $s=s_{1}s_{2}s_{3}$, such that $|s_{2}|>0$ and for every $i\geq 0$, $m\xRightarrow{\;s_{1}s_{2}^{i}s_{3}\;}n$. Therefore, if m\xRightarrow{\;s\;}n\xRightarrow{\;\0^{j};}\textsf{yes}$for some$j\geq 0$, then$m\xRightarrow{;s_{1}s_{2}^{2}s_{3};}n\xRightarrow{;$0^{j};}\textsf{yes}$and$m\xRightarrow{;s_{1}s_{2}^{3}s_{3};}n\xRightarrow{;$0^{j};}\textsf{yes}$. If$|s_{2}|$is not a multiple of$k(l+1)+1$, then it is not hard to see that we reach a contradiction, as$s_{1}s_{2}^{2}s_{3}$0^{j}\notin L_{U}^{k}$, because it includes a block of bits that is not in$W$. Otherwise,$s_{2}$is of the form$f#g$or$f#enc(a_{i})#\cdots#enc(a_{i+j})#g$, where$fg\in{0,1}^{k(l+1)}$and$j\geq 0$. If$gf\notin W$, then$s_{1}s_{2}^{2}s_{3}$0^{j}\notin L_{U}^{k}$, and again, we have a contradiction. But even if$gf\in W$, we see that$gf$appears twice in$s_{1}s_{2}^{3}s_{3}$, and again we have a contradiction, as$s_{1}s_{2}^{3}s_{3}$0^{j}\notin L_{U}^{k}$, because there appear two elements of$W$in$s_{1}s_{2}^{3}s_{3}$ that encode the same string. ∎

Omitted Proofs from Sec. 5

Proof (of Thm. 5.2)

Let $k$ and $m_{U}$ be as defined in Sec. 4. Thm. 2.1 asserts the existence of a formula $\varphi$, such that $l(\varphi)=O(l(m_{U}))$ and \llbracket\varphi\rrbracket=L_{a}(m_{U})\cdot\Sigma_{\}^{\omega}=L_{U}^{k}\cdot\Sigma_{$}^{\omega}$. Now, let$\psi\in\textsc{sHML}$, where$\llbracket\varphi\rrbracket=\llbracket\psi\rrbracket. According to [Thm. 2.1](#S2.Thmtheorem1), there is a regular monitor m$, such that$l(m)=O(l(\psi))$, and$\llbracket\varphi\rrbracket=\llbracket\psi\rrbracket=L_{a}(m)\cdot\Sigma_{$}^{\omega}$. Therefore,$m$recognizes$L_{U}^{k}\cdot\Sigma_{$}^{\omega}, and by [Prop. 5](#Thmproposition5), l(m)=2^{\Omega(2^{k})}=2^{\Omega(2^{\sqrt{l(\varphi)}})}$. This yields that$l(\psi)=2^{\Omega(2^{k})}=2^{\Omega(2^{\sqrt{l(\varphi)}})}$. ∎