Monitoring Hyperproperties With
Prefix Transducers
Monitoring Hyperproperties With Prefix Transducers
Marek Chalupa0000-0003-1132-5516 Thomas A. Henzinger0000-0002-2985-7724

M. Chalupa, T. A. Henzinger
Institute of Science and Technology Austria (ISTA), Klosterneuburg, Austria

Hyperproperties are properties that relate multiple execution traces.
Previous work on monitoring hyperproperties focused on synchronous hyperproperties, usually specified in HyperLTL.
When monitoring synchronous hyperproperties, all traces are assumed to proceed at the same speed.
We introduce (multi-trace) prefix transducers and show how to use them for monitoring synchronous as well as,
for the first time, asynchronous hyperproperties.
Prefix transducers map multiple input traces into one or more output traces
by incrementally matching prefixes of the input traces against expressions similar to regular expressions.
The prefixes of different traces which are consumed by a single matching step of the monitor may have different lengths.
The deterministic and executable nature of prefix transducers makes them more suitable as an intermediate formalism
for runtime verification than logical specifications,
which tend to be highly non-deterministic, especially in the case of asynchronous hyperproperties.
We report on a set of experiments about monitoring asynchronous version of
observational determinism.

§ INTRODUCTION

Hyperproperties [26] are properties that relate multiple execution traces of a system to each other.
One of the most prominent examples of hyperproperties nowadays are the information-flow security policies [52].
Runtime monitoring [1] is a lightweight formal method for analyzing the behavior of a system by checking dynamic
execution traces against a specification.
For hyperproperties, a monitor must check relations between multiple traces.
While many hyperproperties cannot be monitored in general [3, 18, 14, 37, 61],
the monitoring of hyperproperties can still yield useful results, as we may detect their violations [36].

Previous work on monitoring hyperproperties focused on HyperLTL specifications [3, 18], or other synchronous
hyperlogics [2].
Synchronous specifications model processes that progress at the same speed in lockstep, one event on each trace per step.
The synchronous time model has been found overly restrictive for specifying hyperproperties of asynchronous processes,
which may proceed at varying speeds [7, 9, 17, 41].
A more general, asynchronous time model allows multiple traces to proceed at different speeds, independently of each other,
in order to wait for each other only at certain synchronization events.
As far as we know, there has been no previous work on the runtime monitoring of asynchronous hyperproperties.

The important class of $k$-safety hyperproperties [26, 34] can be monitored by processing $k$-tuples of traces [3, 34].
In this work, we develop and evaluate a framework for monitoring hyperproperties under both, synchronous and asynchronous time models.
For this purpose, we introduce (multi-trace) prefix transducers, which map multiple (but fixed) input traces into one or more output traces
by incrementally matching prefixes of the input traces against expressions similar to regular expressions.
The prefixes of different traces which are consumed by a single matching step of the transducer may have different lengths, which allows to proceed on the traces asynchronously.
By instantiating prefix transducers for different combinations of input traces,
we can monitor $k$-safety hyperproperties instead of monitoring only a set of fixed input traces.

The deterministic and executable nature of prefix transducers gives rise to natural monitors. This is in contrast with monitors synthesized
from logical specifications which are often highly non-deterministic, especially in the case of asynchronous (hyper)properties.

nd/.style = align=left,
ev/.style = align=left, rounded corners, scale=0.9,
fill=gray!20, minimum width=1cm
[nd] at (-1.0, 0)
[ev] at (0,   0)  ;
[ev] at (1.8, 0)  ;
[ev] at (3.6, 0)  ;
[ev] at (5.4, 0)  ;

[nd] at (-1.0, -2em)
[ev] at (0,    -2em)  ;
[ev] at (1.8,  -2em)  ;
[ev] at (3.6,  -2em)  ;
[ev] at (5.4,  -2em)  ;

[nd] at (-1.0, -4em)
[ev] at (0,    -4em)  ;
[ev] at (1.8,  -4em)  ;
[ev] at (3.6,  -4em)  ;
[ev] at (5.4,  -4em)  ;
[ev] at (7.2,  -4em)  ;

Traces of abstract events.
The event  signals an input of value v into variable ;
and  signals an output of value v from variable .
The event  indicates whether the debugging mode is turned on or off.

We illustrate prefix transducers on the classical example of observational determinism [64, 48].
Informally, observational determinism (OD) states that whenever two execution traces agree on low (publicly visible) inputs,
they must agree also on low outputs,
thus not leaking any information about high (secret) inputs.
Consider, for example, the traces $t_1$ and $t_2$ in Figure <ref>.
These two traces satisfy OD, because they have the same low inputs (events )
and produce the same low outputs (events ).
All other events in the traces are irrelevant to OD.
The two traces even satisfy synchronous OD, as the input and output events appear at the same positions in both traces,
and thus they can be analysed by synchronous-time monitors
(such as those based on HyperLTL [3, 18, 36, 54, 38]),
or by the following prefix transducer:

q/.style = scale=1, draw, circle, minimum width=7mm, align=left,
lab-edge/.style = scale=0.8, align=left
[q] (0) at (0,0) $q_{0}$;
[q] (1) at (5,0) $q_{1}$;
[q] (2) at (-5,0) $q_{2}$;

[->] ($(0.south) + (0, -3mm)$) to (0);
[->] (0) to[loop] node[lab-edge, yshift=10mm, xshift=9mm]

$\tau_1: \iter{\_}{\lab{e_1}{I_l + O_l}}$

$\tau_2: \iter{\_}{\lab{e_2}{I_l + O_l}}$

1c$\tau_1[e_1] = \tau_2[e_2]$

$\leadsto \tau_o \mapsto \top$

[->] (0) to node[lab-edge, yshift=10mm, xshift=18mm]

$\tau_1: \iter{\_}{\lab{e_1}{O_l}}$

$\tau_2: \iter{\_}{\lab{e_2}{O_l}}$

1c$\tau_1[e_1] \not = \tau_2[e_2]$

$\leadsto \tau_o \mapsto \bot$

[->] (0) to node[lab-edge, yshift=10mm, xshift=0mm]

$\tau_1: \iter{\_}{\lab{e_1}{I_l}}$

$\tau_2: \iter{\_}{\lab{e_2}{I_l}}$

1c$\tau_1[e_1] \not = \tau_2[e_2]$

$\leadsto \tau_o \mapsto \top$

The transducer reads two traces $\tau_1$ and $\tau_2$ that are instantiated with actual traces, e.g., $t_1$ and $t_2$.

It starts in the initial state $q_0$ and either repeatedly takes the self-loop transition, or goes into one of the states $q_1$
or $q_2$ where it gets stuck.
The self-loop transition matches the shortest prefix of $\tau_1$ that contains any events until a low input or output is found.
This is represented by the prefix expression
$\iter{\_}{{(I_l + O_l)}}$, where we use $I_l$ (resp. $O_l$) to represent any low input (resp. output) event,
and $\_$ stands for any event that does not match the right-hand side of $\iter{}{}$.
The same pattern is independently matched by this transition also against the prefix of $\tau_2$.
Moreover, the low input or output events found on traces $\tau_1$ and $\tau_2$ are labeled by $e_1$ and $e_2$, resp.
The self-loop transition is taken if the prefixes of $\tau_1$ and $\tau_2$ match the expressions and, additionally, the

$\tau_1[e_1] = \tau_2[e_2]$ is fulfilled.
The term $\tau[e]$ denotes the sequence of events in trace $\tau$ on the position(s) labeled by $e$.
Therefore, the condition
$\tau_1[e_1] = \tau_2[e_2]$ asserts that the matched input
or output events must be the same (both in terms of type and values).
If the transducer takes the self-loop transition, it outputs (appends) the symbol $\top$ to the output trace $\tau_o$ (as stated by the right-hand side of $\leadsto$).
Then, the matched prefixes are consumed from the input traces and the transducer continues with matching the rest of the traces.
The other two edges are processed analogously.

It is not hard to see that the transducer decides if OD holds for two synchronous input traces.
State $q_0$ represents the situation when OD holds but may still be violated in the future.
If the self-loop transition over $q_0$ cannot be taken, then (since we now assume synchronised traces), the matched prefixes must end either with different low input or different low output events.

In the first case, OD is satisfied by the two traces and the transducer goes to state $q_2$ where it gets stuck (we could, of course, make the transducer total to avoid getting stuck, but in this example we are interested only in its output).
In the second case, OD is violated and before the transducer changes the state to $q_1$,
it appends $\bot$ to the output trace $\tau_o$.
OD is satisfied if $\tau_o$ does not contain (end with) $\bot$ after finishing reading (or getting stuck on) the input traces.

The transducer above works also for monitoring asynchronous OD, where the low input and output events are misaligned by “padding” events (but it requires that there is the same number and order of low input and output events on the input traces – they are just misaligned and possibly carry different values; the general setup where the traces can be arbitrary is discussed in Section <ref>).
The transducer works for asynchronous OD because the prefix expressions for $\tau_1$ and $\tau_2$ are matched independently, and thus they can match prefixes of different lengths.
For example, for $\tau_1 = t_1$ and $\tau_2 = t_3$, the run consumes the traces in the following steps:

nd/.style = align=left,
ev/.style = align=left, rounded corners, scale=0.9,
fill=gray!20, minimum width=1cm
[nd] at (-1.2, 0)
[ev] at (0,   0)  ;
[ev] at (3.6, 0)  ;
[ev] at (5.4, 0)  ;
[ev] at (7.2, 0)  ;

[nd] at (-1.2, -2em)
[ev] at (0,    -2em)  ;
[ev] at (1.8,  -2em)  ;
[ev] at (3.6,  -2em)  ;
[ev] at (5.4,  -2em)  ;
[ev] at (7.2,  -2em)  ;

[] (0.95, 2em) to (0.95, -4em);
[] (6.30, 2em) to (6.30, -4em);
[] (8.10, 2em) to (8.10, -4em);

[] at (0,   2.5em)  step 1;
[] at (3.6, 2.5em)  step 2;
[] at (7.2, 2.5em)  step 3;

Hitherto, we have used the output of prefix transducers to decide OD for the given two traces, i.e., to perform the monitoring task.
We can also define a prefix transducer that, instead of monitoring OD for the two traces,
transforms the asynchronous traces $\tau_1$ and $\tau_2$ into
a pair of synchronous traces $\tau'_1$ and $\tau'_2$ by filtering out “padding” events:

[draw,circle, minimum width=6mm] (0) at (0,0) $q_0$;

[->] ($(0.north) + (0, 5mm)$) to (0);
[->] (0) to[loop left] node[yshift=0mm,align=left]

$\tau_1: \iter{\_}{\lab{e_1}{I_l + O_l}}$

$\tau'_1 \mapsto \tau_1[e_1]$

[->] (0) to[loop right] node[yshift=0mm,align=left]

$\tau_2: \iter{\_}{\lab{e_2}{I_l + O_l}}$

$\tau'_2 \mapsto \tau_2[e_2]$

In this example, the transducer appends every event labeled by $e_i$
to the output trace $\tau'_i$, and so it filters out all events except low inputs and outputs.
It reads and filters both of the input traces independently of each other.
The output traces from the transducer can then be forwarded to, e.g., a HyperLTL monitor[
One more step is needed before we can use a HyperLTL monitor, namely, to transform
the trace of abstract events from the example into a trace of sets of atomic propositions.
This can be also done by a prefix transducer.
compare to monitor automata (and maybe other automata models) – in a new section?

§.§.§ Contributions
This paper makes the following contributions:

* We introduce multi-trace prefix expressions and transducers (Section <ref> and Section <ref>).
These are formalisms that can efficiently and incrementally process words (traces) either fully synchronously, or asynchronously with synchronization points.

* We suggest that prefix transducers are a natural formalism for specifying
many synchronous and asynchronous $k$-safety hyperproperties,
such as observational determinism.

* We design an algorithm for monitoring synchronous and asynchronous $k$-safety hyperproperties using prefix transducers (Section <ref>).

* We provide some experiments to show how our monitors perform (Section <ref>).

"Variants of regular expressions have been used for a long time... special thing about ours expressions is the shortest prefix thing"
- formal definition of k-safety property
and say what all combinations of ...
- say all the additional work that can be done
- say that we could discard some traces or use some search strategy

§ PREFIX EXPRESSIONS

In this section, we define prefix expressions – a formalism
similar to regular expressions
designed to deterministically and unambiguously match prefixes of words.

§.§ Preliminaries

We model sequences of events as words over finite non-empty alphabets.
In some examples it is not clear that the alphabet is finite
Given an alphabet $\Sigma$, the set of finite words over this alphabet is denoted as $\Sigma^*$.
For two words $u = u_0...u_l\in\Sigma^*_1$ and $v=v_0...v_m\in\Sigma^*_2$,
their concatenation $u\cdot v$, also written $uv$ if there is no confusion,
is the word $u_0...u_lv_0...v_m \in (\Sigma_1 \cup \Sigma_2)^*$.
If $w = uv$, we say that $u$ is a prefix of $w$, written $u \le w$, and $v$
is a suffix of $w$. If $u \le w$ and $u \not = w$, we say that $u$ is a
proper prefix of $w$.

For a word $w = w_0...w_{k-1} \in \Sigma^*$, we denote $|w| = k$
its length, $w[i] = w_i$ for $0 \le i < k$ its $i$-th element,
$\substr{w}{s}{e} = w_sw_{s+1}...w_e$ the sub-word beginning at index $s$
and ending at index $e$, and $\suff{w}{s} = w_sw_{s+1}...w_{k-1}$ its suffix
starting at index $s$.

Given a function $f: A \rightarrow B$, we denote $Dom(f) = A$ its domain.
Partial functions with domain $A$ and codomain $B$ are written as $A \hookrightarrow B$.
Functions with a small domain are sometimes given extensionally by listing
the mapping, e.g., $\{x \mapsto 1, y \mapsto 2\}$.
Given a function $f$, $f[x \mapsto c]$ is the function that coincides with $f$ on all elements except on $x$ where it is $c$.

§.§ Syntax of prefix expressions

Let $L$ be a non-empty set of labels (names) and $\Sigma$ a finite non-empty alphabet.
The syntax of prefix expressions () is defined by the
following grammar:

\begin{equation*}
\begin{split}
\alpha ::= &~\epsilon \mid a\mid (\alpha.\alpha) \mid (\alpha + \alpha) \mid (\iter{\alpha}{\beta})
\mid \lab{l}{\alpha}\\
\beta ::=  &~a\mid (\beta + \beta) \mid \lab{l}{\beta}
\end{split}
\end{equation*}

where $a \in \Sigma$ and $l \in L$.
Many parenthesis can be elided if we let '$\iter{}{}$' (iteration) take precedence before
'.' (concatenation), which takes precedence before '+' (disjunction, plus).
We write $a . b$ as $ab$ where there is no confusion.
In the rest of the paper, we assume that a set of labels $L$ is implicitly given,
and that $L$ always has ,,enough” labels.
We denote the set of all prefix expressions over the alphabet $\Sigma$
(and any set of labels $L$) as $\pe(\Sigma)$, and  $\pe(\Sigma, L)$ if we want to
stress that the expressions use labels from $L$.

The semantics of s (defined later) is similar to the semantics of regular
expressions with the difference that a is not matched against a whole word
but it matches only its prefix, and this prefix is the shortest one possible (and non-empty – if not explicitly specified).

For this reason, we do not use the classical Kleene's iteration as it would
introduce ambiguity in matching.
For instance, the regular expression $a^*$ matches all the prefixes
of the word $aaa$. And even if we specify that we should pick the shortest one,
the result would be $\epsilon$, which is usually not desirable, because that means no progress in reading the word.
Picking the shortest non-empty prefix would be a reasonable solution in many cases,
but the problem with ambiguity persists. For example, the regular expression
$(ab)^*(a + b)^*$ matches the word $ab$ in two different ways, which introduces
non-determinism in the process of associating the labels with the matched positions.

To avoid the problems with Kleene's iteration, we use a binary iteration operator
that is similar to the until operator in LTL in that it requires
some letter to appear eventually.
The expression $\iter{\alpha}{\beta}$ could be roughly defined as
$\beta + {\alpha}{\beta} + {\alpha}^2{\beta} +
\dots$ where we evaluate it from left to right and
$\beta$ must match exactly one letter.
The restriction on $\beta$ is important to tackle ambiguity,
but it also helps efficiently evaluate the expression – it is enough to look at
a single letter to decide whether to continue matching whatever follows
the iteration, or whether to match the left-hand side of the expression.
Allowing $\beta$ to match a sequence of letters would require
a look-ahead or backtracking and it is a subject of future extensions.
With our iteration operator, expressions like $\iter{(ab)}{\iter{(a + b)}{}}$
and $\iter{a}{}$ are malformed and forbidden already on the level of syntax.

Sub-expressions of a can be labeled and the matching procedure
described later returns a list of positions in the word that were matched
for each of the labels.
We assume that every label is used maximally once, that is, no two
sub-expressions have the same label.
Labels in s are useful for identifying the sub-word that matched particular
sub-expressions, which will be important in the next
section when we use logical formulae that relate sub-words from
different words (traces).

Two examples of s and their informal evaluation are:

* $\iter{\lab{l}{a+b}}{a}$ – match $a$ or $b$, associating them to
$l$, until you see $a$. Because whenever the word contains $a$,
the right-hand side of the iteration matches,
the left part of the iteration never matches $a$ and $a$ is redundant in the
left-hand side sub-expression.
For the word $bbbaba$, the expression matches the prefix $bbba$
and $l$ is associated with the list of position ranges $(0,0), (1,1), (2,2)$ that
corresponds to the positions of $b$ that were matched by the sub-expression

* $\lab{l_1}{\iter{a}{b}}\lab{l_2}{\iter{(b+c)}{(a+d)}}$ – match $a$
until $b$ is met and call this part $l_1$; then match $b$ or $c$ until $a$ or
$d$ and call that part $l_2$. For the word $aabbbada$, the expression
matches the prefix $aabbba$. The label $l_1$ is associated with the range of
positions $(0,2)$ containing the sub-word $aab$,
and $l_2$ with the range $(3,5)$ containing the sub-word $bba$.

§.§ Semantics of prefix expressions

We first define m-strings before we get to the formal semantics of s.

An m-string is a sequence of pairs of numbers or a special symbol $\bot$.
Intuitively, $(p, \bot)$ represents the beginning of a match at position $p$ in
the analyzed word, $(\bot, p)$ the end of a match at position $p$, and
$(s, e)$ is a match on positions from $s$ to $e$.
The concatenation of m-strings reflects opening and closing the matches.

M-strings are words over the alphabet
$M=(\mathbb{N} \cup \{\bot\})\times(\mathbb{N} \cup \{\bot\})$
with the partial concatenation function
$\mconc: M^* \times M \hookrightarrow M^*$ defined as

\[
\alpha\mconc(c, d) =
\begin{cases}
(c,d)             & \text{if } \alpha = \epsilon \land c \not = \bot \\
\alpha\cdot(c,d)  & \text{if } \alpha = \alpha'\cdot(a, b) \land b \not = \bot\\
\alpha'\cdot(a,d) & \text{if } \alpha = \alpha'\cdot(a, b) \land b = \bot \land c = \bot\\
\alpha'\cdot(c,d) & \text{if } \alpha = \alpha'\cdot(a, b) \land b = \bot \land c \not = \bot
\end{cases}
\]

Every m-string is built up
from the empty string $\epsilon$ by repeatedly concatenating $(p, \bot)$ or
$(\bot, p)$ or $(p, p)$.
The concatenation $\mconc$ is only a partial function (e.g., $\epsilon \mconc
(\bot, \bot)$ is undefined), but we will use only the defined fragment of the

It works as standard concatenation if the last match was closed (e.g., $(0,
4)\mconc(7, \bot) = (0, 4)(7, \bot)$), but it overwrites the last match if we
start a new match without closing the old one (e.g., $(0, \bot)\mconc(2, \bot)
= (2, \bot)$). Overwriting the last match in this situation is valid, because
labels are assumed to be unique and opening a new match before the last match
was closed means that the old match failed.

We extend $\mconc$ to work with m-strings on the right-hand side:

\[
\alpha \mconc w =
\begin{cases}
\alpha & \text{if } w = \epsilon\\
(\alpha \mconc x) \mconc w' & \text{if } w = x \cdot w'
\end{cases}
\]

While evaluating a , we keep one m-string per label used in the . To do so
we use m-maps, partial mappings from labels to m-strings.

Let $L$ be a set of labels and
$M=(\mathbb{N} \cup \{\bot\})\times(\mathbb{N} \cup \{\bot\})$
be the alphabet of m-strings. An m-map is a partial function
$m: L \hookrightarrow M^*$. Given two
m-maps $m_1, m_2: L \hookrightarrow M^*$, we define their concatenation
$m_1\mcomp m_2$ by

\[
(m_1\mcomp m_2)(l) = \sigma_1 \mconc \sigma_2
\]

for all $l\in Dom(m_1) \cup Dom(m_2)$ where $\sigma_i = \epsilon$ if $m_i(l)$
is not defined and $\sigma_i = m_i(l)$ otherwise.

We denote the set of all
m-maps $L \hookrightarrow M^*$ for the set of labels $L$ as $\ML$.

The evaluation of a over a word $w$ is defined as an iterative application
of a set of rewriting rules that are inspired by language
derivatives [19, 5]. For the purposes of evaluation, we
introduce two new prefix expressions: $\bot$
[Because s and m-strings never interact together,
we use the symbol $\bot$ in both, but formally they are different symbols.]
and $\labm{l}{\alpha}$. $\bot$ represents a failed match and
$\labm{l}{\alpha}$ is a ongoing match of a labeled sub-expressions
$\lab{l}{\alpha}$. Further, for a $\alpha$, we define inductively that
$\epsilon \in \alpha$ iff

- $\alpha = \epsilon$, or

- $\alpha$ is one of $(\alpha_0 + \alpha_1)$ or
$\lab{l}{\alpha_0 + \alpha_1}$ or
$\labm{l}{\alpha_0 + \alpha_1}$ and it holds that
$(\epsilon \in  \alpha_0 \lor \epsilon \in \alpha_1)$.

For the rest of this section, let us fix a set of labels $L$, an
alphabet $\Sigma$, and denote $\E = \pe(\Sigma, L)$ the set of all prefix
expressions over this alphabet and this set of labels.
The core of evaluation of s is the one-step
relation $\step{a}{p} \subseteq (\E \times \ML) \times (\E \times
\ML)$ defined for each letter $a$ and natural number $p$,
whose defining rules are depicted in Figure <ref>.
We assume that the rules are evaluated modulo the equalities $\epsilon\cdot\alpha = \alpha\cdot\epsilon = \alpha$,

and we say that $\alpha'$
is a derivation of $\alpha$ if $\alpha \step{a}{p} \alpha'$ for some $a$ and

\begin{align*}
\inferrule{~}{(\epsilon, M) \step{a}{p} (\bot, \emptyset)}\rname{Eps}&&
\inferrule{~}{(\bot, M) \step{a}{p} (\bot, \emptyset)}\rname{Bot}&&
\inferrule{~}{(a, M) \step{a}{p} (\epsilon, M)}\rname{Ltr}
\end{align*}

\begin{align*}
\inferrule{a \not = b}{(a, M) \step{b}{p} (\bot, \emptyset)}\rname{Ltr-fail}&&
\inferrule{(\alpha, M) \step{a}{p} (\alpha', M')\\
\alpha' \not = \bot \\ \epsilon\not\in\alpha'}
{(\alpha\beta, M) \step{a}{p} (\alpha'\beta, M')}\rname{Concat}&&
\end{align*}

\begin{align*}
\inferrule{(\alpha, M) \step{a}{p} (\alpha', M')\\
\epsilon\in\alpha' }
{(\alpha\beta, M) \step{a}{p} (\beta, M')}\rname{Concat-$\epsilon$}&&
\inferrule{(\alpha, M) \step{a}{p} (\alpha', M')\\
\alpha' = \bot}
{(\alpha\beta, M) \step{a}{p} (\bot, \emptyset)}\rname{Concat-$\bot$}
\end{align*}

\begin{align*}
\inferrule{(\alpha_0, M) \step{a}{p} (\alpha'_0, M'_0)\\
(\alpha_1, M) \step{a}{p} (\alpha'_1, M'_1)\\
\epsilon \in\alpha'_0 \lor \epsilon\in\alpha'_1}
{(\alpha_0 + \alpha_1, M) \step{a}{p} (\epsilon, M_0'\mcomp M_1')}\rname{OR-end}
\end{align*}

\begin{align*}
\inferrule{(\alpha_0, M) \step{a}{p} (\alpha'_0, M'_0)\\
(\alpha_1, M) \step{a}{p} (\alpha'_1, M'_1)\\
\epsilon \not\in\alpha'_0 \land \epsilon\not\in\alpha'_1 }
{(\alpha_0 + \alpha_1, M) \step{a}{p} (\alpha'_0 + \alpha'_1, M_0'\mcomp M_1')\\ \alpha'_0 + \alpha'_1 \text{ is reduced w.r.t } \alpha + \bot = \bot + \alpha =\alpha}\rname{OR}
\end{align*}

\begin{align*}
\inferrule{(\beta, M)\step{a}{p}(\beta', M')\\\epsilon \in \beta'}
{(\iter{\alpha}{\beta}, M) \step{a}{p} (\epsilon, M')}\rname{Iter-end}&&
\inferrule{(\beta, M)\step{a}{p}(\beta', \_)\\
\epsilon \not \in \beta'\\
(\alpha, M)\step{a}{p}(\alpha', M')}
{(\iter{\alpha}{\beta}, M) \step{a}{p} (\alpha'\iter{\alpha}{\beta}, M')}\rname{Iter}
\end{align*}

\begin{align*}
\inferrule{(\alpha, M)\step{a}{p}(\alpha', M')\\ \epsilon \not \in \alpha'}
{(\lab{l}{\alpha}, M) \step{a}{p} (\labm{l}{\alpha'}, \{l\mapsto(p, \bot)\}\mcomp M')}\rname{L-start}&&
\inferrule{(\alpha, M)\step{a}{p}(\alpha', M')\\ \epsilon \not \in \alpha'}
{(\labm{l}{\alpha}, M) \step{a}{p} (\labm{l}{\alpha'}, M')}\rname{L-cont}&&
\end{align*}

\begin{align*}
\inferrule{(\alpha, M)\step{a}{p}(\alpha', M')\\ \epsilon \in \alpha'}
{(\lab{l}{\alpha}, M) \step{a}{p} (\epsilon, M'\mcomp \{l\mapsto(p, p)\})}\rname{L-ltr}&&
\inferrule{(\alpha, M)\step{a}{p}(\alpha', M')\\ \epsilon \in \alpha'}
{(\labm{l}{\alpha}, M) \step{a}{p} (\epsilon, M'\mcomp\{l\mapsto(\bot, p)\})}\rname{L-end}
\end{align*}

One-step relation for evaluating prefix expressions.
The rules are evaluated modulo the equalities $\epsilon\cdot\alpha = \alpha\cdot\epsilon = \alpha$.

The first seven rules

in Figure <ref> are rather standard. Rules for disjunction
are non-standard in the way that whenever an operand of a disjunction is
evaluated to $\epsilon$, the whole disjunction is evaluated to $\epsilon$ (rule
Or-end) in order to obtain the shortest match.
Also, after rewriting a disjunction, operands that
evaluated to $\bot$ are dropped (unless the last one if we should drop all

The only non-shortening rule is Iter that unrolls $\alpha$ if $\beta$ was not matched in $\iter{\alpha}{\beta}$.
Thus, evaluating $\iter{\alpha}{\beta}$ can first prolong the expression and then eventually end up again in $\iter{\alpha}{\beta}$ after a finite number of steps.
This does not introduce any problems as the set of derivations remains bounded [21].

There are four rules for handling labellings.
Rule L-ltr handles one-letter matches.

Rule L-start handles the beginning of a match where the expression $\lab{l}{\alpha}$
gets rewritten to $\labm{l}{\alpha}$ so that we know we are currently matching
label $l$ in the next steps. Rules L-cont and L-end continue
and finish the match once the labeled expression evaluates to $\epsilon$.
Concatenating m-maps in the rules works well because of the assumption that no two
sub-expressions have the same label. Therefore, there are no collisions and we
always concatenate information from processing the same sub-expression.

The one-step relation is deterministic, i.e., there is always at
most one rule that can be applied and thus every has a unique single derivation for a fixed letter $a$ and position $p$.

For an arbitrary $\alpha$ over alphabet $\Sigma$, and any $a\in\Sigma$
and $p\in\mathbb{N}$, there exist at most one $\alpha'$ such that
$\alpha \step{a}{p} \alpha'$ (that is, there is at most one defining rule
of $\step{a}{p}$ that can be applied to $\alpha$).

Multiple rules could be applied only if they match the same structure of $\alpha$
(e.g., that $\alpha$ is a disjunction). But for such rules, the premises are pairwise
unsatisfiable together.

Having the deterministic one-step relation, we can define the
evaluation function on words $\delta: \E \times {\Sigma^*} \rightarrow \E
\times \ML$ that returns the rewritten and the m-map
resulting from evaluating the one-step relation for each single letter of the word:
$\delta(\alpha, w) = \overline\delta(\alpha, w, 0, \emptyset)$ where

\[
\overline\delta(\alpha, w, p, M) =
\begin{cases}
(\alpha, M)           & \text{if } w = \epsilon\\
\overline\delta(\alpha', w', p+1, M')
& \text{if } w = aw' \land (\alpha, M)\step{a}{p}(\alpha', M')\\
\end{cases}
\]

We also define the decomposition function
$\rho: \E \times \Sigma^* \rightarrow (\Sigma^* \times \ML \times \Sigma^*) \cup \{\bot\}$
that decomposes a word $w \in \Sigma^*$
into the matched prefix with the resulting m-map, and the rest of $w$:

\[
\rho(\alpha, w) =
\begin{cases}
(u, m, v) & \text{if }~w = uv \land \delta(\alpha, u) = (\epsilon, m)\\
\bot & \text{otherwise}
\end{cases}
\]

Function $\rho$ is well-defined as there is at most one $u$ for which
$\delta(\alpha, u) = (\epsilon, \_)$. This follows
from the determinism of the one-step relation.
Function $\rho$ is going to be important in the next section.

There are only finitely many s that we can obtain
from a by repeated application of $\step{a}{p}$ for
any $a$ and a fixed $p$.

Given a number $p\in\mathbb{N}$ and an arbitrary $\alpha$ over an alphabet $\Sigma$, the set

\[
D_p(\alpha) = \{\alpha' \mid \alpha \step{a_0}{p} ... \step{a_k}{p} \alpha', a_1, ..., a_k \in \Sigma\}
\]

is finite.

Every rule except Iter is shortening.
Application of $\step{a}{p}$ on $\iter{\alpha}{\beta}$ is either $\epsilon$
or $\alpha'\cdot\iter{\alpha}{\beta}$. If $\alpha$ contains nested iteration,
the expression can get extended further to the left,
but because the nesting of iterations must be finite,
at some point the left-hand side of the left-most iteration,
let us call this iteration expression $\xi$,
has no nested iteration and repeatedly applying one-step
relation leads to shortening the expression until $\xi$ again becomes the left-most
expression (or the whole expression evaluates to $\bot$).
From this point on,
any expression obtained by one-step relation is either shorter than the original one
or it has been already seen.

To strengthen the intuition behind the proof sketch above, here are depicted
possible evaluations of an expression over the alphabet $\{a, b, c\}$ with two nested iterations (we do not show the parameter $p$):

[anchor=west](1) at (0, 0) $\iter{(\iter{ab}{c})}{c}$;
[anchor=west](2) at (3, 0) $b(\iter{ab}{c})\iter{(\iter{ab}{c})}{c}$;
[anchor=west](3) at (7, 0) $(\iter{ab}{c})\iter{(\iter{ab}{c})}{c}$;
[below=of 1](e) $\epsilon$;
[below=of 2](b) $\bot$;
(1) edge[double, ->] node[yshift=3mm] $a$(2);
(1) edge[double, ->] node[xshift=3mm] $c$(e);
(2) edge[double, ->] node[yshift=3mm] $b$(3);
(3) edge[bend left, double, ->] node[yshift=-3mm] $a$(2);
(3) edge[bend right, double, ->] node[yshift=3mm] $c$(1);

(1) edge[double, ->] node[yshift=3mm] $b$(b);
(2) edge[double, ->] node[xshift=4mm] $a,c$(b);
(3) edge[double, ->, bend left] node[yshift=-3mm] $b$(b);

Thanks to theorems <ref> and <ref>,
the evaluation function $\delta$ for a fixed $\alpha$ over an alphabet $\Sigma$
can be translated into a unique prefix-free [46] finite state transducer [62].
The transducer has for states the set $D_p(\alpha)$, and edges are formed as in the example above (notice that the expressions in the example above are exactly the expressions from $D_p(\iter{(\iter{ab}{c})}{c})$), i.e., for
any $a\in\Sigma$, there is the transition $\alpha_0 \xrightarrow{a,p/M} \alpha_1$
between two states iff $(\alpha_0, \emptyset) \step{a}{p} (\alpha_1, M)$. The
initial state of a transducer is the state $\alpha$

and the accepting state is $\epsilon$.
A run of the transducer on a word $w = w_0w_1...w_k$ is a sequence of
adjacent edges starting from the initial state such that the guard on $i$-th edge is $w_i, i$:

(\alpha)\xrightarrow{w_0, 0/M_0} (\alpha_1) \xrightarrow{w_1,1/M_1} ...
\xrightarrow{w_{k-1},k-1/M_{k-1}}(\alpha_k)

Further, it holds that $\delta(\alpha, w) = (\alpha_k,
M_0\mcomp...\mcomp M_{k-1})$.

An example of a transducer for
$b(\iter{\lab{l}{ab}}{b})(b+a)$ over the alphabet $\{a, b\}$
is shown in Figure <ref>.

nd/.style = fill=gray!5,draw, rounded corners, inner sep=3pt
[nd] (0) at (-1, 0)  $b(\iter{\lab{l}{ab}}{b})(b+a)$;
[nd] (1) at (3, 0)   $(\iter{\lab{l}{ab}}{b})(b+a)$;
[nd] (2) at (7, 0)   $(b+a)$;
[nd] (3) at (3, -1.5)$[b]_l(\iter{\lab{l}{ab}}{b})(b+a)$;
[nd,double, color=istagreen,fill=white]
(5) at (7, -1.5) $\epsilon$;

[->] ($(0.west) + (-5mm, 0)$)  to (0);
[->] (0) edge node[yshift=3mm]$b,p/\emptyset$ (1);
[->] (1) edge node[yshift=3mm]$b,p/\emptyset$ (2);
[->] (1) edge node[ xshift=-13mm]$a,p/\{l\mapsto(p, \bot)\}$ (3);
[] ($(3.north) + (5mm, 0)$)
edge[->] node[xshift=13mm]$b,p/\{l \mapsto (\bot, p) \}$
($(1.south) + (5mm, 0)$);

[->] (2) to node[xshift=4mm]$*/\emptyset$ (5);

Finite transducer for $b(\iter{\lab{l}{ab}}{b})(b+a)$.
Redundant states and transitions

were omitted.

Strictly formally, this transducer as shown in Figure <ref>
would be symbolic transducer [62] as the position $p$ on edges represents any natural number.
However, $p$ is rather a parameter of the transducer and it only propagates into the output of some edges.
Therefore, it would be more precise to avoid having $p$ in the guard of the edge
and, instead, output functions that take $p$ as the only parameter. For example,
instead of the m-map $\{l \mapsto (p, \bot)\}$,
we would output a map that returns the m-map: $\lambda p.\{l \mapsto (p, \bot)\}$.
The semantics of the output of the transducer then would be modified
to supply and evaluate the outputs on the right sequence of $p$s.
This approach, although formally better, seems unnecessarily complicated
for our purposes.

The fact that s correspond to prefix-free transducers
suggests how to compose and perform other operations with s.

§ MULTI-TRACE PREFIX EXPRESSIONS AND TRANSDUCERS

In this section, we define multi-trace prefix expressions and
multi-trace prefix transducers.

§.§ Multi-trace prefix expressions

A multi-trace prefix expression ()
matches prefixes of multiple words.
Every consists of prefix expressions associated to input words and
a condition which is a logical formula that must be satisfied by the matched prefixes.

Multi-trace prefix expression ()
over trace variables $V_\tau$ and alphabet $\Sigma$ is a list of pairs together with a formula:

$$(\tau_0, e_0), \ldots, (\tau_k, e_k)[\varphi]$$

where $\tau_i \in V_\tau$ are trace variables and $e_i$ are s over the alphabet
$\Sigma$. The formula $\varphi$ is called the condition of .
We require that for all $i \not = j$, labels in $e_i$ and $e_j$ are distinct.

If the space allows, we typeset s over multiple lines as can be seen
in the examples of prefix transducers throughout the paper.

conditions are logic formulae over m-strings and input words[
The conditions can be almost arbitrary formulae,
depending on how much we are willing to pay for their evaluation.
They could even contain nested s. As we will see later, conditions are evaluated only after matching the prefixes which gives us a lot of freedom in choosing the logic. For the purposes of this work,
however, we use only simple conditions that we need in our examples
and evaluation.

Let $V_\tau$ be a set of trace variables and $L$ a set of labels.
Atomic terms of conditions are $l$ for each $l \in L$,
$\tau[l]$ for any label $l$ and trace variable $\tau \in V_\tau$,
and constants (words over arbitrary alphabet and m-strings).

A well-formed condition is a boolean formula built up inductively from terms with these rules:

* $t = t'$ is a well-formed condition for $t, t'$ atomic terms

* if $C$ is a well-formed condition, $\neg C$ is a well-formed condition

* $(C \land C')$ are well-formed conditions for well-formed conditions $C, C'$

As usual, we can omit parenthesis using the precedence rules that the equality have
the highest priority, then negation ($\neg$) and then conjunction
($\land$). We write $t \not = t'$ for $\neg(t = t')$ and we use the classical
shortcuts for disjunction and implication: $C \lor C' \equiv \neg(\neg C \land \neg C')$,
and $C \implies C' \equiv \neg C \lor C'$.

For an assignment $\sigma: V_\tau \rightarrow \Sigma^*$ of trace variables to words
and an m-map $M$, we define the evaluation of atomic terms $\teval{\sigma, M}{\cdot}$
in the following way:

\begin{align*}
\teval{\sigma, M}{c} =&~ c \text{ for any constant } c\\
\teval{\sigma, M}{l} =&~
\begin{cases}
M[l]       & \text{if } l \in Dom(M)\\
\epsilon   & \text{otherwise}
\end{cases}\\
\teval{\sigma, M}{\tau[t]} =&~
\begin{cases}
\sigma(\tau)[s_0 .. e_0]\cdot ... \cdot \sigma(\tau)[s_k .. e_k]
& \text{if } \teval{\sigma, M}{t} = (s_0, e_0)\cdot ... \cdot(s_k, e_k)\\
& \text{and } \forall i. s_i \not = \bot \land e_i \not = \bot\\
\epsilon      & \text{otherwise}
\end{cases}\\
\end{align*}

The satisfaction relation $\models$ on conditions is evaluated w.r.t the
trace assignment $\sigma$ and an m-map $M$:

\begin{align*}
\sigma, M \models t = t'  \iff &~ \teval{\sigma, M}{t} = \teval{\sigma, M}{t'}\\
\sigma, M \models \neg C  \iff &~ \sigma, M \not \models C\\
\sigma, M \models C \land C' \iff &~ \sigma, M \models C \text{ and } \sigma, M \models C'\\
\end{align*}

The condition $l_1 = l_2 \land \tau_1[l_1] \not = \tau_2[l_2]$
gets evaluated to true for $\sigma = \{\tau_1 \mapsto abcba, \tau_2 \mapsto bacab\}$ and
$M = \{l_1,l_2 \mapsto (0, 1)(3,4)\}$, because the terms are evaluated to
$\teval{\sigma, M}{l_1} = \teval{\sigma, M}{l_2} = (0, 1)(3,4)$ and therefore
$\teval{\sigma, M}{\tau_1[l_1]} = abba$ and
$\teval{\sigma, M}{\tau_2[l_2]} = baab$.

Given an $\alpha$, we denote as $\alpha(\tau)$ the PE associated to
trace variable $\tau$ and if we want to highlight that $\alpha$ has the condition $\varphi$, we write $\alpha[\varphi]$.
We denote the set of all s over trace variables $V_\tau$ and alphabet $\Sigma$ as $\mathit{\mpe}(V_\tau, \Sigma)$.
An $\alpha[\varphi]$ over trace variables $V_I$ satisfies a trace assignment, written $\sigma \models \alpha$, iff
$\tau \in V_I: \rho(\alpha(\tau), \sigma(\tau)) = (u_\tau, M_\tau, v_\tau)$ and
$\sigma, M_{\tau_1}\mcomp ... \mcomp M_{\tau_k} \models \varphi$ where
$\{{\tau_1}, ..., {\tau_k}\} = V_I$. That is, $\sigma \models \alpha$ if
every prefix expression for $\alpha$ has matched a prefix and the condition
$\varphi$ is satisfied.

§.§ Multi-trace prefix transducers

Multi-trace prefix transducers () are finite transducers [62] with s as guards on the transitions.

If a transition is taken, one or more symbols are appended to one or more
output words, the state is changed to the target state of the transition and the matched prefixes of input words are consumed. The evaluation then continues matching
new prefixes of the shortened input words.
Combining s with finite state transducers allows to read
input words asynchronously (evaluating s) while having synchronization points
and finite memory (states of the transducer).

A multi-trace prefix expression transducer () is a tuple $(V_I, V_O, \Sigma_I, \Sigma_O, Q, q_0, \Delta)$ where

* $V_I$ is a finite set of input trace variables

* $V_O$ is a finite set of output trace variables

* $\Sigma_I$ is an input alphabet

* $\Sigma_O$ is an output alphabet

* $Q$ is a finite non-empty set of states

* $q_0 \in Q$ is the initial state

* $\Delta: Q \times \mathit{\mpe}(V_I, \Sigma_I) \times (V_O \hookrightarrow {\Sigma^*_O}) \times Q$
is the transition relation; we call the partial mappings $(V_O \hookrightarrow {\Sigma^*_O})$ output assignments.

A run of an  $(V_I, V_O, \Sigma_I, \Sigma_O, L, Q, q_0, \Delta)$
on trace assignment $\sigma_0$ is a sequence

$\pi = (q_0, \sigma_0) \xrightarrow{\nu_0} (q_1, \sigma_1) \xrightarrow{\nu_1}
\ldots \xrightarrow{\nu_{k-1}} (q_k, \sigma_k)$
of alternating states and trace assignments $(q_i, \sigma_i)$ with output assignments
such that for each $(q_i, \sigma_i) \xrightarrow{\nu_i}(q_{i+1}, \sigma_{i+1})$

there is a transition $(q_i, \alpha, \nu_i, q_{i+1}) \in \Delta$ such that $\sigma_i \models \alpha$ and $\forall\tau \in V_I: \sigma_{i+1}(\tau) = v_\tau$ where
$(\_, \_, v_\tau)=\rho(\alpha(\tau), \sigma_i(\tau))$.

That is, taking a transition in an  is conditioned by
satisfying its  and its effect is that every matched
prefix is removed from its word and the output assignment is put to output.

The output $O(\pi)$ of the run $\pi$

is the concatenation of the output assignments
$\nu_0 \cdot \nu_1 \cdot ... \cdot \nu_{k-1}$,
where a missing assignment to a trace is considered to be $\epsilon$.
Formally, for any $t\in V_O$, $\nu_i \cdot \nu_j$ takes the value

(\nu_i \cdot \nu_j)(t) =
\begin{cases}
\nu_i(t)\cdot\nu_j(t) & \text{if } \nu_i(t) \text{ and } \nu_j(t) \text{ are defined}\\
\nu_i(t)         & \text{if } \nu_i(t) \text{ is defined and } \nu_j(t) \text{ is undefined}\\
\nu_j(t)         & \text{if } \nu_i(t) \text{ is undefined and } \nu_j(t) \text{ is defined}
\end{cases}

Consider the  in Figure <ref> and
words $t_1 = ababcaba$ and $t_2 = babacbab$ and the assignment
$\sigma = \{\tau_1 \mapsto t_1, \tau_2 \mapsto t_2\}$. The run on this assignment
is depicted in the same figure on the bottom left.
The output of the  on $\sigma$
is $\bot\top\top\top$.
For any words that are entirely consumed by the
without getting stuck, it holds that $\tau_1$ starts with a sequence
of $ab$'s and $\tau_2$ with a sequence of $ba$'s of the same length.
Then there is one $c$ on both words and the words end with a sequence
of $a$ or $b$ but such that when there is $a$ in one word, there must be $b$
in the other word and vice versa.

[draw,circle, minimum width=6mm] (0) at (0,0) $q_0$;
[draw,circle, minimum width=6mm] (1) at (5,0) $q_1$;

[->] ($(0.west) + (-5mm, 0)$) to (0);
[->] (0) to node[yshift=9mm,xshift=8mm,align=left]

$\tau_1: \iter{\lab{l_1}{ab}}{c}$

$\tau_2: \iter{\lab{l_2}{ba}}{c}$

1c$l_1 = l_2$

$\leadsto \tau_o \mapsto \bot$
[->] (1) to[loop right] node[yshift=0mm,align=left]

$\tau_1: \lab{l_1}{a + b}$

$\tau_2: \lab{l_2}{a + b}$

1c$\tau_1[l_1] \not = \tau_2[l_2]$

$\leadsto \tau_o \mapsto \top$

[align=left] (t) at  (  -1,0) $\tau_1:$
[align=left] (r1) at (  0,0) a
[align=left] (r2) at (0.7,0) b
[align=left] (r3) at (1.4,0) a
[align=left] (r4) at (2.1,0) b
[align=left] (rc) at (2.8,0) c
[align=left] (r5) at (3.5,0) a
[align=left] (r6) at (4.2,0) b
[align=left] (r7) at (4.9,0) a

[color=gray!50] (-1.5, -.5) – (5.4, -.5);

[align=left] (t0) at (-1, -.8) $\tau_o:$;
[align=left] (t1) at ( 1.4, -.8) $\bot$;
[align=left] (t2) at ( 3.5, -.8) $\top$;
[align=left] (t3) at ( 4.2, -.8) $\top$;
[align=left] (t4) at ( 4.9, -.8) $\top$;

[align=left] (q0) at ( -.25, .8) $q_0$;
[align=left] (q1) at ( 3.15, .8) $q_1$;
[align=left] (q2) at ( 3.85, .8) $q_1$;
[align=left] (q3) at ( 4.55, .8) $q_1$;
[align=left] (q4) at ( 5.25, .8) $q_1$;

[->] (q0) to (q1);
[->] (q1) to (q2);
[->] (q2) to (q3);
[->] (q3) to (q4);

[on background layer]

[fit=(r1)(rc), inner sep=0, fill=istalightazure, rounded corners];

[fit=(r5), inner sep=0, fill=istalightgreen!40, rounded corners];
[fit=(r6), inner sep=0, fill=istalightgreen!40, rounded corners];
[fit=(r7), inner sep=0, fill=istalightgreen!40, rounded corners];

[align=left] (t) at  (  -1,0) $\tau_1:$
[align=left] (r1) at (  0,0) a
[align=left] (r2) at (0.7,0) b
[align=left] (r3) at (1.4,0) a
[align=left] (r4) at (2.1,0) b
[align=left] (rc) at (2.8,0) a
[align=left] (r5) at (3.5,0) b
[align=left] (r6) at (4.2,0) c
[align=left] (r7) at (4.9,0) a
[align=left] (r8) at (5.6,0) b
[align=left] (r9) at (6.3,0) a

[color=gray!50] (-1.5, -.5) – (6.8, -.5);

[align=left] (q0) at ( -.25, .8) $q_0$;
[align=left] (q1) at ( 4.55, .8) $q_1$;
[align=left] (q2) at ( 5.25, .8) $q_1$;
[align=left] (q3) at ( 5.95, .8) $q_1$;
[align=left] (q4) at ( 6.65, .8) $q_1$;

[align=left] (t0) at (-1, -.8) $\tau_o:$;
[align=left] (t1) at ( 2.1, -.8) $\bot$;
[align=left] (t2) at ( 4.9, -.8) $\top$;
[align=left] (t3) at ( 5.6, -.8) $\top$;
[align=left] (t4) at ( 6.3, -.8) $\top$;

[->] (q0) to (q1);
[->] (q1) to (q2);
[->] (q2) to (q3);
[->] (q3) to (q4);

[on background layer]

[fit=(r1)(rc), inner sep=0, fill=istalightazure, rounded corners];
[inner sep=0, fill=istalightazure, rounded corners,
minimum height=1.4em, minimum width=2cm] at (3.5, .215) ;

[fit=(r7), inner sep=0, fill=istalightgreen!40, rounded corners];
[fit=(r8), inner sep=0, fill=istalightgreen!40, rounded corners];
[fit=(r9), inner sep=0, fill=istalightgreen!40, rounded corners];

The from Example <ref> and a demonstration of its two runs.
Colored regions show parts of words as they are matched by
the transitions, the sequence of passed states is shown above the traces.

Now assume that the words are
$t_1 = abababcaba$ and $t_2 = babacbab$ with the same assignment.
The situation changes as now the expression on trace $t_1$
matches the prefix $(ab)^3$ while on $t_2$ the prefix $(ba)^2$.
Thus $l_1 = (0, 6) \not = (0, 4) = l_2$ and the match fails.

Finally, assume that we remove the condition $\cond{l_1 = l_2}$
from the first transition. Then for the new words the
matches again and the match is depicted on the bottom right in Figure <ref>.

In the next section, we work with deterministic s.
We say that an is deterministic if it can take at most one transition
in any situation.

Let $T = (V_I, V_O, \Sigma_I, \Sigma_O, Q, q_0, \Delta)$ be an .
We say that T is deterministic () if for any state $q\in Q$,
and an arbitrary trace assignment $\sigma: V_I \rightarrow \Sigma_I^*$,
if there are multiple transitions $(q, \alpha_1, \nu_1, q_1), ..., (q, \alpha_k, \nu_k, q_k)$ such that $\forall i: \sigma \models \alpha_i$,
it holds that there exists a proper prefix $\eta$ of $\sigma$,
(i.e., $\forall \tau\in V_I: \eta(\tau) \le \sigma(\tau)$ and for some $\tau$ $\eta(\tau) <\sigma(\tau)$),
and there exist $i$ such that
$\eta \models \alpha_i$ and $\forall j \not = i: \eta \not \models \alpha_j$.

Intuitively, an is if whenever there is a trace assignment that
satisfies more than one transition from a state, one of the transitions matches
“earlier” than any other of those transitions.

§ HYPERTRACE TRANSFORMATIONS

A hyperproperty is a set of sets of infinite traces.

In this section, we discuss an algorithm for monitoring hyperproperties,
which are those whose violation can be witnessed by at most $k$ finite traces:
A hyperproperty $S$ is hyperproperty

\[
\forall T \subseteq  \Sigma^\omega: T \not \in S \implies
%\exists M \in \mathcal{P}_{fin}(\Sigma^*). M \le T \land |M| \le k \land
\exists M \subseteq \Sigma^*: M \le T \land |M| \le k \land
(\forall T' \subseteq\Sigma^\omega: M \le T' \implies T' \not \in S)
\]

where $\Sigma^\omega$ is the set of infinite words over alphabet $\Sigma$,
and $M \le T$ means that each word in $M$ is a (finite) prefix of a word in $T$.

We assume unbounded parallel input model [37],
where there may be arbitrary many traces digested in parallel, and
new traces may be announced at any time.
Our algorithm is basically the combinatorial
algorithm for monitoring hyperproperties of Finkbeiner et al. [35, 42] where we exchange automata generated from HyperLTL
specifications with s.

That is, to monitor a hyperproperty, we instantiate an for every k-tuple of input traces.

An advantage of using s instead of monitor automata in the algorithm of
Finkbeiner et al. is that we automatically
get a monitoring solution for asynchronous hyperproperties.
A disadvantage is that we cannot automatically use some of the optimizations designed
for HyperLTL monitors that are based on the structure (e.g., symmetry) of the HyperLTL
formula [36].

The presented version of our algorithm assumes that the input is as it is preferable to have deterministic monitors.
Deciding whether a given is deterministic depends a lot on the chosen logic used
for constraints. We are currently working on an algorithm that decides
the determinism for s with the equality constraints used in this paper.
In the rest of the paper, we assume that the used s are known to be
s (which is also the case of s used in our evaluation).
We make the remark that in cases where the input is not known to be
deterministic and/or a check is impractical,
one may resort to a way how to resolve possible non-determinism instead,
such as using priorities on the edges.
This is a completely valid solution and it is easy to modify our algorithm to work
this way. In fact, the algorithm works also with non-deterministic s with a small modification.

§.§ Algorithm for online monitoring of hyperproperties

Our algorithm is depicted in Algorithm <ref>
and Algorithm <ref> (auxiliary procedures).
In essence, the algorithm maintains a set of configurations where one
configuration corresponds to the state of evaluation of one edge of an  instance.
Whenever the algorithm may make a progress in some configuration,
it does so and acts according to whether matching the edge succeeds, fails, or needs more events.

Now we discuss functioning of the algorithm in more detail.
The input is an  $(\{V_I, \{\tau_O\}, \Sigma_I,$ $ \{\bot, \top\}, Q, q_0, \Delta\})$. W.l.o.g we assume that $V_I = \{\tau_1, ..., \tau_k\}$.
The  outputs a sequence of verdicts $\{\top, \bot\}^*$.
A violation of the property is represented by $\bot$, so
whenever $\bot$ appears on the output, the algorithm terminates and reports the violation.
A simple modification is to terminate on true.

A configuration is a 4-tuple $(\sigma, (p_1, ..., p_k), M, e)$ where
$\sigma$ is a function that maps trace variables to traces,
the vector $(p_1, ..., p_k)$ keeps track of
reading positions in the input traces, $M$ is the current m-map gathered
while evaluating the of $e$, and $e$ is the edge that is being evaluated.
More precisely, $e$ is the edge that still needs to be evaluated in the future
as its gets repeatedly rewritten during the run of the algorithm.
If the edge has $E$, we write
$E[\tau \mapsto \xi]$ for the created from $E$ by setting the for $\tau$ to $\xi$.

The algorithm uses three global variables.
Variable $\val{workbag}$ stores configurations to be processed.
Variable $\val{traces}$ is a map that remembers the so-far-seen contents of all traces.
Whenever a new event arrives on a trace $t$,
we append it to $\val{traces}(t)$.
Traces on which a new event may still arrive are stored in variable
Note that to follow the spirit of online monitoring setup,
in this section, we treat traces as opaque objects
that we query for next events.

In each iteration of the main loop (line <ref>), the algorithm
first calls the procedure  (line <ref>,
the procedure is defined in Algorithm <ref>).

This procedure adds new traces to $\val{onlinetraces}$ and
updates $\val{workbag}$ with new configurations if there are any new traces,
and extends traces in $\val{traces}$ with new events.

The core of the algorithm are lines <ref>–<ref>
that take all configuration sets and update them with unprocessed events.

The algorithm pops every set of configurations from $\val{workbag}$
(lines <ref>–<ref>)
and attempts to make a progress on every configuration in the set (line <ref>).
For each trace where a progress can be made in the current configuration
(line <ref>),
i.e., there is an unprocessed
event on the trace $\tau_i$ ($p_i < |\val{traces}(\sigma(\tau_i))|$), and the
corresponding on the edge still has not matched ($E(\tau_i) \not =
\epsilon$), we do a step on this (line <ref>).
The new state of the configuration is aggregated into the primed temporary variables
($E', M', ...$).

If the  matches (lines <ref> and <ref>),
we check if other configurations from the set have progressed enough for us to be
sure that this configuration has matched the shortest prefix (line <ref>).
That is, we compare $p'_1, ..., p'_k$ against positions $p''_1, ..., p''_k$ from each other configuration in $C$ if it is strictly smaller
(i.e., $p'_i \le p''_i$ for all $i$ and there is $j$ s.t., $p'_j < p''_j$).
If this is true, we can be sure that there is no other edge that
can match a shorter prefix and that has not matched it yet because it was waiting for events.
If this configuration is the shortest match,
the output of the edge is checked if it contains $\bot$ (line <ref>)
and if so, false with the counterexample is returned on line <ref>
because the monitored property is violated.

Else, the code falls-through to line <ref> that queues
new configurations for successor edges as the current edge has been successfully matched
and then continues with a new iteration of the outer-most loop (line <ref>).
The continue statement has the effect that all other configurations derived from the
same state (other edges) are dropped and therefore progress is made only on the
configuration (edge) that matched.

If any progress on the can be made in the future, or it has already matched
but we do not know if it is the shortest match yet,
the modified configuration is pushed into the set
of configurations instead of the original one (line <ref>).
If not all the configurations from $C$ were dropped because they could not proceed,
line <ref> pushes the modified set of configurations back to
workbag and new iteration starts.

§.§ Discussion

To see that the algorithm is correct, let us follow the evolution of the set
of configurations for a single instance of the  on traces $t_1, ..., t_k$.
The initial set of configurations corresponding to outgoing edges from
the initial state is created and put to $\val{workbag}$
exactly once on line <ref> in Algorithm <ref>.
When it is later popped from workbag on lines <ref>–<ref> (we are back in Algorithm <ref>), every configuration (edge) is updated – a step is taken on every
from the edge's (lines <ref>–<ref>)
where a step can be made.
If matching the fails, the configuration is discarded due to the jump on line <ref>
or line <ref>.
If matching the has neither failed nor succeeded (and no violation has been found,
in which case the algorithm would immediately terminate),
the updated configuration is pushed back to $\val{workbag}$ and revisited in later iterations.
If the has been successfully matched and it is not known to be the shortest match, it is put back
to $\val{workbag}$ and revisited later when other configurations may have proceeded and we
may again check if it is the shortest match or not.
If it is the shortest match, its successor edges are queued to $\val{workbag}$
on line <ref> (if no violation is found).
This way we incrementally first match the first edge on the run of
the on traces $t_1, ..., t_k$ (or find out that no edge matches),
then the second edge after it gets queued into $\val{workbag}$
on line <ref>, and so on.

The algorithm terminates if the number of traces is bounded.
If it has not terminated because of finding a violation on line <ref>,
it will terminate on line <ref>.
To see that the condition on line <ref> will eventually get true if the number
of traces is bounded, it is enough to realize that unless a configuration
gets matched or failed, it is discarded at latest when failing the condition
on line <ref> after reading entirely (finite) input traces.
Otherwise, if a configuration fails, the set is never put back to $\val{workbag}$
and if it gets matched, it can get back to $\val{workbag}$ repeatedly
only until the shortest match is identified. But if
every event comes in finite time, some of the configurations in the set will eventually
be identified as the shortest match (because the is deterministic), and the set of configurations will be done.
Therefore, $\val{workbag}$ will eventually become empty.

Worth remark is that if we give up on checking if the matched is the shortest
match on line <ref> (we set the condition to true)
and on line <ref>, we continue with the loop
on line <ref> instead of with the outer-most loop, i.e.,
we do not discard the set of configurations upon a successfully taken edge,
the algorithm will work also for generic non-deterministic s.

There is another difference between our algorithm and the algorithm of
Finkbeiner et al. [35, 37, 42].
In our algorithm, we assume that existing traces may be extended at any time
until the last event has been seen.
The algorithm of Finkbeiner et al. assumes that when a new trace appears, its
contents is entirely known.
So their algorithm is incremental on the level of traces, while our algorithm
is incremental on the level of traces and events.

The monitor templates in the algorithm of Finkbeiner et al.
are automata whose edges match propositions on different traces. Therefore, they can
be seen as trivial s where each prefix expression is a single letter or $\epsilon$.
Realizing this, we could say that our monitoring algorithm is an asynchronous
extension of the algorithm of Finkbeiner et al. where we allow to read multiple
letters on edges, or, alternatively, that in the context of monitoring
hyperproperties, s are a generalization of HyperLTL template automata
to asynchronous settings.

§ EMPIRICAL EVALUATION

We conducted a set of experiments about monitoring
asynchronous version of OD on random and semi-random traces.
The traces contain input and output events
with  $\in \{$$, $ $\}$,
and  a 64-bit unsigned number.
Further, a trace can contain

the event  without parameters that abstracts any event
that have occurred in the system, but that is irrelevant to OD.

q/.style = scale=1, draw, circle, minimum width=7mm, align=left,
lab-edge/.style = scale=0.8, align=left
[q] (0) at (0,0) $q_{0}$;
[q] (1) at (5,0) $q_{1}$;
[q] (2) at (-8.5,0) $q_{2}$;

[->] ($(0.south) + (0, -3mm)$) to (0);
[->] (0) to[loop] node[lab-edge, yshift=10mm, xshift=0mm]

$\tau_1: \iter{E}{\lab{e_1}{I_l + O_l}}$

$\tau_2: \iter{E}{\lab{e_2}{I_l + O_l}}$

1c$\tau_1[e_1] = \tau_2[e_2]$

[->] (0) to node[lab-edge, yshift=10mm, xshift=4mm]

$\tau_1: \iter{E}{\lab{e_1}{O_l + \$}}$

$\tau_2: \iter{E}{\lab{e_2}{O_l + \$}}$

1c$\tau_1[e_1] \not = \tau_2[e_2]$

$\leadsto \tau_o \mapsto \bot$

[->] (0) to node[lab-edge, yshift=16mm, xshift=0mm]

$\tau_1: \iter{E}{\lab{e_1}{O_l + I_l + \$}}$

$\tau_2: \iter{E}{\lab{e_2}{O_l + I_l + \$}}$

$\tau_1[e_1] \not = \tau_2[e_2]~\land$

$\tau_1[e_1] = O_l \implies \tau_2[e_2] \not \in \{O_l, \$\}~\land$

$\tau_2[e_2] = O_l \implies \tau_1[e_1] \not \in \{O_l, \$\}$

$\leadsto \tau_o \mapsto \top$

The used for monitoring asynchronous OD in the experiments.

The used for monitoring OD is

a modified version of the for monitoring OD from Section <ref>, and is shown in Figure <ref>.
The modification makes the handle also traces with different number and order of input and output events.

The letter $\$$ represents the end of trace and is automatically appended to the input traces.
We abuse the notation and write $\tau_1[e_1] = O_l$ for the expression that would be formally a disjunction comparing $\tau_1[e_1]$ to all possible constants represented by $O_l$. However, in the implementation, this is a simple constant-time check of the type of the event, identical to checking that an event matches $O_l$ when evaluating prefix expressions.
The term $\tau_i[e_i] \not \in \{O_l, \$\}$ is just a shortcut for
$\tau_i[e_i] \not = O_l \land \tau_i[e_i] \not = \$$.

The self-loop transition in the in Figure <ref> has no output and we enabled the algorithm to stop processing traces whenever $\top$ is detected on the output of the transducer
because that means that OD holds for the input traces.
Also, we used the reduction of traces [36] – because OD is symmetric and reflexive, then if we evaluate it on the tuple of traces $(t_1, t_2)$, we do not have to evaluate it for $(t_2, t_1)$ and $(t_i, t_i)$.

CPU time and maximal memory consumption of monitoring asynchronous OD on random traces with approx. 10% of low input events and 10% of low output events. Values are the average of 10 runs.

Monitors were implemented in C++ with the help of the framework
[22]. The experiments were run on a machine
with AMD EPYC CPU with the frequency 3.1 GHz.
An artifact with the implementation of the algorithm and scripts to reproduce the experiments can be found on Zenodo[

§.§.§ Experiments on random traces

In this experiment, input traces of different lengths were generated such that approx. 10% were low input and 10% low output events.
These events always carried the value 0 or 1 to increase the chance
that some traces coincide on inputs and outputs.

Results of this experiment are depicted in Figure <ref>.
The left plot shows that the monitor is capable of processing hundreds of traces in a short time and seem to scale well with the number of traces, irrespective of the length of traces.
The memory consumption is depending more on the length of traces as shown in
the middle plot. This is expected as all the input traces are stored in memory.
Finally, the maximal size of the workbag grows linearly with the number of traces
but not with the length of traces, as the right plot shows.

§.§.§ Experiments on periodic traces

In this experiment, we generated a single trace that contains low input and output events periodically with fixed distances.
Multiple instances of this trace were used as the input traces.

The goal of the experiment is to see how the monitor performs on traces that must be processed to the very end and if the performance is affected by the layout of events.

The plots in Figure <ref> show that
the monitor scales worse than on random traces as it has to always process the traces to their end. For the same reason, the performance
of the monitor depends more on the length of the traces.
Still, it can process hundreds of traces in a reasonable time.
The data do not provide a clear hint on how the distances between events change the runtime, but they do not affect it significantly.

The memory consumption remains unaffected by distances.

The plot shows CPU time and memory consumption of monitoring asynchronous OD on instances of the same trace with low input and output events laid out periodically with fixed distances.

§ RELATED WORK

In this section, we review the most closely related work.
More exhaustive review can be found in the extended version of this paper [21].

Logics for hyperproperties
Logics for hyperproperties are typically created by extending a logic for trace
properties. Hyperlogics HyperLTL [25],
HyperCTL$^*$ [25], and
HyperQPTL [56] extend LTL [55],
CTL$^*$ [32], and QPTL [60], resp.,
with explicit quantification over traces.
The logic FO[<,E] [39] and S1S[E] [27]
are first- and second- order logics with successors
extended with the equal level predicate
that relates the same time points on different traces.
TeamLTL [50, 63] extends LTL with team semantics,
where teams are sets of traces.
Many other formalism were introduced to describe hyperproperties [31, 16, 27, 40, 15, 7, 2].

All of the hitherto mentioned logics use synchronous time model.
Asynchronous HyperLTL [9],
Stuttering HyperLTL [17], and Context HyperLTL [17]
are extensions of HyperLTL to asynchronous time model.
Gutsfeld et al. [41] introduce very expressive
Multi-tape Alternating Asynchronous Word Automata (AAWA)
and the temporal fixpoint calculus $H_\mu$ for the specification and analysis
of asynchronous hyperproperties. AAWAs are
so far the only automata-based formalism for specification of asynchronous hyperproperties.
Beutner et al. define HyperATL$^*$ [12],
an extension of the logic ATL$^*$ [4] that can capture
asynchronous hyperproperties via quantification over strategies of a scheduler.
Hypernode automata [8] introduced by Bartocci et al.
combine finite-state automata with the hypertrace logic which allows to describe
properties that have multiple ,,phases”. The hypertrace logic ignores stuttering and prefixing to enable asynchronous time model.

Runtime monitoring of hyperproperties
The first paper on runtime monitoring of hyperproperties
is due to Agrawal and Bonakdarpur [3].
They consider monitoring hyperproperties specified with HyperLTL.
In general, monitoring algorithms for hyperproperties can be classified
as combinatorial or constraint-based [42].
Combinatorial algorithms [35, 36, 42]
construct multiple instances of an monitoring automaton and therefore our
algorithm fall into this category.
Constraint-based algorithms [18, 43, 42, 2]
translate the monitoring task into a set of constraints (e.g., SMT formulae)
and apply rewriting and solving  of the constraints to monitor a given hyperproperty.

Stream runtime verification (SRV) [58] specifies monitoring
as transformation of streams of data, which makes SRV also related to transducers.
It is common that there are multiple input and output streams in an SRV specification,

languages like TeSSLa [51] support
asynchronous time model. So far as we know, no one has used
SRV languages in the context of hyperproperties yet.

BeepBeep [44] and  [22]
are stream processors designed not only for runtime monitoring.
Both frameworks support an unbounded number of input streams.
allows their dynamic creation, and as for BeepBeep,
one can use its API to program the same functionality.

Neither of the frameworks was considered in the context of hyperproperties yet
– we used some data structures from in the implementation of our monitors,
but we have not used its capabilities as a stream processor.

There are many works on the monitorability and the complexity of monitoring
hyperproperties [3, 13, 14, 37, 61, 30].

- combination with static analysis [14] to tackle the monitorability problem
- reduction to monitoring trace properties [54], focused on 2-safety, which includes "1 variants of many interesting security properties including noninteference [25], integrity
[10], software doping [5, 13], and data minimality [3]."
- alternation-free fragment of HyperLTL[18], space independent of the number of traces

Runtime enforcement
Runtime enforcement [59, 33] is the process of
transforming input streams into output streams such that the output streams
satisfy a given property, usually a security policy.
Runtime enforcement of hyperproperties was explored by Coenen et al. [28].

Prefix transducers also transform input streams to output streams and thus
could be used to enforce (at least some) policies[
At least on the abstract level, the enforcement has usually also the other part that actually modifies the running system.

Automata and regular expressions
Automata [47] and transducers [62] are the basis of s and are well explored.
PEs are closely tied with the co-inductive definition of automata [57] because
both are based on language derivatives [19, 5].
In fact, the decomposition function $\rho$ can be directly used
to define the co-algebra of s.
Multi-track automata [20] are automata that read n-tuples of letters.
They commonly use also a special letter $\lambda$ for a gap (no letter) and thus can describe asynchronous reading of words.

Regular expressions (RE) [47] are an ubiquitous
formalism with many uses and many restrictions/extensions.
Prefixed regular expressions (PRE) [6]
are a subset of REs

with some properties similar to PEs.
Semantically, prefix-free REs [45] are closer to PEs than PREs,

because PEs give raise to prefix-free languages as follows from <cit.>
and the fact that a PE corresponds to a prefix-free transducer [21].
REs with the shortest-match semantics [24]
are very close to PEs, however, unlike PEs, they can be ambiguous.

s with a single input word could be seen as a modification of
expression automata [46], which are automata with REs on edges.

s use binary version of Kleene star.
The “original” star defined by Kleene was actually binary [49, 11].
Kleene, however, did not have restrictions on the right-hand side of the star
as we do and it developed in a short time into the more engaging unary star that people use today [29].

Backreferences in regular expressions refer to
parts of the word that were already matched [53, 23].
They can be even named [10], raising more similarities to our labels.
In REs, backreferences bring a great power as they allow
non-regular languages to be matched [10].
s can also recognize some non-regular patterns, however,
labels are much weaker than backreferences because constraints
are evaluated only a posteriori, while backreferences modify the way how REs are matched.

unambiguity in formalism

§ CONCLUSION AND FUTURE WORK

We introduced prefix expressions and multi-trace prefix transducers, a formalism that we see as a natural executable specification
for the monitoring of synchronous and asynchronous hyperproperties.
Prefix expressions are similar to regular expressions, but match only prefixes of words.
The reason why we prefer prefix expressions over regular expressions (that could also be used to match prefixes) is that our
prefix expressions are deterministic and unambiguous.
These properties make evaluating prefix expressions efficient.
The matched prefixes, more precisely their parts that were explicitely labeled, can be then reasoned about using logical formulae, which are a part of multi-trace
prefix expressions that extend prefix expressions to multiple words.
Multi-trace prefix expressions are used as guards on edges in multi-trace prefix transducers, which incrementally match and consume
prefixes of input words and transform them into output words.
Combining prefix expressions with finite state transducers allows us to read input words asynchronously (matching prefix expressions)
with synchronisation points (states of the transducer).
Combining finite state transducers with a ”labeled“ version of some other formalism like LTL or regular expressions would work similarly well if one solves or accepts possible non-determinism and unambiguity of these formalisms.

We use prefix transducers to monitor synchronous and asynchronous hyperproperties.
Our experimental evaluation of monitoring asynchronous observational determinism shows that a prefix-transducer-based monitoring
algorithm can scale to thousands of traces.

Prefix transducers provide a flexible formalism for optimizing monitoring algorithms.
We currently implement an asynchronous monitoring algorithm that uses prefix transducers to summarize the seen traces,
similar to the constraint-based algorithms for monitoring synchronous hyperproperties [42].
We also want to analyze the transducers to avoid instantiating them on redundant tuples of traces,
similar to the optimizations for HyperLTL monitors [36].
Furthermore, the evaluation of prefix transducers provides many opportunities for parallelization,
ranging from parallelizing the workbag in Algorithm <ref> to evaluating prefix expressions for different traces in parallel.
Finally, we work on compiling prefix transducers from a high-level logical specification languages for asynchronous hyperproperties,
namely [8].
All our implementation work is carried out to extend the  [22] software infrastructure for monitoring.

We could adapt known formalisms, for example LTL or regular expressions (RE)
to be used instead of prefix expressions on edges of transducers.
Labeling of sub-expressions is not strictly tied to prefix expressions
and we could have also "labeled" versions of LTL or REs.
With these formalisms, however, we need to take care of things like ambiguity,
to make sure that matched labeled substrings are uniquely determined –
or, alternatively, allow non-unique matches and thus introduce more
non-determinism in matching. We chose to use prefix expressions as they
are deterministic and seem to be the right formalism for our needs,
but exploring possibilities of "labeled" REs or LTL could be interesting
future work. The advantage of using REs or LTL would be that these are well-known
formalisms, people know how to use them, and the specifications could be
shorter than with prefix expressions just because the non-determinism.

§.§.§ Acknowledgements
This work was supported in part by the ERC-2020-AdG 101020093.
The authors would like to thank Ana Oliveira da Costa for commenting on a draft of the paper.

[1]
Lectures on Runtime Verification - Introductory and Advanced Topics, LNCS, vol.
10457. Springer (2018). 10.1007/978-3-319-75632-5

[2]
Aceto, L., Achilleos, A., Anastasiadi, E., Francalanza, A.: Monitoring
hyperproperties with circuits. In: FORTE 2022. LNCS, vol. 13273, pp. 1–10.
Springer (2022). 10.1007/978-3-031-08679-3_1

[3]
Agrawal, S., Bonakdarpour, B.: Runtime verification of $k$-safety
hyperproperties in HyperLTL. In: CSF 2016. pp. 239–252. IEEE (2016).

[4]
Alur, R., Henzinger, T.A., Kupferman, O.: Alternating-time temporal logic. J.
ACM  49(5),  672–713 (2002). 10.1145/585265.585270

[5]
Antimirov, V.M.: Partial derivatives of regular expressions and finite
automaton constructions. Theor. Comput. Sci.  155(2),  291–319
(1996). 10.1016/0304-3975(95)00182-4

[6]
Baeza-Yates, R.A., Gonnet, G.H.: Fast text searching for regular expressions
or automaton searching on tries. J. ACM  43(6),  915–936 (1996).

[7]
Bartocci, E., Ferrère, T., Henzinger, T.A., Nickovic, D., da Costa, A.O.:
Flavors of sequential information flow. In: VMCAI 2022. LNCS, vol. 13182,
pp. 1–19. Springer (2022). 10.1007/978-3-030-94583-1_1

[8]
Bartocci, E., Henzinger, T.A., Nickovic, D., da Costa, A.O.: Hypernode automata
(2023). 10.48550/arXiv.2305.02836

[9]
Baumeister, J., Coenen, N., Bonakdarpour, B., Finkbeiner, B., Sánchez,
C.: A temporal logic for asynchronous hyperproperties. In: CAV 2021. LNCS,
vol. 12759, pp. 694–717. Springer (2021).

[10]
Berglund, M., van der Merwe, B.: Regular expressions with backreferences
re-examined. In: Stringology Conference 2017. pp. 30–41. Czech Technical
University in Prague (2017),

[11]
Bergstra, J.A., Bethke, I., Ponse, A.: Process algebra with iteration and
nesting. Comput. J.  37(4),  243–258 (1994).
10.1093/comjnl/37.4.243, <https://doi.org/10.1093/comjnl/37.4.243>

[12]
Beutner, R., Finkbeiner, B.: A temporal logic for strategic hyperproperties.
In: CONCUR 2021. LIPIcs, vol. 203, pp. 24:1–24:19. Schloss Dagstuhl -
Leibniz-Zentrum für Informatik (2021).

[13]
Bonakdarpour, B., Finkbeiner, B.: The complexity of monitoring hyperproperties.
In: CSF 2018. pp. 162–174. IEEE (2018). 10.1109/CSF.2018.00019

[14]
Bonakdarpour, B., Sánchez, C., Schneider, G.: Monitoring hyperproperties
by combining static analysis and runtime verification. In: ISoLA 2018.
LNCS, vol. 11245, pp. 8–27. Springer (2018).

[15]
Bonakdarpour, B., Sheinvald, S.: Finite-word hyperlanguages. In: LATA 2021.
LNCS, vol. 12638, pp. 173–186. Springer (2021).

[16]
Bozzelli, L., Maubert, B., Pinchinat, S.: Unifying hyper and epistemic temporal
logics. In: FoSSaCS 2015. LNCS, vol. 9034, pp. 167–182. Springer (2015).

[17]
Bozzelli, L., Peron, A., Sánchez, C.: Asynchronous extensions of
HyperLTL. In: LICS 2021. pp. 1–13. IEEE (2021).

[18]
Brett, N., Siddique, U., Bonakdarpour, B.: Rewriting-based runtime verification
for alternation-free hyperltl. In: TACAS 2017. LNCS, vol. 10206, pp. 77–93
(2017). 10.1007/978-3-662-54580-5_5

[19]
Brzozowski, J.A.: Derivatives of regular expressions. J. ACM  11(4),
481–494 (1964). 10.1145/321239.321249

[20]
Bultan, T., Yu, F., Alkhalaf, M., Aydin, A.: Relational String Analysis, pp.
57–68. Springer (2017). 10.1007/978-3-319-68670-7_5

[21]
Chalupa, M., Henzinger, T.A.: Monitoring hyperproperties with prefix
transducers (2023), arXiv

[22]
Chalupa, M., Muehlboeck, F., Lei, S.M., Henzinger, T.A.: Vamos: Middleware for
best-effort third-party monitoring. In: FASE 2023. LNCS, vol. 13991, pp.
260–281. Springer (2023). 10.1007/978-3-031-30826-0_15

[23]
Chida, N., Terauchi, T.: On lookaheads in regular expressions with
backreferences. In: FSCD 2022. LIPIcs, vol. 228, pp. 15:1–15:18. Schloss
Dagstuhl - Leibniz-Zentrum für Informatik (2022).

[24]
Clarke, C.L.A., Cormack, G.V.: On the use of regular expressions for searching
text. ACM Trans. Program. Lang. Syst.  19(3),  413–426 (1997).

[25]
Clarkson, M.R., Finkbeiner, B., Koleini, M., Micinski, K.K., Rabe, M.N.,
Sánchez, C.: Temporal logics for hyperproperties. In: POST 2014.
LNCS, vol. 8414, pp. 265–284. Springer (2014).

[26]
Clarkson, M.R., Schneider, F.B.: Hyperproperties. J. Comput. Secur.
18(6),  1157–1210 (2010). 10.3233/JCS-2009-0393

[27]
Coenen, N., Finkbeiner, B., Hahn, C., Hofmann, J.: The hierarchy of
hyperlogics. In: LICS 2019. pp. 1–13. IEEE (2019).

[28]
Coenen, N., Finkbeiner, B., Hahn, C., Hofmann, J., Schillo, Y.: Runtime
enforcement of hyperproperties. In: ATVA 2021. LNCS, vol. 12971, pp.
283–299. Springer (2021). 10.1007/978-3-030-88885-5_19

[29]
Copi, I.M., Elgot, C.C., Wright, J.B.: Realization of events by logical nets.
J. ACM  5(2),  181–196 (apr 1958). 10.1145/320924.320931,

[30]
Damanafshan, M., Fallah, M.S.: Monitorable hyperproperties of nonterminating
systems. J. Log. Algebraic Methods Program.  128,  100796 (2022).

[31]
Dimitrova, R., Finkbeiner, B., Kovács, M., Rabe, M.N., Seidl, H.: Model
checking information flow in reactive systems. In: VMCAI 2012. LNCS,
vol. 7148, pp. 169–185. Springer (2012). 10.1007/978-3-642-27940-9_12

[32]
Emerson, E.A., Halpern, J.Y.: "sometimes" and "not never" revisited: on
branching versus linear time temporal logic. J. ACM  33(1),
151–178 (1986). 10.1145/4904.4999

[33]
Falcone, Y., Mounier, L., Fernandez, J., Richier, J.: Runtime enforcement
monitors: composition, synthesis, and enforcement abilities. Formal Methods
Syst. Des.  38(3),  223–262 (2011). 10.1007/s10703-011-0114-4

[34]
Finkbeiner, B., Haas, L., Torfah, H.: Canonical representations of k-safety
hyperproperties. In: CSF 2019. pp. 17–31. IEEE (2019).

[35]
Finkbeiner, B., Hahn, C., Stenger, M., Tentrup, L.: Monitoring hyperproperties.
In: RV 2017. LNCS, vol. 10548, pp. 190–207. Springer (2017).

[36]
Finkbeiner, B., Hahn, C., Stenger, M., Tentrup, L.: RVHyper: A runtime
verification tool for temporal hyperproperties. In: TACAS 2018. LNCS, vol.
10806, pp. 194–200. Springer (2018). 10.1007/978-3-319-89963-3_11

[37]
Finkbeiner, B., Hahn, C., Stenger, M., Tentrup, L.: Monitoring hyperproperties.
Formal Methods Syst. Des.  54(3),  336–363 (2019).

[38]
Finkbeiner, B., Hahn, C., Stenger, M., Tentrup, L.: Efficient monitoring of
hyperproperties using prefix trees. Int. J. Softw. Tools Technol. Transf.
22(6),  729–740 (2020). 10.1007/s10009-020-00552-5

[39]
Finkbeiner, B., Zimmermann, M.: The first-order logic of hyperproperties. In:
STACS 2017. LIPIcs, vol. 66, pp. 30:1–30:14. Schloss Dagstuhl -
Leibniz-Zentrum für Informatik (2017).

[40]
Gutsfeld, J.O., Müller-Olm, M., Ohrem, C.: Propositional dynamic logic
for hyperproperties. In: CONCUR 2020. LIPIcs, vol. 171, pp. 50:1–50:22.
Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2020).

[41]
Gutsfeld, J.O., Müller-Olm, M., Ohrem, C.: Automata and fixpoints for
asynchronous hyperproperties. In: POPL 2021. pp. 1–29 (2021).

[42]
Hahn, C.: Algorithms for monitoring hyperproperties. In: RV 2019. LNCS, vol.
11757, pp. 70–90. Springer (2019). 10.1007/978-3-030-32079-9_5

[43]
Hahn, C., Stenger, M., Tentrup, L.: Constraint-based monitoring of
hyperproperties. In: TACAS 2019. LNCS, vol. 11428, pp. 115–131. Springer
(2019). 10.1007/978-3-030-17465-1_7

[44]
Hallé, S., Khoury, R.: Event stream processing with beepbeep 3. In:
RV-CuBES 2017. Kalpa Publications in Computing, vol. 3, pp. 81–88.
EasyChair (2017). 10.29007/4cth

[45]
Han, Y., Wang, Y., Wood, D.: Prefix-free regular-expression matching. In: CPM
2005. LNCS, vol. 3537, pp. 298–309. Springer (2005).

[46]
Han, Y., Wood, D.: The generalization of generalized automata: Expression
automata. In: CIAA 2004, Revised Selected Papers. LNCS, vol. 3317, pp.
156–166. Springer (2004). 10.1007/978-3-540-30500-2_15

[47]
Hopcroft, J.E., Ullman, J.D.: Introduction to Automata Theory, Languages and
Computation. Addison-Wesley (1979)

[48]
Huisman, M., Worah, P., Sunesen, K.: A temporal logic characterisation of
observational determinism. In: CSFW 2006. p. 3. IEEE (2006).

[49]
Kleene, S.C.: Representation of events in nerve nets and finite automata.
Automata Studies pp. 3–41 (1956)

[50]
Krebs, A., Meier, A., Virtema, J., Zimmermann, M.: Team semantics for the
specification and verification of hyperproperties. In: MFCS 2018. LIPIcs,
vol. 117, pp. 10:1–10:16. Schloss Dagstuhl - Leibniz-Zentrum für
Informatik (2018). 10.4230/LIPIcs.MFCS.2018.10

[51]
Leucker, M., Sánchez, C., Scheffel, T., Schmitz, M., Schramm, A.: Tessla:
runtime verification of non-synchronized real-time streams. In: SAC 2018.
pp. 1925–1933. ACM (2018). 10.1145/3167132.3167338

[52]
McLean, J.: Security models and information flow. In: SP 1990. pp. 180–189.
IEEE (1990). 10.1109/RISP.1990.63849

[53]
Penna, G.D., Intrigila, B., Tronci, E., Zilli, M.V.: Synchronized regular
expressions. Acta Informatica  39(1),  31–70 (2003).

[54]
Pinisetty, S., Schneider, G., Sands, D.: Runtime verification of
hyperproperties for deterministic programs. In: FormaliSE 2018. pp. 20–29.
ACM (2018). 10.1145/3193992.3193995

[55]
Pnueli, A.: The temporal logic of programs. In: FOCS 1977. pp. 46–57. IEEE
(1977). 10.1109/SFCS.1977.32

[56]
Raabe, M.N.: A Temporal Logic Approach to Information-flow Control. Ph.D.
thesis, Saarland University (2016)

[57]
Rutten, J.J.M.M.: Automata and coinduction (an exercise in coalgebra). In:
CONCUR '98. LNCS, vol. 1466, pp. 194–218. Springer (1998).

[58]
Sánchez, C.: Synchronous and asynchronous stream runtime verification.
In: VORTEX 2021. pp. 5–7. ACM (2021). 10.1145/3464974.3468453

[59]
Schneider, F.B.: Enforceable security policies. ACM Trans. Inf. Syst. Secur.
3(1),  30–50 (2000). 10.1145/353323.353382

[60]
Sistla, A.P.: Theoretical Issues in the Design and Verification of Distributed
Systems. Ph.D. thesis, Harvard University (1983)

[61]
Stucki, S., Sánchez, C., Schneider, G., Bonakdarpour, B.: Gray-box
monitoring of hyperproperties. In: FM 2019. LNCS, vol. 11800, pp. 406–424.
Springer (2019). 10.1007/978-3-030-30942-8_25

[62]
Veanes, M., Hooimeijer, P., Livshits, B., Molnar, D., Bjørner, N.S.:
Symbolic finite state transducers: algorithms and applications. In: POPL
2012. pp. 137–150. ACM (2012). 10.1145/2103656.2103674

[63]
Virtema, J., Hofmann, J., Finkbeiner, B., Kontinen, J., Yang, F.: Linear-time
temporal logic with team semantics: Expressivity and complexity. In: FSTTCS
2021. LIPIcs, vol. 213, pp. 52:1–52:17. Schloss Dagstuhl - Leibniz-Zentrum
für Informatik (2021). 10.4230/LIPIcs.FSTTCS.2021.52

[64]
Zdancewic, S., Myers, A.C.: Observational determinism for concurrent program
security. In: CSFW 2003. p. 29. IEEE (2003).

§.§ Prefix expressions

There are only finitely many s that we can obtain
from a by repeated application of $\step{a}{p}$ for
any $a$ and a fixed $p$.

Given a number $p\in\mathbb{N}$ and an arbitrary $\alpha$ over an alphabet $\Sigma$, the set

\[
D_p(\alpha) = \{\alpha' \mid \alpha \step{a_0}{p} ... \step{a_k}{p} \alpha', a_1, ..., a_k \in \Sigma\}
\]

is finite.

Every rule except Iter is shortening.
Application of $\step{a}{p}$ on $\iter{\alpha}{\beta}$ is either $\epsilon$
or $\alpha'\cdot\iter{\alpha}{\beta}$. If $\alpha$ contains nested iteration,
the expression can get extended further to the left,
but because the nesting of iterations must be finite,
at some point the left-hand side of the left-most iteration,
let us call this iteration expression $\xi$,
has no nested iteration and repeatedly applying one-step
relation leads to shortening the expression until $\xi$ again becomes the left-most
expression (or the whole expression evaluates to $\bot$).
From this point on,
any expression obtained by one-step relation is either shorter than the original one
or it has been already seen.

To strengthen the intuition behind the proof sketch above, here are depicted
possible evaluations of an expression over the alphabet $\{a, b, c\}$ with two nested iterations (we do not show the parameter $p$):

[anchor=west](1) at (0, 0) $\iter{(\iter{ab}{c})}{c}$;
[anchor=west](2) at (3, 0) $b(\iter{ab}{c})\iter{(\iter{ab}{c})}{c}$;
[anchor=west](3) at (7, 0) $(\iter{ab}{c})\iter{(\iter{ab}{c})}{c}$;
[below=of 1](e) $\epsilon$;
[below=of 2](b) $\bot$;
(1) edge[double, ->] node[yshift=3mm] $a$(2);
(1) edge[double, ->] node[xshift=3mm] $c$(e);
(2) edge[double, ->] node[yshift=3mm] $b$(3);
(3) edge[bend left, double, ->] node[yshift=-3mm] $a$(2);
(3) edge[bend right, double, ->] node[yshift=3mm] $c$(1);

(1) edge[double, ->] node[yshift=3mm] $b$(b);
(2) edge[double, ->] node[xshift=4mm] $a,c$(b);
(3) edge[double, ->, bend left] node[yshift=-3mm] $b$(b);

Thanks to theorems <ref> and <ref>,
the evaluation function $\delta$ for a fixed $\alpha$ over an alphabet $\Sigma$
can be translated into a unique prefix-free [46] finite state transducer [62].
The transducer has for states the set $D_p(\alpha)$, and edges are formed as in the example above (notice that the expressions in the example above are exactly the expressions from $D_p(\iter{(\iter{ab}{c})}{c})$), i.e., for
any $a\in\Sigma$, there is the transition $\alpha_0 \xrightarrow{a,p/M} \alpha_1$
between two states iff $(\alpha_0, \emptyset) \step{a}{p} (\alpha_1, M)$. The
initial state of a transducer is the state $\alpha$

and the accepting state is $\epsilon$.
A run of the transducer on a word $w = w_0w_1...w_k$ is a sequence of
adjacent edges starting from the initial state such that the guard on $i$-th edge is $w_i, i$:

(\alpha)\xrightarrow{w_0, 0/M_0} (\alpha_1) \xrightarrow{w_1,1/M_1} ...
\xrightarrow{w_{k-1},k-1/M_{k-1}}(\alpha_k)

Further, it holds that $\delta(\alpha, w) = (\alpha_k,
M_0\mcomp...\mcomp M_{k-1})$.

An example of a transducer for
$b(\iter{\lab{l}{ab}}{b})(b+a)$ over the alphabet $\{a, b\}$
is shown in Figure <ref>.

nd/.style = fill=gray!5,draw, rounded corners, inner sep=3pt
[nd] (0) at (-1, 0)  $b(\iter{\lab{l}{ab}}{b})(b+a)$;
[nd] (1) at (3, 0)   $(\iter{\lab{l}{ab}}{b})(b+a)$;
[nd] (2) at (7, 0)   $(b+a)$;
[nd] (3) at (3, -1.5)$[b]_l(\iter{\lab{l}{ab}}{b})(b+a)$;
[nd,double, color=istagreen,fill=white]
(5) at (7, -1.5) $\epsilon$;

[->] ($(0.west) + (-5mm, 0)$)  to (0);
[->] (0) edge node[yshift=3mm]$b,p/\emptyset$ (1);
[->] (1) edge node[yshift=3mm]$b,p/\emptyset$ (2);
[->] (1) edge node[ xshift=-13mm]$a,p/\{l\mapsto(p, \bot)\}$ (3);
[] ($(3.north) + (5mm, 0)$)
edge[->] node[xshift=13mm]$b,p/\{l \mapsto (\bot, p) \}$
($(1.south) + (5mm, 0)$);

[->] (2) to node[xshift=4mm]$*/\emptyset$ (5);

Finite transducer for $b(\iter{\lab{l}{ab}}{b})(b+a)$.
Redundant states and transitions

were omitted.

Strictly formally, this transducer as shown in Figure <ref>
would be symbolic transducer [62] as the position $p$ on edges represents any natural number.
However, $p$ is rather a parameter of the transducer and it only propagates into the output of some edges.
Therefore, it would be more precise to avoid having $p$ in the guard of the edge
and, instead, output functions that take $p$ as the only parameter. For example,
instead of the m-map $\{l \mapsto (p, \bot)\}$,
we would output a map that returns the m-map: $\lambda p.\{l \mapsto (p, \bot)\}$.
The semantics of the output of the transducer then would be modified
to supply and evaluate the outputs on the right sequence of $p$s.
This approach, although formally better, seems unnecessarily complicated
for our purposes.