$(p_{j},c_{j}).{{\llparenthesis\,\varphi_{j},\Pi\,\rrparenthesis}}$ for some
$j{\,\in\,}I$, or else (ii) via the default monitor synthesised by
$\textsf{def}(\textstyle\bigwedge_{i\in
I}\mathbf{[}(p_{i},c_{i})\mathbf{]}\varphi_{i})$. We consider both
eventualities.

      1. (1)

In this case we apply rules eRec, eSel and eTrn on (90) and deduce that

$\displaystyle\exists j\in I\cdot(p_{j},c_{j})(\textsf{a}?v)=\sigma$ (95)
$\displaystyle
m^{\prime}={\llparenthesis\,\varphi_{j}\sigma,\Pi\,\rrparenthesis}.$ (96)

and so from (94), (95) and (72) we infer that
$s^{\prime}\vDash\varphi_{j}\sigma$ from which by the definition of
$\mathcal{R}$ we have that
$(s^{\prime},{\llparenthesis\,\varphi_{j}\sigma,\Pi\,\rrparenthesis}[s^{\prime}])\in\mathcal{R}$,
and so from (92) and (96) we can conclude that

$\displaystyle(s^{\prime},r^{\prime})\in\mathcal{R}$ (97)

as required, and so this case is done by (94) and (97).

      2. (2)

When we apply rules eRec, eSel and eTrn we deduce that
$m^{\prime}=\textsf{id}$ and so by the definition of
${\llparenthesis\,-\,\rrparenthesis}$ we have that

$\displaystyle m^{\prime}={\llparenthesis\,\mathsf{tt},\Pi\,\rrparenthesis}.$
(98)

Consequently, as every process satisfies $\mathsf{tt}$, we know that
$s^{\prime}\vDash\mathsf{tt}$ and so by the definition of $\mathcal{R}$ we
have that
$(s^{\prime},{\llparenthesis\,\mathsf{tt},\Pi\,\rrparenthesis}[s^{\prime}])\in\mathcal{R}$,
so that from (92) and (98) we can conclude that

$\displaystyle(s^{\prime},r^{\prime})\in\mathcal{R}$ (99)

as required. Hence this case is done by (94) and (99).

  * •

_$\mu=\textsf{a}!v$ :_ When $\mu=\textsf{a}!v$, the transition in (75) can be
performed via iDef, iTrnO or iEnO. We omit the proof for this case due to its
strong resemblance to that of case $\mu=\textsf{a}?v$.

_Case $\varphi=\mathsf{max}\,X.\varphi\emph{ and }X\in\textbf{fv}(\varphi)$._
Now, lets assume that

$\displaystyle{\llparenthesis\,\mathsf{max}\,X.\varphi,\Pi\,\rrparenthesis}[s]\xrightarrow{\;\mu\;}r^{\prime}$
(100)

and that $s\vDash\mathsf{max}\,X.\varphi$ from which by the definition of
$\vDash$ we have that

$\displaystyle s\vDash\varphi\\{{\mathsf{max}\,X.\varphi}/{X}\\}.$ (101)

Since
$\varphi\\{{\mathsf{max}\,X.\varphi}/{X}\\}{\,\in\,}\textsc{sHML}_{\textbf{nf}}$,
by the restrictions imposed by $\textsc{sHML}_{\textbf{nf}}$ we know that:
$\varphi$ cannot be $X$ because (bound) logical variables are required to be
_guarded_ , and it also cannot be $\mathsf{tt}$ or $\mathsf{ff}$ since $X$ is
required to be defined in $\varphi$, i.e., $X\in\textbf{fv}(\varphi)$. Hence,
we know that $\varphi$ can only have the following form, that is

$\displaystyle\varphi=\mathsf{max}\,Y_{0}.\ldots\mathsf{max}\,Y_{n}.\raisebox{0.86108pt}{\scalebox{0.8}{$\displaystyle\bigwedge_{i\in
I}\,$}}\mathbf{[}(p_{i},c_{i})\mathbf{]}\varphi_{i}$ (102)

and so by (101), (102) and the definition of $\vDash$ we have that

$\displaystyle s\vDash\textstyle\bigwedge_{i\in
I}\mathbf{[}(p_{i},c_{i})\mathbf{]}\varphi_{i}\\{\cdot\cdot\\}\quad\emph{
where }$ (103)
$\displaystyle\\{\cdot\cdot\\}=\\{{\mathsf{max}\,X.\varphi}/{X},{(\mathsf{max}\,Y_{0}.\ldots\mathsf{max}\,Y_{n}.\textstyle\bigwedge_{i\in
I}\mathbf{[}(p_{i},c_{i})\mathbf{]}\varphi_{i})}/{Y_{0}},\ldots\\}.$

Since ${\llparenthesis\,\textstyle\bigwedge_{i\in
I}\mathbf{[}(p_{i},c_{i})\mathbf{]}\varphi_{i}\\{\cdot\cdot\\},\Pi\,\rrparenthesis}$
synthesises the _unfolded equivalent_ of
${\llparenthesis\,\mathsf{max}\,X.\varphi,\Pi\,\rrparenthesis}$, from (100) we
know that

$\displaystyle{\llparenthesis\,\textstyle\bigwedge_{i\in
I}\mathbf{[}(p_{i},c_{i})\mathbf{]}\varphi_{i}\\{\cdot\cdot\\},\Pi\,\rrparenthesis}[s]\xrightarrow{\;\mu\;}r^{\prime}.$
(104)

Hence, since we know (103) and (104), from this point onwards the proof
proceeds as per the previous case. We thus omit showing the remainder of this
proof.

From the above cases we can therefore conclude that $(b)$ holds as well.

We are finally in a position to state and prove our eventual transparency
results following Section 4.

######  Proposition 11 (Eventual Transparency).

For every input port set $\Pi$, $\textsc{sHML}_{\textbf{nf}}$ formula
$\varphi$, system states $s,s^{\prime}{\,\in\,}\textsc{Sys}$, action disabling
monitor $m^{\prime}$ and trace $t$, if
${\llparenthesis\,\varphi,\Pi\,\rrparenthesis}[s]\xRightarrow{\;t\;}m^{\prime}[s^{\prime}]$
and $s^{\prime}\in\llbracket\textsl{after}(\varphi,t)\rrbracket$ then
$m^{\prime}[s^{\prime}]\sim s^{\prime}$. ∎

######  Proof 5.7.

We must prove that for every formula
$\varphi{\,\in\,}\textsc{sHML}_{\textbf{nf}}$ if
${\llparenthesis\,\varphi,\Pi\,\rrparenthesis}{\,=\,}m$ then
$\textsf{evtenf}(m,\varphi)$. We prove that for every
$\varphi{\,\in\,}\textsc{sHML}_{\textbf{nf}}$, if
${\llparenthesis\,\varphi,\Pi\,\rrparenthesis}[s]\xRightarrow{\;t\;}m^{\prime}[s^{\prime}]$
and $s^{\prime}\vDash\textsl{after}(\varphi,t)$ then
$m^{\prime}[s^{\prime}]\sim s^{\prime}$.

Now, assume that

$\displaystyle{\llparenthesis\,\varphi,\Pi\,\rrparenthesis}[s]\xRightarrow{\;t\;}m^{\prime}[s^{\prime}]$
(105) $\displaystyle s^{\prime}\vDash\textsl{after}(\varphi,t)$ (106)

and so from (105) and 9 we have that

$\displaystyle\exists\psi\in\textsc{sHML}_{\textbf{nf}}\cdot\psi=\textsl{after}(\varphi,t)$
(107)
$\displaystyle{\llparenthesis\,\textsl{after}(\varphi,t),\Pi\,\rrparenthesis}=m^{\prime}={\llparenthesis\,\psi,\Pi\,\rrparenthesis}.$
(108)

Hence, knowing (106) and (107), by 10 (Transparency) we conclude that
${\llparenthesis\,\textsl{after}(\varphi,t),\Pi\,\rrparenthesis}[s^{\prime}]\sim
s^{\prime}$ as required, and so we are done.

##  6\. Transducer Optimality

Recall 3 from Section 4. Through criteria such as Sections 4 and 4, it defined
what it means for a monitor to adequately enforce a formula. However, it did
_not_ assess whether a monitor is (to some extent) the “ _best_ ” that one can
find to enforce a property. In order to define such a notion we must first be
able to compare monitors to one another via some kind of _distance
measurement_ that tells them apart. One potential measurement is to assess the
monitor’s level of _intrusiveness_ when enforcing the property.

$\textsl{mc}(m,t_{\tau})\,\overset{\leavevmode\resizebox{6.0pt}{}{\,{def}}\,}{=}\,\left\\{\begin{array}[]{cl}1+\textsl{mc}(m^{\prime},t_{\tau}^{\prime})&\emph{
if }t_{\tau}{\,=\,}\mu t_{\tau}^{\prime}\emph{ and }m[\textsf{sys}(\mu
t_{\tau}^{\prime})]\xrightarrow{\;\mu^{\prime}\;}m^{\prime}[\textsf{sys}(t_{\tau}^{\prime})]\emph{
and }\mu{\,\neq\,}\mu^{\prime}\\\ 1+\textsl{mc}(m^{\prime},t_{\tau})&\emph{ if
}t_{\tau}{\,\in\,}\\{\mu t_{\tau}^{\prime},\varepsilon\\}\emph{ and
}m[\textsf{sys}(t_{\tau})]\xrightarrow{\;\mu^{\prime}\;}m^{\prime}[\textsf{sys}(t_{\tau})]\\\\[2.84526pt]
\textsl{mc}(m^{\prime},t_{\tau}^{\prime})&\emph{ if }t_{\tau}{\,=\,}\mu
t_{\tau}^{\prime}\emph{ and }m[\textsf{sys}(\mu
t_{\tau}^{\prime})]\xrightarrow{\;\mu\;}m^{\prime}[\textsf{sys}(t_{\tau}^{\prime})]\\\
|{\,t_{\tau}\,}|&\emph{ if }t_{\tau}{\,\in\,}\\{\mu
t_{\tau}^{\prime},\varepsilon\\}\emph{ and }\forall\mu^{\prime}\cdot
m[\textsf{sys}(t_{\tau})]\mathchoice{\mathrel{\hbox to0.0pt{\kern
9.06046pt\kern-5.27776pt$\displaystyle\not$\hss}{\xrightarrow{\;\mu^{\prime}\;}}}}{\mathrel{\hbox
to0.0pt{\kern
9.06046pt\kern-5.27776pt$\textstyle\not$\hss}{\xrightarrow{\;\mu^{\prime}\;}}}}{\mathrel{\hbox
to0.0pt{\kern
7.18661pt\kern-4.11108pt$\scriptstyle\not$\hss}{\xrightarrow{\;\mu^{\prime}\;}}}}{\mathrel{\hbox
to0.0pt{\kern
6.08408pt\kern-3.3333pt$\scriptscriptstyle\not$\hss}{\xrightarrow{\;\mu^{\prime}\;}}}}\end{array}\right.$
Figure 6. Modification Count (mc).

In Figure 6 we define function mc that inductively analyses a system run,
represented as an explicit trace $t_{\tau}$, and counts the number of
modifications applied by the monitor. In each case the function reconstructs a
trace system $\textsf{sys}(t_{\tau})$ and instruments it with the monitor $m$
in order to assess the type of transformation applied. Specifically, in the
first two cases, mc increments the counter whenever the monitor adapts,
disables or enables an action, and then it recurses to keep on inspecting the
run (i.e., the suffix $t_{\tau}^{\prime}$ in the first, and the same trace
$t_{\tau}$ in the second) vis-a-vis the subsequent monitor state,
$m^{\prime}$. The third case, specifies that the counter stays unmodified when
the monitor applies an identity transformation, while the last case returns
the length of $t_{\tau}$ when $m[\textsf{sys}(t_{\tau})]$ is unable to execute
further. Recall the monitors of Section 3 and consider the following system
run
$t_{\tau}^{0}{=}\textsf{a}?v_{1}.\textsf{a}?v_{2}.\tau.\textsf{a}!w_{2}.\textsf{a}!w_{2}.\textsf{b}!(\textsf{log},v_{2},w_{2})$.
For $m_{\textbf{e}}$ and $m_{\textbf{a}}$, function mc respectively counts
three enabled actions, i.e., $\textsl{mc}(m_{\textbf{e}},t_{\tau}^{0}){=}3$,
and four adapted actions, i.e., $\textsl{mc}(m_{\textbf{a}},t_{\tau}^{0}){=}4$
(since $\textsf{b}!(\textsf{log},v_{2},w_{2})$ remains unmodified). The
maximum count of 5 is attained by $m_{\textbf{d}}$ as it immediately blocks
the first input $\textsf{a}?v_{1}$, and so none of the actions in
$t_{\tau}^{0}$ can be executed by the composite system i.e., $\forall\mu\cdot
m_{\textbf{d}}[\textsf{sys}(t_{\tau}^{0})]\\!\mathchoice{\mathrel{\hbox
to0.0pt{\kern
8.29045pt\kern-5.27776pt$\displaystyle\not$\hss}{\xrightarrow{\;\mu\;}}}}{\mathrel{\hbox
to0.0pt{\kern
8.29045pt\kern-5.27776pt$\textstyle\not$\hss}{\xrightarrow{\;\mu\;}}}}{\mathrel{\hbox
to0.0pt{\kern
6.63663pt\kern-4.11108pt$\scriptstyle\not$\hss}{\xrightarrow{\;\mu\;}}}}{\mathrel{\hbox
to0.0pt{\kern
5.53407pt\kern-3.3333pt$\scriptscriptstyle\not$\hss}{\xrightarrow{\;\mu\;}}}}$
and so $\textsl{mc}(m_{\textbf{d}},t_{\tau}^{0}){=}5$. Similarly,
$\textsl{mc}(m_{\textbf{dt}},t_{\tau}^{0}){=}4$ since $m_{\textbf{dt}}$ allows
the first request to be made, but blocks the second erroneous one, and as a
result it also forbids the execution of the subsequent actions, i.e.,
$\forall\mu\cdot
m_{\textbf{dt}}[\textsf{sys}(t_{\tau}^{0})]\xrightarrow{\;\textsf{a}?v_{1}\;}{\\!\cdot\\!}\mathchoice{\mathrel{\hbox
to0.0pt{\kern
8.29045pt\kern-5.27776pt$\displaystyle\not$\hss}{\xrightarrow{\;\mu\;}}}}{\mathrel{\hbox
to0.0pt{\kern
8.29045pt\kern-5.27776pt$\textstyle\not$\hss}{\xrightarrow{\;\mu\;}}}}{\mathrel{\hbox
to0.0pt{\kern
6.63663pt\kern-4.11108pt$\scriptstyle\not$\hss}{\xrightarrow{\;\mu\;}}}}{\mathrel{\hbox
to0.0pt{\kern
5.53407pt\kern-3.3333pt$\scriptscriptstyle\not$\hss}{\xrightarrow{\;\mu\;}}}}$.
Finally, $m_{\textbf{det}}$ performs the least number of modifications, namely
$\textsl{mc}(m_{\textbf{det}},t_{\tau}^{0}){=}2$. The first modification is
caused when the monitor blocks the second erroneous input and internally
_inserts_ a default input value that allows the composite system to proceed
over a $\tau$-action. This contrasts with $m_{\textbf{d}}$ and
$m_{\textbf{dt}}$ which fail to perform this insertion step thereby
contributing to their high intrusiveness score. The second modification is
attained when $m_{\textbf{det}}$ suppresses the redundant response.
$\hfill\blacksquare$

$\textsl{ec}(m)\,\overset{\leavevmode\resizebox{6.0pt}{}{\,{def}}\,}{=}\,\left\\{\begin{array}[]{cl}\emptyset&\emph{
if }m{\,=\,}X\\\ \bigcup_{i\in I}\textsl{ec}(m_{i})&\emph{ if
}m{\,=\,}\sum_{i\in I}m_{i}\\\ \textsl{ec}(m^{\prime})&\emph{ if
}m{\,=\,}\textsf{rec}\,X.m^{\prime}\emph{ or
}m{\,=\,}(p,c,\underline{p}).{m^{\prime}}\\\
\\{\textsf{DIS}\\}{\,\cup\,}\textsl{ec}(m^{\prime})&\emph{ if
}m{\,=\,}((x)!(y),c,\bullet).{m^{\prime}}\emph{ or
}m{\,=\,}(\bullet,c,\textsf{a}?v).{m^{\prime}}\\\
\\{\textsf{EN}\\}{\,\cup\,}\textsl{ec}(m^{\prime})&\emph{ if
}m{\,=\,}((x)?(y),c,\bullet).{m^{\prime}}\emph{ or
}m{\,=\,}(\bullet,c,\textsf{a}!v).{m^{\prime}}\\\
\\{\textsf{ADPT}\\}{\,\cup\,}\textsl{ec}(m^{\prime})&\emph{ if
}m{\,=\,}(p,c,p^{\prime}).{m^{\prime}}\emph{ and
}p^{\prime}{\,\neq\,}\underline{p}{\,\neq\,}\bullet\end{array}\right.$
Figure 7. Enforcement Capabilities (ec).

We can now use function mc to compare monitors to each other in order to
identify the least intrusive one, i.e., the monitor that applies the least
amount of transformations when enforcing a specific property. However, for
this comparison to be fair, we must also compare like with like. This means
that if a monitor enforces a formula by only disabling actions, it is only
fair to compare it to other monitors of the same kind. It is reasonable to
expect that monitors with more enforcement capabilities are likely to be
“better” than those with fewer capabilities. We determine the enforcement
capabilities of a monitor via function ec of Figure 7. It inductively analyses
the structure of the monitor and deduces whether it can enable, disable and
adapt actions based on the type of transformation triples it defines. For
instance, if the monitor defines an output suppression triple,
$((x)!(y),c,\bullet).{m^{\prime}}$, or an input insertion branch,
$(\bullet,c,\textsf{a}?v).{m^{\prime}}$, then ec determines that the monitor
can disable actions DIS, while if it defines an input suppression,
$((x)?(y),c,\bullet).{m^{\prime}}$, or an output insertion branch,
$(\bullet,c,\textsf{a}!v).{m^{\prime}}$, then it concludes that the monitor
can enable actions, EN. Similarly, if a monitor defines a replacement
transformation, it infers that the monitor can adapt actions, ADPT.

Recall the monitors of Section 3. With function ec we determine that
$\textsl{ec}(m_{\textbf{e}}){=}\\{\textsf{EN}\\}$,
$\textsl{ec}(m_{\textbf{a}}){=}\\{\textsf{ADPT}\\}$,
$\textsl{ec}(m_{\textbf{d}}){=}\textsl{ec}(m_{\textbf{dt}}){=}\textsl{ec}(m_{\textbf{det}}){=}\\{\textsf{DIS}\\}$.
Monitors may also have multiple types of enforcement capabilities. For
instance,

$\textsl{ec}(\textsf{rec}\,X.((x)?(y),\bullet).{X}+((x)!(y),\bullet).{X}){=}\\{\textsf{EN},\textsf{DIS}\\}.$
$\hfill\blacksquare$

With these definitions we now define _optimal enforcement_. [Optimal
Enforcement] A monitor $m$ is _optimal_ when enforcing $\varphi$, denoted as
$\textsf{oenf}(m,\varphi)$, iff it _enforces_ $\varphi$ (3) and when for every
state $s$, explicit trace $t_{\tau}$ and monitor $n$, if
$\textsl{ec}(n){\,\subseteq\,}\textsl{ec}(m)$, $\textsf{enf}(n,\varphi)$ and
$s\xrightarrow{\;t_{\tau}\;}$ then
$\textsl{mc}(m,t_{\tau}){\,\leq\,}\textsl{mc}(n,t_{\tau})$. ∎ Figure 7 states
that an adequate (sound and eventually transparent) monitor $m$ is _optimal_
for $\varphi$, if one cannot find another adequate monitor $n$, with the same
(or fewer) enforcement capabilities, that performs _fewer modifications_ than
$m$ and is thus _less intrusive_.

Recall formula $\varphi_{1}$ of Section 2 and monitor $m_{\textbf{det}}$ of
Section 4. Although showing that $\textsf{oenf}(m_{\textbf{det}},\varphi_{1})$
is inherently difficult, from Figure 6 we already get the intuition that it
holds since $m_{\textbf{det}}$ imposes the least amount of modifications
compared to the other monitors of Sections 3 and 3. We further reaffirm this
intuition using systems $s_{\textbf{b}}$ and $s_{\textbf{c}}$ from Section 2.
In fact, when considering the invalid runs
$t_{\tau}^{1}{\,\overset{\leavevmode\resizebox{6.0pt}{}{\,{def}}\,}{=}\,}{\textsf{a}?v_{1}.\tau.\textsf{a}!w_{1}.\textsf{a}!w_{1}.\textsf{b}!(\textsf{log},v_{1},w_{1})}$
of $s_{\textbf{b}}$, and
$t_{\tau}^{2}{\,\overset{\leavevmode\resizebox{6.0pt}{}{\,{def}}\,}{=}\,}{\textsf{a}?v_{1}.\textsf{a}?v_{2}.\tau.\textsf{a}!w_{2}.\textsf{b}!(\textsf{log},v_{2},w_{2})}$
of $s_{\textbf{c}}$, one can easily deduce that no other adequate action
disabling monitor can enforce $\varphi_{1}$ with fewer modifications than
those imposed by $m_{\textbf{det}}$, namely,
$\textsl{mc}(m_{\textbf{det}},t_{\tau}^{1}){\,=\,}\textsl{mc}(m_{\textbf{det}},t_{\tau}^{2}){\,=\,}1$.
Furthermore, consider the invalid traces
$t_{\tau}^{1}\\{^{\textsf{c}}{\\!/}_{\textsf{a}}\\}$ and
$t_{\tau}^{2}\\{^{\textsf{c}}{\\!/}_{\textsf{a}}\\}$ that are respectively
produced by versions of $s_{\textbf{b}}$ and $s_{\textbf{c}}$ that interact on
some port c instead of a (for any port $\textsf{c}{\,\neq\,}\textsf{a}$).
Since $m_{\textbf{det}}$ binds the port c to its data binder $x$ and uses this
information in its insertion branch, $(\bullet,(x?(\\_))).Y$, the _same_
modification count is achieved for these traces, as well i.e.,
$\textsl{mc}(m_{\textbf{det}},t_{\tau}^{1}\\{^{\textsf{c}}{\\!/}_{\textsf{a}}\\}){\,=\,}\textsl{mc}(m_{\textbf{det}},t_{\tau}^{2}\\{^{\textsf{c}}{\\!/}_{\textsf{a}}\\}){\,=\,}1$.
$\hfill\blacksquare$

Section 6 describes the case where formula $\varphi$ is optimally enforced by
a _finite-state_ and _finitely-branching_ monitor, $m_{\textbf{det}}$. In the
general case, this is not always possible. Consider formula $\varphi_{2}$
stating that an initial input on port a followed by another input from some
other port $x_{2}{\neq}\textsf{a}$ constitutes invalid system behaviour. Also
consider monitor $m_{1}$ where $\textsf{enf}(m_{1},\varphi_{2})$.

$\displaystyle\varphi_{2}$
$\displaystyle\,\overset{\leavevmode\resizebox{6.0pt}{}{\,{def}}\,}{=}\,\mathbf{[}(\textsf{a}?(\\_))\mathbf{]}\mathbf{[}((x_{2})?(\\_),x_{2}{\neq}\textsf{a})\mathbf{]}\mathsf{ff}$
$\displaystyle m_{1}$
$\displaystyle\,\overset{\leavevmode\resizebox{6.0pt}{}{\,{def}}\,}{=}\,(\textsf{a}?(\\_)).{\textsf{rec}\,Y.((\bullet,\textsf{b}?v_{\text{def}}).Y+(\textsf{a}?(\\_)).\textsf{id})}$

When enforcing a system that generates the run
$t_{\tau}^{3}{\,\,\overset{\leavevmode\resizebox{6.0pt}{}{\,{def}}\,}{=}\,\,}\textsf{a}?v_{1}.\textsf{b}?v_{2}.\textsf{a}!w_{1}.u_{\tau}^{3}$,
monitor $m_{1}$ modifies the trace only _once_. Although it disables the input
$\textsf{b}?v_{2}$, it subsequently unblocks the SuS by inserting
$\textsf{b}?v_{\text{def}}$ and so trace $t_{\tau}^{3}$ is transformed into
$\textsf{a}?v_{1}.\tau.\textsf{a}!w_{1}.u_{\tau}^{3}$. However, for a slightly
modified version of $t_{\tau}^{3}$, e.g.,
$t_{\tau}^{3}\\{^{\textsf{c}}{\\!/}_{\textsf{b}}\\}$, $m_{1}$ scores a
modification count of $2+|{\,u_{\tau}^{3}\,}|$. This is the case because,
although it blocks the invalid input on port c, it fails to insert the default
value that unblocks the SuS. A more expressive version of $m_{1}$, such as

$m_{2}{\,\,\overset{\leavevmode\resizebox{6.0pt}{}{\,{def}}\,}{=}\,\,}(\textsf{a}?(\\_)).{\textsf{rec}\,Y.((\bullet,\textsf{b}?v_{\text{def}}).Y+\underline{(\bullet,\textsf{c}?v_{\text{def}}).Y}+(\textsf{a}?(\\_)).\textsf{id})},$

circumvents this problem by defining an extra insertion branch (underlined),
but still fails to be optimal in the case of
$t_{\tau}^{3}\\{^{\textsf{d}}{\\!/}_{\textsf{b}}\\}$. In this case, there does
not exist a way to finitely define a monitor that can insert a default value
on every possible input port $x_{2}{\,\neq\,}\textsf{a}$. Hence, it means that
the optimal monitor $m_{\textsf{opt}}$ for $\varphi_{1}$ would be an _infinite
branching_ one, i.e., it requires a countably infinite summation that is not
expressible in Trn,

$m_{\textsf{opt}}{\,\overset{\leavevmode\resizebox{6.0pt}{}{\,{def}}\,}{=}\,}(\textsf{a}?(\\_)).{(\textsf{rec}\,Y.\sum_{\textsf{b}{\,\in\,}\textsc{Port}\emph{
and
}\textsf{a}{\neq}\textsf{b}}(\bullet,\textsf{b}?v_{\text{def}}).Y+(\textsf{a}?(\\_)).\textsf{id})}$

or alternatively

$(\textsf{a}?(\\_)).{(\textsf{rec}\,Y.\sum_{\textsf{b}{\,\in\,}\textsc{Port}}(\bullet,\textsf{a}{\neq}\textsf{b},\textsf{b}?v_{\text{def}}).Y+(\textsf{a}?(\\_)).\textsf{id})}$

where the condition $\textsf{a}{\neq}\textsf{b}$ is evaluated at runtime.
$\hfill\blacksquare$

Unlike Section 6, Figure 7 presents a case where optimality can only be
attained by a monitor that defines an _infinite number of branches_ ; this is
problematic since monitors are required to be _finitely_ described. As it is
not always possible to find a finite monitor that enforces a formula using the
least amount of transformation for every possible system, this indicates that
Figure 7 is too strict. We thus mitigate this issue by weakening Figure 7 and
redefine it in terms of the set of system states $\textsc{Sys}_{\Pi}$, i.e.,
the set of states that can only perform inputs using the ports specified in a
finite $\Pi{\,\subset\,}\textsc{Port}$. Although this weaker version does
_not_ guarantee that the monitor $m$ optimally enforces $\varphi$ on _all_
possible systems, it, however, ensures optimal enforcement for all the systems
that input values via the ports specified in $\Pi$.

[Weak Optimal Enforcement] A monitor $m$ is _weakly optimal_ when enforcing
$\varphi$, denoted as $\textsf{oenf}(m,\varphi,\Pi)$, iff it _enforces_
$\varphi$ (3) and when for every state $s{\,\in\,}\textsc{Sys}_{\Pi}$,
explicit trace $t_{\tau}$ and monitor $n$, if
$\textsl{ec}(n){\,\subseteq\,}\textsl{ec}(m)$, $\textsf{enf}(n,\varphi)$ and
$s\xrightarrow{\;t_{\tau}\;}$ then
$\textsl{mc}(m,t_{\tau}){\,\leq\,}\textsl{mc}(n,t_{\tau})$. ∎

Monitor $m_{1}$ from Figure 7 ensures that $\varphi_{2}$ is optimally enforced
on systems that interact on ports a and b, i.e., when
$\Pi{\,=\,}\\{\textsf{a},\textsf{b}\\}$, while monitor $m_{2}$ guarantees it
when $\Pi{\,=\,}\\{\textsf{a},\textsf{b},\textsf{c}\\}$. $\hfill\blacksquare$

We can show that a synthesised monitor
${\llparenthesis\,\varphi,\Pi\,\rrparenthesis}$ obtained using the synthesis
function Section 5 from Section 5 is also guaranteed to be optimal (as stated
by Figure 7) when enforcing $\varphi$ on a SuS $s$ whose input ports are
specified by $\Pi$, i.e., $s{\,\in\,}\textsc{Sys}_{\Pi}$. Since our synthesis
produces only action disabling monitors, i.e.,
$\textsl{ec}({\llparenthesis\,\varphi,\Pi\,\rrparenthesis}){\,=\,}\\{\textsf{DIS}\\}$
for all $\varphi$ and $\Pi$, we can limit ourselves to monitors pertaining to
the set
$\textsc{DisTrn}{\,\overset{\leavevmode\resizebox{6.0pt}{}{\,{def}}\,}{=}\,}\\!\left\\{\begin{array}[]{rcl}\begin{array}[]{c}\\!\\!n\end{array}&\vrule&\begin{array}[]{l}\text{if
}\textsl{ec}(n){\,\subseteq\,}\\{\textsf{DIS}\\}\\!\\!\end{array}\end{array}\right\\}$.
The proof for 16 below relies on the following lemmas.

######  Lemma 12.

For every $m{\,\in\,}\textsc{DisTrn}$ and explicit trace $t_{\tau}$, there
exists some $N$ such that $\textsl{mc}(m,t_{\tau}){\,=\,}N$. ∎

######  Lemma 13.

For every action $\alpha$ and monitor $m{\,\in\,}\textsc{DisTrn}$, if it is
the case that $m\xrightarrow{\;{\rm ActaAstron.}\;}m^{\prime}$,
$\textsf{enf}(m,\textstyle\bigwedge_{i\in
I}\mathbf{[}(p_{i},c_{i})\mathbf{]}\varphi_{i})$ and
$(p_{j},c_{j})(\alpha){\,=\,}\sigma$ (for some $j{\in}I$) then
$\textsf{enf}(m^{\prime},\varphi_{j}\sigma)$. ∎

######  Lemma 14.

For every monitor $m{\,\in\,}\textsc{DisTrn}$, whenever
$\textsf{enf}(m,\textstyle\bigwedge_{i\in
I}\mathbf{[}(p_{i},c_{i})\mathbf{]}\varphi_{i})$ and, for some $m^{\prime}$,
$m\xrightarrow{\;(\textsf{a}!v){\scriptscriptstyle\blacktriangleright}\bullet\;}m^{\prime}$
then $\textsf{enf}(m^{\prime},\textstyle\bigwedge_{i\in
I}\mathbf{[}(p_{i},c_{i})\mathbf{]}\varphi_{i})$. ∎

######  Lemma 15.

For every monitor $m{\,\in\,}\textsc{DisTrn}$, whenever
$\textsf{enf}(m,\textstyle\bigwedge_{i\in
I}\mathbf{[}(p_{i},c_{i})\mathbf{]}\varphi_{i})$ and, for some $m^{\prime}$,
$m\xrightarrow{\;\bullet{\scriptscriptstyle\blacktriangleright}(\textsf{a}?v)\;}m^{\prime}$
then $\textsf{enf}(m^{\prime},\textstyle\bigwedge_{i\in
I}\mathbf{[}(p_{i},c_{i})\mathbf{]}\varphi_{i})$. ∎

######  Theorem 16 (Weak Optimal Enforcement).

For every system $s{\,\in\,}\textsc{Sys}_{\Pi}$, explicit trace $t_{\tau}$ and
monitor $m$, if
$\textsl{ec}(m){\,\subseteq\,}\textsl{ec}({\llparenthesis\,\varphi,\Pi\,\rrparenthesis})$,
$\textsf{enf}(m,\varphi)$ and $s\xrightarrow{\;t_{\tau}\;}$ implies
$\textsl{mc}({\llparenthesis\,\varphi,\Pi\,\rrparenthesis},t_{\tau}){\,\leq\,}\textsl{mc}(m,t_{\tau})$.

######  Proof 6.1.

Since, from 12, we know that for every $m{\,\in\,}\textsc{DisTrn}$, there
exists some $N$ such that $\textsl{mc}(m,t_{\tau}){\,=\,}N$, we can prove that
if $\textsf{enf}(m,\varphi)$, $s{\xrightarrow{\;t_{\tau}\;}}$ and
$\textsl{mc}({\llparenthesis\,\varphi,\Pi\,\rrparenthesis},t_{\tau}){\,=\,}N$
then $N{\,\leq\,}\textsl{mc}(m,t_{\tau})$. We proceed by rule induction on
$\textsl{mc}({\llparenthesis\,\varphi,\Pi\,\rrparenthesis},t_{\tau})$.

_Case
$\textsl{mc}({\llparenthesis\,\varphi,\Pi\,\rrparenthesis},t_{\tau})\emph{
when }t_{\tau}{\,=\,}\mu t_{\tau}^{\prime}\emph{ and
}{\llparenthesis\,\varphi,\Pi\,\rrparenthesis}[\textsf{sys}(\mu
t_{\tau}^{\prime})]\xrightarrow{\;\mu\;}m^{\prime}_{\varphi}[\textsf{sys}(t_{\tau}^{\prime})]$._
Assume that

$\displaystyle\textsl{mc}({\llparenthesis\,\varphi,\Pi\,\rrparenthesis},\mu
t_{\tau}^{\prime})=\textsl{mc}(m^{\prime}_{\varphi},t_{\tau}^{\prime})=N$
(109)

which implies that

$\displaystyle{\llparenthesis\,\varphi,\Pi\,\rrparenthesis}[\textsf{sys}(\mu
t_{\tau}^{\prime})]\xrightarrow{\;\mu\;}m^{\prime}_{\varphi}[\textsf{sys}(t_{\tau}^{\prime})]$
(110)

and also assume that

$\displaystyle\textsf{enf}(m,\varphi)$ (111)

and that $s\xrightarrow{\;\mu t_{\tau}^{\prime}\;}$. By the rules in our model
we can infer that the reduction in (110) can result from rule iAsy when
$\mu{\,=\,}\tau$, iDef and iTrnO when $\mu{\,=\,}\textsf{a}!v$, or iTrnI when
$\mu{\,=\,}\textsf{a}?v$. We consider each case individually.

  * •

iAsy: By rule iAsy from (110) we know that $\mu{\,=\,}\tau$ and that

$\displaystyle
m^{\prime}_{\varphi}={\llparenthesis\,\varphi,\Pi\,\rrparenthesis}.$ (112)

Since from (111) we know that $m$ is sound and eventual transparent, we can
thus deduce that $m$ does not hinder internal $\tau$-actions from occurring
and so the composite system
${\llparenthesis\,\varphi,\Pi\,\rrparenthesis}[\textsf{sys}(\tau
t_{\tau}^{\prime})]$ can always transition over $\tau$ via rule iAsy, that is,

$\displaystyle m[\textsf{sys}(\tau
t_{\tau}^{\prime})]\xrightarrow{\;\tau\;}m[\textsf{sys}(t_{\tau}^{\prime})].$
(113)

Hence, by (109), (111) and since $s\xrightarrow{\;\tau t_{\tau}^{\prime}\;}$
entails $s\xrightarrow{\;\tau\;}s^{\prime}$ and
$s^{\prime}\xrightarrow{\;t_{\tau}^{\prime}\;}$ we can apply the _inductive
hypothesis_ and deduce that $N{\,\leq\,}\textsl{mc}(m,t_{\tau}^{\prime})$ so
that by (113) and the definition of mc, we conclude that
$N{\,\leq\,}\textsl{mc}(m,\tau t_{\tau}^{\prime})$ as required.

  * •

iDef: From (110) and rule iDef we know that $\mu{\,=\,}\textsf{a}!v$,
${\llparenthesis\,\varphi,\Pi\,\rrparenthesis}\mathchoice{\mathrel{\hbox
to0.0pt{\kern
11.76962pt\kern-5.27776pt$\displaystyle\not$\hss}{\xrightarrow{\;\textsf{a}!v\;}}}}{\mathrel{\hbox
to0.0pt{\kern
11.76962pt\kern-5.27776pt$\textstyle\not$\hss}{\xrightarrow{\;\textsf{a}!v\;}}}}{\mathrel{\hbox
to0.0pt{\kern
9.07204pt\kern-4.11108pt$\scriptstyle\not$\hss}{\xrightarrow{\;\textsf{a}!v\;}}}}{\mathrel{\hbox
to0.0pt{\kern
7.27365pt\kern-3.3333pt$\scriptscriptstyle\not$\hss}{\xrightarrow{\;\textsf{a}!v\;}}}}$
and that $m^{\prime}_{\varphi}=\textsf{id}$. Since id does not modify actions,
we can deduce that
$\textsl{mc}(m_{\varphi}^{\prime},t_{\tau}^{\prime}){\,=\,}0$ and so by the
definition of mc we know that
$\textsl{mc}({\llparenthesis\,\varphi,\Pi\,\rrparenthesis},(\textsf{a}!v)t_{\tau}^{\prime}){\,=\,}0$
as well. This means that we cannot find a monitor that performs fewer
transformations, and so we conclude that
$0{\,\leq\,}\textsl{mc}(m,(\textsf{a}!v)t_{\tau}^{\prime})$ as required.

  * •

iTrnI: From (110) and rule iTrnI we know that $\mu{\,=\,}\textsf{a}?v$ and
that

$\displaystyle{\llparenthesis\,\varphi,\Pi\,\rrparenthesis}\xrightarrow{\;(\textsf{a}?v){\scriptscriptstyle\blacktriangleright}(\textsf{a}?v)\;}m^{\prime}_{\varphi}.$
(114)

We now inspect the cases for $\varphi$.

    * –

$\varphi{\,\in\,}\\{\mathsf{ff},\mathsf{tt},X\\}$: The cases for $\mathsf{ff}$
and $X$ do not apply since ${\llparenthesis\,\mathsf{ff},\Pi\,\rrparenthesis}$
and ${\llparenthesis\,X,\Pi\,\rrparenthesis}$ do not yield a valid monitor,
while the case when $\varphi{\,=\,}\mathsf{tt}$ gets trivially satisfied since
${\llparenthesis\,\mathsf{tt},\Pi\,\rrparenthesis}{\,=\,}\textsf{id}$ and
$\textsl{mc}(\textsf{id},(\textsf{a}?v)t_{\tau}^{\prime}){\,=\,}0$.

    * –

$\varphi{\,=\,}\textstyle\bigwedge_{i\in
I}\mathbf{[}(p_{i},c_{i})\mathbf{]}\varphi_{i}$ where $\\#_{i\in
I}(p_{i},c_{i})$: Since $\varphi=\textstyle\bigwedge_{i\in
I}\mathbf{[}(p_{i},c_{i})\mathbf{]}\varphi_{i}$, by the definition of
${\llparenthesis\,-\,\rrparenthesis}$ we have that

$\displaystyle\begin{array}[]{@{\hspace{-1mm}}r@{\hspace{-40mm}}cl}{\llparenthesis\,\varphi_{\mathbf{\wedge}}=\textstyle\bigwedge_{i\in
I}\mathbf{[}(p_{i},c_{i})\mathbf{]}\varphi_{i},\Pi\,\rrparenthesis\\\
&=&\textsf{rec}\,Y.\left(\\!\begin{array}[]{c}\raisebox{0.86108pt}{\scalebox{0.8}{$\displaystyle\sum_{i\in
I}$}}\left\\{\begin{array}[]{lc}\textsf{dis}(p_{i},c_{i},Y,\Pi)&\emph{ if
}\varphi_{i}=\mathsf{ff}\\\
(p_{i},c_{i}).{{\llparenthesis\,\varphi_{i},\Pi\,\rrparenthesis}}&\emph{
otherwise
}\end{array}\right.\end{array}\right)+\textsf{def}(\raisebox{0.86108pt}{\scalebox{0.8}{$\displaystyle\bigwedge_{i\in
I}\,$}}\mathbf{[}(p_{i},c_{i})\mathbf{]}\varphi_{i})\\\
&=&{\left(\\!\begin{array}[]{c}\raisebox{0.86108pt}{\scalebox{0.8}{$\displaystyle\sum_{i\in
I}$}}\left\\{\begin{array}[]{lc}\textsf{dis}(p_{i},c_{i},{\llparenthesis\,\varphi_{\mathbf{\wedge}},\Pi\,\rrparenthesis},\Pi)&\emph{
if }\varphi_{i}=\mathsf{ff}\\\
(p_{i},c_{i}).{{\llparenthesis\,\varphi_{i},\Pi\,\rrparenthesis}}&\emph{
otherwise
}\end{array}\right.\end{array}\right)+\textsf{def}(\raisebox{0.86108pt}{\scalebox{0.8}{$\displaystyle\bigwedge_{i\in
I}\,$}}\mathbf{[}(p_{i},c_{i})\mathbf{]}\varphi_{i})}\end{array}}$ (124)

Since normalized conjunctions are disjoint, i.e., $\\#_{i\in I}(p_{i},c_{i})$,
from (124) we can infer that the identity reduction in (114) can only happen
when $\textsf{a}?v$ matches an identity branch,
$(p_{j},c_{j}).{{\llparenthesis\,\varphi_{j},\Pi\,\rrparenthesis}}$ (for some
$j{\,\in\,}I$), and so we have that

$\displaystyle(p_{j},c_{j})(\textsf{a}?v)=\sigma.$ (125)

Hence, knowing (114) and (125), by rule eTrn we know that
$m^{\prime}_{\varphi}{\,=\,}{\llparenthesis\,\varphi_{j}\sigma,\Pi\,\rrparenthesis}$
and so by (109) we can infer that

$\displaystyle\textsl{mc}(m^{\prime}_{\varphi},t_{\tau}^{\prime})=N\;\emph{
where
}m^{\prime}_{\varphi}{\,=\,}{\llparenthesis\,\varphi_{j}\sigma,\Pi\,\rrparenthesis}.$
(126)

Since from (124) we also know that the monitor branch
$(p_{j},c_{j}).{{\llparenthesis\,\varphi_{j},\Pi\,\rrparenthesis}}$ is derived
from a non-violating modal necessity, i.e.,
$\mathbf{[}(p_{j},c_{j})\mathbf{]}\varphi_{j}$ where
$\varphi_{j}{\,\neq\,}\mathsf{ff}$, we can infer that $\textsf{a}?v$ is not a
violating action and so it should not be modified by any other monitor $m$, as
otherwise it would infringe the eventual transparency constraint of assumption
(111). Therefore, we can deduce that

$\displaystyle
m\xrightarrow{\;(\textsf{a}?v){\scriptscriptstyle\blacktriangleright}(\textsf{a}?v)\;}m^{\prime}\quad(\text{for
some }m^{\prime})$ (127)

and subsequently, knowing (127) and that
$t_{\tau}{\,=\,}(\textsf{a}?v)t_{\tau}^{\prime}$ and also that
$\textsf{sys}((\textsf{a}?v)t_{\tau}^{\prime}){\xrightarrow{\;\textsf{a}?v\;}}\textsf{sys}(t_{\tau}^{\prime})$,
by rule iTrnI and the definition of mc we infer that

$\displaystyle\textsl{mc}(m,(\textsf{a}?v)t_{\tau}^{\prime})=\textsl{mc}(m^{\prime},t_{\tau}^{\prime}).$
(128)

As by (111), (114), (125) and 13 we know that
$\textsf{enf}(m^{\prime},\varphi_{j}\sigma)$, by (126) and since
$s\xrightarrow{\;(\textsf{a}?v)t_{\tau}^{\prime}\;}$ entails that
$s\xrightarrow{\;\textsf{a}?v\;}s^{\prime}$ and
$s^{\prime}\xrightarrow{\;t_{\tau}^{\prime}\;}$, we can apply the _inductive
hypothesis_ and deduce that
$N{\,\leq\,}\textsl{mc}(m^{\prime},t_{\tau}^{\prime})$ and so from (128) we
conclude that $N{\,\leq\,}\textsl{mc}(m,(\textsf{a}?v)t_{\tau}^{\prime})$ as
required.

    * –

$\varphi{\,=\,}\mathsf{max}\,X.\varphi^{\prime}$ and
$X{\,\in\,}\textbf{fv}(\varphi^{\prime})$: Since
$\varphi{\,=\,}\mathsf{max}\,X.\varphi^{\prime}$, by the syntactic
restrictions of $\textsc{sHML}_{\textbf{nf}}$ we infer that $\varphi^{\prime}$
cannot be $\mathsf{ff}$ or $\mathsf{tt}$ since
$X{\,\notin\,}\textbf{fv}(\varphi^{\prime})$ otherwise, and it cannot be $X$
since every logical variable must be guarded. Hence, $\varphi^{\prime}$ must
be of a specific form, i.e., $\mathsf{max}\,Y_{1}\ldots
Y_{n}.\textstyle\bigwedge_{i\in
I}\mathbf{[}(p_{i},c_{i})\mathbf{]}\varphi_{i}$, and so by unfolding every
fixpoint in $\mathsf{max}\,X.\varphi^{\prime}$ we reduce our formula to
$\varphi\,\overset{\leavevmode\resizebox{6.0pt}{}{\,{def}}\,}{=}\,\textstyle\bigwedge_{i\in
I}\mathbf{[}(p_{i},c_{i})\mathbf{]}\varphi_{i}\\{^{\mathsf{max}\,X.\varphi^{\prime}}{\\!/}_{X},\ldots\\}$.
We thus omit the remainder of this proof as it becomes identical to that of
the subcase when
$\varphi{\,=\,}\raisebox{0.86108pt}{\scalebox{0.8}{$\displaystyle\bigwedge_{i\in
I}\,$}}\mathbf{[}(p_{i},c_{i})\mathbf{]}\varphi_{i}$.

  * •

iTrnO: We elide the proof for this case as it is very similar to that of
iTrnI.

_Case
$\textsl{mc}({\llparenthesis\,\varphi,\Pi\,\rrparenthesis},t_{\tau})\emph{
when }t_{\tau}{=}\mu t_{\tau}^{\prime}\emph{ and
}{\llparenthesis\,\varphi,\Pi\,\rrparenthesis}[\textsf{sys}(\mu
t_{\tau}^{\prime})]{\xrightarrow{\;\mu^{\prime}\;}}m^{\prime}_{\varphi}[\textsf{sys}(t_{\tau}^{\prime})]\emph{
and }\mu^{\prime}{\neq}\mu$._
Assume that

$\displaystyle\textsl{mc}({\llparenthesis\,\varphi,\Pi\,\rrparenthesis},\mu
t_{\tau}^{\prime})=1+M$ (129) $\displaystyle\emph{ where
}M=\textsl{mc}(m^{\prime}_{\varphi},t_{\tau}^{\prime})$ (130)

which implies that

$\displaystyle{\llparenthesis\,\varphi,\Pi\,\rrparenthesis}[\textsf{sys}(\mu
t_{\tau}^{\prime})]\xrightarrow{\;\mu^{\prime}\;}m^{\prime}_{\varphi}[\textsf{sys}(t_{\tau}^{\prime})]\;\emph{
where }\mu^{\prime}\neq\mu$ (131)

and also assume that

$\displaystyle\textsf{enf}(m,\varphi)$ (132)

and that $s\xrightarrow{\;\mu t_{\tau}^{\prime}\;}$. Since we only consider
action disabling monitors, the $\mu^{\prime}$ reduction of (131) can only be
achieved via rules iDisO or iDisI. We thus explore both cases.

  * •

iDisI: From (131) and by rule iDisI we have that $\mu=\textsf{a}?v$ and
$\mu^{\prime}=\tau$ and that

$\displaystyle{\llparenthesis\,\varphi,\Pi\,\rrparenthesis}\xrightarrow{\;\bullet{\scriptscriptstyle\blacktriangleright}\textsf{a}?v\;}m^{\prime}_{\varphi}.$
(133)

We now inspect the cases for $\varphi$.

    * –

$\varphi{\,\in\,}\\{\mathsf{ff},\mathsf{tt},X\\}$: These cases do not apply
since ${\llparenthesis\,\mathsf{ff},\Pi\,\rrparenthesis}$ and
${\llparenthesis\,X,\Pi\,\rrparenthesis}$ do not yield a valid monitor, while
${\llparenthesis\,\mathsf{tt},\Pi\,\rrparenthesis}{\,=\,}\textsf{id}$ does not
perform the reduction in (133).

    * –

$\varphi{\,=\,}\textstyle\bigwedge_{i\in
I}\mathbf{[}(p_{i},c_{i})\mathbf{]}\varphi_{i}$ where $\\#_{i\in
I}(p_{i},c_{i})$: Since $\varphi=\textstyle\bigwedge_{i\in
I}\mathbf{[}(p_{i},c_{i})\mathbf{]}\varphi_{i}$, by the definition of
${\llparenthesis\,-\,\rrparenthesis}$ we have that

$\displaystyle\begin{array}[]{@{\hspace{-1mm}}r@{\hspace{-40mm}}cl}{\llparenthesis\,\varphi_{\mathbf{\wedge}}=\textstyle\bigwedge_{i\in
I}\mathbf{[}(p_{i},c_{i})\mathbf{]}\varphi_{i},\Pi\,\rrparenthesis\\\
&=&\textsf{rec}\,Y.\left(\\!\begin{array}[]{c}\raisebox{0.86108pt}{\scalebox{0.8}{$\displaystyle\sum_{i\in
I}$}}\left\\{\begin{array}[]{lc}\textsf{dis}(p_{i},c_{i},Y,\Pi)&\emph{ if
}\varphi_{i}=\mathsf{ff}\\\
(p_{i},c_{i}).{{\llparenthesis\,\varphi_{i},\Pi\,\rrparenthesis}}&\emph{
otherwise
}\end{array}\right.\end{array}\right)+\textsf{def}(\raisebox{0.86108pt}{\scalebox{0.8}{$\displaystyle\bigwedge_{i\in
I}\,$}}\mathbf{[}(p_{i},c_{i})\mathbf{]}\varphi_{i})\\\
&=&{\left(\\!\begin{array}[]{c}\raisebox{0.86108pt}{\scalebox{0.8}{$\displaystyle\sum_{i\in
I}$}}\left\\{\begin{array}[]{lc}\textsf{dis}(p_{i},c_{i},{\llparenthesis\,\varphi_{\mathbf{\wedge}},\Pi\,\rrparenthesis},\Pi)&\emph{
if }\varphi_{i}=\mathsf{ff}\\\
(p_{i},c_{i}).{{\llparenthesis\,\varphi_{i},\Pi\,\rrparenthesis}}&\emph{
otherwise
}\end{array}\right.\end{array}\right)+\textsf{def}(\raisebox{0.86108pt}{\scalebox{0.8}{$\displaystyle\bigwedge_{i\in
I}\,$}}\mathbf{[}(p_{i},c_{i})\mathbf{]}\varphi_{i})}\end{array}}$ (143)

Since normalized conjunctions are disjoint i.e., $\\#_{i\in I}(p_{i},c_{i})$,
and since $s\xrightarrow{\;\mu t_{\tau}^{\prime}\;}$ where
$\mu=(\textsf{a}?v)$, by the definition of dis, from (143) we deduce that the
reduction in (133) can only be performed by an insertion branch of the form,
$(\bullet,c_{j}\\{{\textsf{a}}/{x}\\},\textsf{a}?v).{{\llparenthesis\,\textstyle\bigwedge_{i\in
I}\mathbf{[}(p_{i},c_{i})\mathbf{]}\varphi_{i},\Pi\,\rrparenthesis}}$ that can
only be derived from a violating modal necessity
$\mathbf{[}(p_{j},c_{j})\mathbf{]}\mathsf{ff}$ (for some $j{\,\in\,}I$).
Hence, we can infer that

$\displaystyle m^{\prime}_{\varphi}={\llparenthesis\,\textstyle\bigwedge_{i\in
I}\mathbf{[}(p_{i},c_{i})\mathbf{]}\varphi_{i},\Pi\,\rrparenthesis}$ (144)
$\displaystyle p_{j}=(x)?(y)\emph{ and
}c_{j}\\{{\textsf{a}}/{x}\\}\Downarrow\textsf{true}.$ (145)

Knowing (145) and that $\mathbf{[}(p_{j},c_{j})\mathbf{]}\mathsf{ff}$ we can
deduce that any input on port a is erroneous and so for the soundness
constraint of assumption (132) to hold, any other monitor $m$ is obliged to
somehow _block_ this input port. As we consider action disabling monitors,
i.e., $m{\,\in\,}\textsc{DisTrn}$, we can infer that monitor $m$ may block
this input in two ways, namely, either by not reacting to the input action,
i.e., $m\mathchoice{\mathrel{\hbox to0.0pt{\kern
12.74184pt\kern-5.27776pt$\displaystyle\not$\hss}{\xrightarrow{\;\textsf{a}?v\;}}}}{\mathrel{\hbox
to0.0pt{\kern
12.74184pt\kern-5.27776pt$\textstyle\not$\hss}{\xrightarrow{\;\textsf{a}?v\;}}}}{\mathrel{\hbox
to0.0pt{\kern
9.7526pt\kern-4.11108pt$\scriptstyle\not$\hss}{\xrightarrow{\;\textsf{a}?v\;}}}}{\mathrel{\hbox
to0.0pt{\kern
7.75977pt\kern-3.3333pt$\scriptscriptstyle\not$\hss}{\xrightarrow{\;\textsf{a}?v\;}}}}$,
or by additionally inserting a default value $v$, i.e.,
$m\xrightarrow{\;\bullet{\scriptscriptstyle\blacktriangleright}(\textsf{a}?v)\;}m^{\prime}$.
We explore both cases.

      * *

$m\mathchoice{\mathrel{\hbox to0.0pt{\kern
12.74184pt\kern-5.27776pt$\displaystyle\not$\hss}{\xrightarrow{\;\textsf{a}?v\;}}}}{\mathrel{\hbox
to0.0pt{\kern
12.74184pt\kern-5.27776pt$\textstyle\not$\hss}{\xrightarrow{\;\textsf{a}?v\;}}}}{\mathrel{\hbox
to0.0pt{\kern
9.7526pt\kern-4.11108pt$\scriptstyle\not$\hss}{\xrightarrow{\;\textsf{a}?v\;}}}}{\mathrel{\hbox
to0.0pt{\kern
7.75977pt\kern-3.3333pt$\scriptscriptstyle\not$\hss}{\xrightarrow{\;\textsf{a}?v\;}}}}$:
Since
$\textsf{sys}((\textsf{a}?v)t_{\tau}^{\prime})\xrightarrow{\;\textsf{a}?v\;}\textsf{sys}(t_{\tau}^{\prime})$
and since $m\mathchoice{\mathrel{\hbox to0.0pt{\kern
12.74184pt\kern-5.27776pt$\displaystyle\not$\hss}{\xrightarrow{\;\textsf{a}?v\;}}}}{\mathrel{\hbox
to0.0pt{\kern
12.74184pt\kern-5.27776pt$\textstyle\not$\hss}{\xrightarrow{\;\textsf{a}?v\;}}}}{\mathrel{\hbox
to0.0pt{\kern
9.7526pt\kern-4.11108pt$\scriptstyle\not$\hss}{\xrightarrow{\;\textsf{a}?v\;}}}}{\mathrel{\hbox
to0.0pt{\kern
7.75977pt\kern-3.3333pt$\scriptscriptstyle\not$\hss}{\xrightarrow{\;\textsf{a}?v\;}}}}$,
by the rules in our model we know that for every action $\mu^{\prime}$,
$m[\textsf{sys}((\textsf{a}?v)t_{\tau}^{\prime})]{\mathchoice{\mathrel{\hbox
to0.0pt{\kern
9.06046pt\kern-5.27776pt$\displaystyle\not$\hss}{\xrightarrow{\;\mu^{\prime}\;}}}}{\mathrel{\hbox
to0.0pt{\kern
9.06046pt\kern-5.27776pt$\textstyle\not$\hss}{\xrightarrow{\;\mu^{\prime}\;}}}}{\mathrel{\hbox
to0.0pt{\kern
7.18661pt\kern-4.11108pt$\scriptstyle\not$\hss}{\xrightarrow{\;\mu^{\prime}\;}}}}{\mathrel{\hbox
to0.0pt{\kern
6.08408pt\kern-3.3333pt$\scriptscriptstyle\not$\hss}{\xrightarrow{\;\mu^{\prime}\;}}}}}$
and so by the definition of mc we have that
$\textsl{mc}(m,(\textsf{a}?v)t_{\tau}^{\prime}){\,=\,}|{\,(\textsf{a}?v)t_{\tau}^{\prime}\,}|$
meaning that by blocking inputs on a, $m$ also blocks (and thus modifies)
every subsequent action of trace $t_{\tau}^{\prime}$. Hence, this suffices to
deduce that _at worst_ $1+M$ is equal to
$|{\,(\textsf{a}?v)t_{\tau}^{\prime}\,}|$, that is
$1+M{\,\leq\,}|{\,(\textsf{a}?v)t_{\tau}^{\prime}\,}|$, and so from (129) we
can deduce that
$1+M{\,\leq\,}\textsl{mc}({\llparenthesis\,\varphi,\Pi\,\rrparenthesis},\mu
t_{\tau}^{\prime})$ as required.

      * *

$m\xrightarrow{\;\bullet{\scriptscriptstyle\blacktriangleright}(\textsf{a}?v)\;}m^{\prime}$:
Since
$\textsf{sys}((\textsf{a}?v)t_{\tau}^{\prime})\xrightarrow{\;\textsf{a}?v\;}\textsf{sys}(t_{\tau}^{\prime})$
and since
$m\xrightarrow{\;\bullet{\scriptscriptstyle\blacktriangleright}(\textsf{a}?v)\;}m^{\prime}$,
by rule iDisI we know that
$m[\textsf{sys}((\textsf{a}?v)t_{\tau}^{\prime})]\xrightarrow{\;\tau\;}m[\textsf{sys}(t_{\tau}^{\prime})]$
and so by the definition of mc we have that

$\displaystyle\textsl{mc}(m,(\textsf{a}?v)t_{\tau}^{\prime})=1+\textsl{mc}(m^{\prime},t_{\tau}^{\prime}).$
(146)

As by (132), (133) and 15 we infer that
$\textsf{enf}(m^{\prime},\textstyle\bigwedge_{i\in
I}\mathbf{[}(p_{i},c_{i})\mathbf{]}\varphi_{i})$, by (130), (146) and since
$s{\,\xrightarrow{\;(\textsf{a}?v)t_{\tau}^{\prime}\;}}$ entails that
$s{\,\xrightarrow{\;(\textsf{a}?v)\;}\,}s^{\prime}$ and
$s^{\prime}{\,\xrightarrow{\;t_{\tau}^{\prime}\;}}$, we can apply the
_inductive hypothesis_ and deduce that
$M{\,\leq\,}\textsl{mc}(m^{\prime},t_{\tau}^{\prime})$ and so from (129),
(130) and (146) we conclude that
$1+M{\,\leq\,}\textsl{mc}(m,(\textsf{a}?v)t_{\tau}^{\prime})$ as required.

    * –

$\varphi{\,=\,}\mathsf{max}\,X.\varphi^{\prime}$ and
$X{\,\in\,}\textbf{fv}(\varphi^{\prime})$: We omit showing this proof as it is
a special case of when $\varphi{\,=\,}\textstyle\bigwedge_{i\in
I}\mathbf{[}(p_{i},c_{i})\mathbf{]}\varphi_{i}$.

  * •

iDisO: We omit showing the proof for this subcase as it is very similar to
that of case iDisI. Apart from the obvious differences (e.g., $\textsf{a}!v$
instead of $\textsf{a}?v$), 14 is used instead of 15.

_Case
$\textsl{mc}({\llparenthesis\,\varphi,\Pi\,\rrparenthesis},t_{\tau})\emph{
when }t_{\tau}{\,\in\,}\\{\mu t_{\tau}^{\prime},\varepsilon\\}\emph{ and
}{\llparenthesis\,\varphi,\Pi\,\rrparenthesis}[\textsf{sys}(\mu
t_{\tau}^{\prime})]\mathchoice{\mathrel{\hbox to0.0pt{\kern
9.06046pt\kern-5.27776pt$\displaystyle\not$\hss}{\xrightarrow{\;\mu^{\prime}\;}}}}{\mathrel{\hbox
to0.0pt{\kern
9.06046pt\kern-5.27776pt$\textstyle\not$\hss}{\xrightarrow{\;\mu^{\prime}\;}}}}{\mathrel{\hbox
to0.0pt{\kern
7.18661pt\kern-4.11108pt$\scriptstyle\not$\hss}{\xrightarrow{\;\mu^{\prime}\;}}}}{\mathrel{\hbox
to0.0pt{\kern
6.08408pt\kern-3.3333pt$\scriptscriptstyle\not$\hss}{\xrightarrow{\;\mu^{\prime}\;}}}}$._
Assume that

$\displaystyle\textsl{mc}({\llparenthesis\,\varphi,\Pi\,\rrparenthesis},t_{\tau})=|{\,t_{\tau}\,}|\quad(\text{where
}t_{\tau}{\,\in\,}\\{\mu t_{\tau}^{\prime},\varepsilon\\})$ (147)
$\displaystyle{\llparenthesis\,\varphi,\Pi\,\rrparenthesis}[\textsf{sys}(\mu
t_{\tau}^{\prime})]\mathchoice{\mathrel{\hbox to0.0pt{\kern
9.06046pt\kern-5.27776pt$\displaystyle\not$\hss}{\xrightarrow{\;\mu^{\prime}\;}}}}{\mathrel{\hbox
to0.0pt{\kern
9.06046pt\kern-5.27776pt$\textstyle\not$\hss}{\xrightarrow{\;\mu^{\prime}\;}}}}{\mathrel{\hbox
to0.0pt{\kern
7.18661pt\kern-4.11108pt$\scriptstyle\not$\hss}{\xrightarrow{\;\mu^{\prime}\;}}}}{\mathrel{\hbox
to0.0pt{\kern
6.08408pt\kern-3.3333pt$\scriptscriptstyle\not$\hss}{\xrightarrow{\;\mu^{\prime}\;}}}}$
(148) $\displaystyle\textsf{enf}(m,\varphi)$ (149)

Since $t_{\tau}{\,\in\,}\\{\mu t_{\tau}^{\prime},\varepsilon\\}$ we consider
both cases individually.

  * •

$t_{\tau}=\varepsilon:$ This case holds trivially since by (147), (148) and
the definition of mc,
$\textsl{mc}({\llparenthesis\,\varphi,\Pi\,\rrparenthesis},\varepsilon)=|{\,\varepsilon\,}|=0$.

  * •

$t_{\tau}=\mu t_{\tau}^{\prime}:$ Since $t_{\tau}=\mu t_{\tau}^{\prime}$ we
can immediately exclude the cases when $\mu{\,\in\,}\\{\tau,\textsf{a}!v\\}$
since rules iAsy and iDef make it impossible for (148) to be attained in such
cases. Particularly, rule iAsy always permits the SuS to independently perform
an internal $\tau$-move, while rule iDef allows the monitor to default to id
whenever the system performs an unspecified output $\textsf{a}!v$. However, in
the case of inputs, $\textsf{a}?v$, the monitor may completely block inputs on
a port a and as a consequence cause the entire composite system
${\llparenthesis\,\varphi,\Pi\,\rrparenthesis}[\textsf{sys}(\mu
t_{\tau}^{\prime})]$ to block, thereby making (148) a possible scenario. We
thus inspect the cases for $\varphi$ vis-a-vis $\mu{\,=\,}\textsf{a}?v$.

    * –

$\varphi{\,\in\,}\\{\mathsf{ff},\mathsf{tt},X\\}$: These cases do not apply
since ${\llparenthesis\,\mathsf{ff},\Pi\,\rrparenthesis}$ and
${\llparenthesis\,X,\Pi\,\rrparenthesis}$ do not yield a valid monitor and
since ${\llparenthesis\,\mathsf{tt},\Pi\,\rrparenthesis}{\,=\,}\textsf{id}$ is
incapable of attaining (148).

    * –

$\varphi{\,=\,}\raisebox{0.86108pt}{\scalebox{0.8}{$\displaystyle\bigwedge_{i\in
I}\,$}}\mathbf{[}(p_{i},c_{i})\mathbf{]}\varphi_{i}$ where $\\#_{i\in
I}(p_{i},c_{i})$: Since
$\varphi{\,=\,}\raisebox{0.86108pt}{\scalebox{0.8}{$\displaystyle\bigwedge_{i\in
I}\,$}}\mathbf{[}(p_{i},c_{i})\mathbf{]}\varphi_{i}$, by the definition of
${\llparenthesis\,-\,\rrparenthesis}$ we have that

$\displaystyle\begin{array}[]{@{\hspace{-1mm}}r@{\hspace{-40mm}}cl}{\llparenthesis\,\varphi_{\mathbf{\wedge}}=\textstyle\bigwedge_{i\in
I}\mathbf{[}(p_{i},c_{i})\mathbf{]}\varphi_{i},\Pi\,\rrparenthesis\\\
&=&\textsf{rec}\,Y.\left(\\!\begin{array}[]{c}\raisebox{0.86108pt}{\scalebox{0.8}{$\displaystyle\sum_{i\in
I}$}}\left\\{\begin{array}[]{lc}\textsf{dis}(p_{i},c_{i},Y,\Pi)&\emph{ if
}\varphi_{i}=\mathsf{ff}\\\
(p_{i},c_{i}).{{\llparenthesis\,\varphi_{i},\Pi\,\rrparenthesis}}&\emph{
otherwise
}\end{array}\right.\end{array}\right)+\textsf{def}(\raisebox{0.86108pt}{\scalebox{0.8}{$\displaystyle\bigwedge_{i\in
I}\,$}}\mathbf{[}(p_{i},c_{i})\mathbf{]}\varphi_{i})\\\
&=&{\left(\\!\begin{array}[]{c}\raisebox{0.86108pt}{\scalebox{0.8}{$\displaystyle\sum_{i\in
I}$}}\left\\{\begin{array}[]{lc}\textsf{dis}(p_{i},c_{i},{\llparenthesis\,\varphi_{\mathbf{\wedge}},\Pi\,\rrparenthesis},\Pi)&\emph{
if }\varphi_{i}=\mathsf{ff}\\\
(p_{i},c_{i}).{{\llparenthesis\,\varphi_{i},\Pi\,\rrparenthesis}}&\emph{
otherwise
}\end{array}\right.\end{array}\right)+\textsf{def}(\raisebox{0.86108pt}{\scalebox{0.8}{$\displaystyle\bigwedge_{i\in
I}\,$}}\mathbf{[}(p_{i},c_{i})\mathbf{]}\varphi_{i})}\end{array}}$ (159)

Since $\mu=\textsf{a}?v$, from (159) and by the definitions of dis and def we
can infer that the only case when (148) is possible is when the inputs on port
a satisfy a violating modal necessity, that is, there exists some
$j{\,\in\,}I$ such that $\mathbf{[}(p_{j},c_{j})\mathbf{]}\mathsf{ff}$ and for
every $v{\,\in\,}\textsc{Val}$,
$\textsf{match(}p_{j},\textsf{a}?v\textsf{)}{\,=\,}\sigma$ and
$c_{j}\sigma\Downarrow\textsf{true}$. At the same time, the monitor is also
_unaware_ of the port on which the erroneous input can be made, i.e.,
$\textsf{a}{\,\notin\,}\Pi$. Hence, this case does not apply since we limit
ourselves to $\textsc{Sys}_{\Pi}$, i.e., states of system that can only input
values via the ports specified in $\Pi$.

    * –

$\varphi{\,=\,}\mathsf{max}\,X.\varphi^{\prime}$: As argued in previous cases,
this is a special case of $\varphi{\,=\,}\textstyle\bigwedge_{i\in
I}\mathbf{[}(p_{i},c_{i})\mathbf{]}\varphi_{i}$ and so we omit this part of
the proof.

_Case
$\textsl{mc}({\llparenthesis\,\varphi,\Pi\,\rrparenthesis},t_{\tau})\emph{
when }t_{\tau}{\,\in\,}\\{\mu t_{\tau}^{\prime},\varepsilon\\}\emph{ and
}{\llparenthesis\,\varphi,\Pi\,\rrparenthesis}[\textsf{sys}(t_{\tau})]\xrightarrow{\;\mu^{\prime}\;}m^{\prime}_{\varphi}[\textsf{sys}(t_{\tau})]$._
As we only consider action disabling monitors, this case does not apply since
the transition
${\llparenthesis\,\varphi,\Pi\,\rrparenthesis}[\textsf{sys}(t_{\tau})]\xrightarrow{\;\mu^{\prime}\;}m^{\prime}_{\varphi}[\textsf{sys}(t_{\tau})]$
can only be achieved via action enabling and rules iEnO and iEnI.

##  7\. Conclusions and Related Work

This work extends the framework presented in the precursor to this work
[ACFI18] to the setting of bidirectional enforcement where observable actions
such as inputs and outputs require different treatment. We achieve this by:

  1. (1)

augmenting substantially our instrumentation relation (Figure 4);

  2. (2)

refining our definition of enforcement to incorporate transparency over
violating systems (3);

  3. (3)

providing a more extensive synthesis function (Section 5) that is proven
correct (4); and

  4. (4)

exploring notions of transducer optimality in terms of limited levels of
intrusiveness (Figures 7 and 7 and 16).

#### Future work.

There are a number of possible avenues for extending our work. One immediate
step would be the implementation of the monitor operational model presented in
Section 3 together with the synthesis function described in Section 5. This
effort should be integrated it within the detectEr tool suite [CFS15, AF16,
CFAI17, CFA+17, AAA+21]. This would allow us to assess the overhead induced by
our proposed bidirectional monitoring [AAFI21]. Another possible direction
would be the development of behavioural theories for the transducer
operational model presented in Section 3, along the lines of the refinement
preorders studied in earlier work on sequence recognisers [Fra21, Fra17,
AAF+21]. Finally, applications of this theory on transducers, along the lines
of [LMM20] are also worth exploring.

#### Related work.

In his seminal work [Sch00], Schneider introduced the concept of runtime
enforcement and enforceability in a linear-time setting. Particularly, in his
setting a property is deemed enforceable if its _violation_ can be _detected_
by a _truncation automaton_ , and prevented via system termination. By
preventing misbehaviour, these automata can only enforce safety properties.
Ligatti et al.extended this work in [LBW05] via _edit automata_ —an
enforcement mechanism capable of _suppressing_ and _inserting_ system actions.
A property is thus enforceable if it can be expressed as an edit automaton
that _transforms_ invalid executions into valid ones via suppressions and
insertions. As a means to assess the correctness of these automata, the
authors introduced _soundness_ and _transparency_.

Both settings by Schneider [Sch00] and Ligatti et al.[LBW05] assume a trace
based view of the SuS and that every action can be freely manipulated by the
monitor. They also do not distinguish between the specification and the
enforcement mechanism, as properties are encoded in terms of the enforcement
model itself, i.e., as edit/truncation automata. In our prior work [ACFI18],
we addressed this issue by separating the specification and verification
aspects of the logic and explored the enforceability of $\mu$HML in a
unidirectional context and in relation to a definition of adequate enforcement
defined in terms of soundness and transparency. In this paper we adopt a
stricter notion of enforceability that requires adherence to eventual
transparency and investigate the enforceability of sHML formulas in the
context of bidirectional enforcement.

Bielova and Massacci [Bie11, BM11b] remark that, on their own, soundness and
transparency fail to specify the extent in which a transducer should modify
invalid runtime behaviour and thus introduce a _predictability_ criterion. A
transducer is _predictable_ if one can predict the edit-distance between an
invalid execution and a valid one. With this criterion, adequate monitors are
further restricted by setting an upper bound on the number of transformations
that a monitor can apply to correct invalid traces. Although this is similar
to our notion of optimality, we however use it to compare an adequate (sound
and eventual transparent) monitor to _all_ the other adequate monitors and
determine whether it is the least intrusive monitor that can enforce the
property of interest.

In [KAB+17] Könighofer et al.present a synthesis algorithm similar to our own
that produces action replacement monitors called _shields_ from safety
properties encoded as automata-based specifications. Although their shields
can analyse both the inputs and outputs of a reactive system, they still
perform unidirectional enforcement since they only modify the data associated
with the system’s output actions. By definition, shields should adhere to
correctness and minimum deviation which are, in some sense, analogous to
soundness and transparency respectively.

In [PRS+16, PRS+17], Pinisetty et al.conduct a preliminary investigation of RE
in a bidirectional setting. They, however, model the behaviour of the SuS as a
trace of input and output pairs, _a.k.a._ _reactions_ , and focus on enforcing
properties by modifying the payloads exchanged by these reactions. This way of
modelling system behaviour is, however, quite restrictive as it only applies
to synchronous reactive systems that output a value in reaction to an input.
This differs substantially from the way we model systems as LTSs, particularly
since we can model more complex systems that may opt to collect data from
multiple inputs, or supply multiple outputs in response to an input. The
enforcement abilities studied in [PRS+16, PRS+17] are also confined to action
replacement that only allows the monitor to modify the data exchanged by the
system in its reactions, and so the monitors in [PRS+16, PRS+17] are unable to
disable and enable actions. Due to their trace based view of the system, their
correctness specifications do not allow for defining correct system behaviour
in view of its different execution branches. This is particularly useful when
considering systems whose inputs may lead them into taking erroneous
computation branches that produce invalid outputs. Moreover, since their
systems do not model communication ports, their monitors cannot influence
directly the control structure of the SuS, e.g., by opening, closing or
rerouting data through different ports.

Finally, Lanotte et al. [LMM20] employ similar synthesis techniques and
correctness criteria to ours (Sections 4 and 4) to generate enforcement
monitors for a timed setting. They apply their process-based approach to build
tools that enforce data-oriented security properties. Although their
implementations handle the enforcement of first-order properties, the theory
on which it is based does not, nor does it investigate logic enforceability.

## References

  * [AAA+21] Duncan Paul Attard, Luca Aceto, Antonis Achilleos, Adrian Francalanza, Anna Ingólfsdóttir, and Karoliina Lehtinen.  Better late than never or: Verifying asynchronous components at runtime.  In Kirstin Peters and Tim A. C. Willemse, editors, Formal Techniques for Distributed Objects, Components, and Systems - 41st IFIP WG 6.1 International Conference, FORTE 2021, Held as Part of the 16th International Federated Conference on Distributed Computing Techniques, DisCoTec 2021, Valletta, Malta, June 14-18, 2021, Proceedings, volume 12719 of Lecture Notes in Computer Science, pages 207–225. Springer, 2021.
  * [AAF+20] Luca Aceto, Antonis Achilleos, Adrian Francalanza, Anna Ingólfsdóttir, and Sævar Örn Kjartansson.  Determinizing monitors for HML with recursion.  J. Log. Algebraic Methods Program., 111:100515, 2020.
  * [AAF+21] Luca Aceto, Antonis Achilleos, Adrian Francalanza, Anna Ingólfsdóttir, and Karoliina Lehtinen.  The Best a Monitor Can Do.  In CSL, volume 183 of LIPIcs, pages 7:1–7:23. Schloss Dagstuhl, 2021.
  * [AAFI18] Luca Aceto, Antonis Achilleos, Adrian Francalanza, and Anna Ingólfsdóttir.  A Framework for Parameterized Monitorability.  In FoSSaCS, pages 203–220. Springer, 2018.
  * [AAFI21] Luca Aceto, Duncan Paul Attard, Adrian Francalanza, and Anna Ingólfsdóttir.  On benchmarking for concurrent runtime verification.  In FASE, volume 12649 of LNCS, pages 3–23. Springer, 2021\.
  * [ACFI18] Luca Aceto, Ian Cassar, Adrian Francalanza, and Anna Ingólfsdóttir.  On Runtime Enforcement via Suppressions.  In CONCUR, volume 118, pages 34:1–34:17. Schloss Dagstuhl, 2018\.
  * [ACFI21] Luca Aceto, Ian Cassar, Adrian Francalanza, and Anna Ingólfsdóttir.  On bidirectional runtime enforcement.  In Kirstin Peters and Tim A. C. Willemse, editors, Formal Techniques for Distributed Objects, Components, and Systems - 41st IFIP WG 6.1 International Conference, FORTE 2021, Held as Part of the 16th International Federated Conference on Distributed Computing Techniques, DisCoTec 2021, Valletta, Malta, June 14-18, 2021, Proceedings, volume 12719 of Lecture Notes in Computer Science, pages 3–21. Springer, 2021.
  * [AF16] Duncan Paul Attard and Adrian Francalanza.  A Monitoring Tool for a Branching-Time Logic.  In RV, pages 473–481. Springer, 2016.
  * [AI99] Luca Aceto and Anna Ingólfsdóttir.  Testing Hennessy-Milner Logic with Recursion.  In Wolfgang Thomas, editor, FoSSaCS, pages 41–55. Springer, 1999\.
  * [AILS07] Luca Aceto, Anna Ingólfsdóttir, Kim Guldstrand Larsen, and Jiri Srba.  Reactive Systems: Modelling, Specification and Verification.  Cambridge Univ. Press, NY, USA, 2007.
  * [Av11] Rajeev Alur and Pavol Černý.  Streaming Transducers for Algorithmic Verification of Single-pass List-processing Programs.  In POPL, pages 599–610. ACM, 2011.
  * [BCD+17] Laura Bocchi, Tzu-Chun Chen, Romain Demangeon, Kohei Honda, and Nobuko Yoshida.  Monitoring networks through multiparty session types.  TCS, 669:33 – 58, 2017.
  * [Bie11] Nataliia Bielova.  A theory of constructive and predictable runtime enforcement mechanisms.  PhD thesis, University of Trento, 2011.
  * [BM11a] Nataliia Bielova and Fabio Massacci.  Do you really mean what you actually enforced?-edited automata revisited.  Journal of Information Security, 10(4):239–254, 2011.
  * [BM11b] Nataliia Bielova and Fabio Massacci.  Predictability of enforcement.  In International Symposium on Engineering Secure Software and Systems, pages 73–86. Springer, 2011.
  * [CBD+12] Tzu-Chun Chen, Laura Bocchi, Pierre-Malo Deniélou, Kohei Honda, and Nobuko Yoshida.  Asynchronous Distributed Monitoring for Multiparty Session Enforcement.  In TGC, pages 25–45. Springer, 2012.
  * [CFA+17] Ian Cassar, Adrian Francalanza, Duncan Paul Attard, Luca Aceto, and Anna Ingólfsdóttir.  A Suite of Monitoring Tools for Erlang.  In RV-CuBES, volume 3 of Kalpa Publications in Computing, pages 41–47. EasyChair, 2017.
  * [CFAI17] Ian Cassar, Adrian Francalanza, Luca Aceto, and Anna Ingólfsdóttir.  eAOP: An Aspect Oriented Programming Framework for Erlang.  In Erlang, ACM SIGPLAN, 2017.
  * [CFS15] Ian Cassar, Adrian Francalanza, and Simon Said.  Improving Runtime Overheads for detectEr.  In FESCA, volume 178 of EPTCS, pages 1–8, 2015.
  * [FAI17] Adrian Francalanza, Luca Aceto, and Anna Ingólfsdóttir.  Monitorability for the Hennessy-Milner logic with recursion.  Formal Methods in System Design, 51(1):87–116, 2017.
  * [FFM08] Yliès Falcone, Jean-Claude Fernandez, and Laurent Mounier.  Synthesizing enforcement monitors wrt. the safety-progress classification of properties.  In Information Systems Security. Springer, 2008.
  * [FFM12] Yliès Falcone, Jean-Claude Fernandez, and Laurent Mounier.  What can you verify and enforce at runtime?  Journal on Software Tools for Technology Transfer, 14(3):349, 2012\.
  * [Fra17] Adrian Francalanza.  Consistently-Detecting Monitors.  In CONCUR, volume 85 of LIPIcs, pages 8:1–8:19, Dagstuhl, Germany, 2017.
  * [Fra21] Adrian Francalanza.  A Theory of Monitors.  Information and Computation, page 104704, 2021.
  * [HL95] M. Hennessy and X. Liu.  A Modal Logic for Message Passing Processes.  Acta Informatica, 32(4):375–393, Apr 1995.
  * [HL96] M. Hennessy and H. Lin.  Proof systems for message-passing process algebras.  Formal Aspects of Computing, 8(4):379–407, 1996.
  * [HRTZ18] Klaus Havelund, Giles Reger, Daniel Thoma, and Eugen Zălinescu.  Monitoring Events that Carry Data, pages 61–102.  Springer International Publishing, Cham, 2018.
  * [JGP16] Limin Jia, Hannah Gommerstadt, and Frank Pfenning.  Monitors and blame assignment for higher-order session types.  In POPL, pages 582–594, NY, USA, 2016. ACM.
  * [KAB+17] Bettina Könighofer, Mohammed Alshiekh, Roderick Bloem, Laura Humphrey, Robert Könighofer, Ufuk Topcu, and Chao Wang.  Shield synthesis.  Formal Methods in System Design, 51(2):332–361, Nov 2017.
  * [Koz83] Dexter C. Kozen.  Results on the propositional $\mu$-calculus.  Theoretical Computer Science, 27:333–354, 1983.
  * [KT12] Raphaël Khoury and Nadia Tawbi.  Which security policies are enforceable by runtime monitors? a survey.  Computer Science Review, 6(1):27–45, 2012.
  * [Lar90] Kim G Larsen.  Proof systems for satisfiability in Hennessy-Milner logic with recursion.  Theoretical Computer Science, 72(2):265–288, 1990.
  * [LBW05] Jay Ligatti, Lujo Bauer, and David Walker.  Edit automata: enforcement mechanisms for run-time security policies.  Journal of Information Security, 4(1):2–16, 2005.
  * [LBW09] Jay Ligatti, Lujo Bauer, and David Walker.  Run-time enforcement of nonsafety policies.  ACM Trans. Inf. Syst. Secur., 12(3):19:1–19:41, January 2009.
  * [LMM20] Ruggero Lanotte, Massimo Merro, and Andrei Munteanu.  Runtime enforcement for control system security.  In CSF, pages 246–261. IEEE, 2020.
  * [MPW92] Robin Milner, Joachim Parrow, and David Walker.  A Calculus of Mobile Processes, I.  Information and Computation, 100(1):1–40, 1992.
  * [PRS+16] Srinivas Pinisetty, Partha S. Roop, Steven Smyth, Stavros Tripakis, and Reinhard von Hanxleden.  Runtime enforcement of reactive systems using synchronous enforcers.  CoRR, abs/1612.05030, 2016.
  * [PRS+17] Srinivas Pinisetty, Partha S. Roop, Steven Smyth, Nathan Allen, Stavros Tripakis, and Reinhard Von Hanxleden.  Runtime enforcement of cyber-physical systems.  ACM Trans. Embed. Comput. Syst., 16(5s):178:1–178:25, September 2017.
  * [RH97] J. Rathke and M. Hennessy.  Local model checking for value-passing processes (extended abstract).  In TACS, pages 250–266. Springer, 1997.
  * [Sak09] Jacques Sakarovitch.  Elements of Automata Theory.  Cambridge University Press, New York, NY, USA, 2009.
  * [San11] Davide Sangiorgi.  Introduction to Bisimulation and Coinduction.  Cambridge University Press, New York, NY, USA, 2011.
  * [Sch00] Fred B Schneider.  Enforceable security policies.  ACM Transactions on Information and System Security (TISSEC), 3(1):30–50, 2000.
  * [vHRF17] A. C. van Hulst, M. A. Reniers, and W. J. Fokkink.  Maximally permissive controlled system synthesis for non-determinism and modal logic.  Discrete Event Dynamic Systems, 27(1):109–142, 2017.


# Parametric excitations of coupled nanomagnets

Domonkos Laszlo Farkas  Gyorgy Csaba<EMAIL_ADDRESS>Faculty of
Information Technology and Bionics, Pazmany University Budapest, Hungary

###### Abstract

We demonstrate that parametrically excited eigenmodes in nearby nanomagnets
can be coupled to each other. Both positive (in-phase) and negative (anti-
phase) couplings can be realized by a combination of appropriately chosen
geometry and excitation field frequency. The oscillations are sufficiently
stable against thermal fluctuations. The phase relation between field-coupled
nanomagnets shows a hysteretic behavior with the phase relation being locked
over a wide frequency range. We envision that this computational study lays
the groundwork to use field-coupled nanomagnets as parametrons as building
blocks of logic devices, neuromorphic systems of Ising machines.

##  I Introduction

Our research is motivated by the possibility of using the oscillation phase of
a nanomagnet as the information-carrying physical variable in a computing
system. The idea of using the phase of a parametrically-excited system as a
variable in computing has a long history ref:wigington  – in fact the magnetic
parametron was one of the first practically successful computing paradigms
before the age of integrated, transistor-based digital electronics.

In this paper - following the footsteps of earlier works ref:parametron ;
ref:bauer  – we first show that small-sized nanomagnets can indeed act as
parametrons. It means that they produce $f_{0}$ frequency oscillations to a
$2f_{0}$ frequency excitation and be locked to this external pumping field
with two distinct, stable phases.

To use individual magnetic parametrons as building blocks of computing devices
they should be interconnected with each other. One possibility is to use the
stray field of the magnets for this, which comes for free, not requiring
additional hardware. The oscillatory stray field of a neighboring magnet
shifts the resonance frequency of a node in such a way that a given $2f_{0}$
excitation may favorably excite only on or the other phase, effectively
realizing positive (in-phase) or negative (anti-phase) couplings between the
phase variables of the magnets.

Nanomagnets coupled by their stray fields have been intensely researched for
applications in beyond-Moore computing paradigms. For example, in Nanomagnet
Logic (NML) the magnetic orientation of a nanomagnet acts as a logic variable
ref:nml , and this magnetic orientation, in turn, controlled by the field-
coupling to neighboring magnets. The NML architecture enables a potentially
low-power, non-volatile, straightforwardly realizable architecture for Boolean
and non-Boolean functions. In this paper we extend the NML paradigm to
dynamically-coupled nanomagnets. We call the field-coupled building blocks
Coupled NanoMagnet Parametrons (CNMPs).

The realization of computationally useful magnetization patterns requires both
negatively (anti-phase) and positively (in-phase) coupled magnets or at least
negatively coupled ones. In-phase coupled magnets alone are not
computationally useful as they have only a trivial ground state with all
magnets oscillating in phase. We will show that the strength and the sign of
couplings can be engineered by choosing the right parametric excitation
frequency for a given geometry.

##  II Oscillatory states of a stand-alone nanomagnet

Oscillatory eigenstates of nanoscale magnets are a well-studied and the reader
is referred to ref:serpico  for more information. Here we are primarily
interested in parametrically excited quasi-uniform oscillation modes in small
magnets as they are the ones that provide sufficiently strong fields for
coupling to neighbors.

###  II.1 Simulation setup

We study an ellipse-shaped (major axis=160 nm, minor axis=80 nm, thickness=20
nm) YIG nanomagnet, see Figure 1. The elliptical shape is useful to increase
the ellipticity of the magnetization precession orbit and remove the
degeneracy of eigenmodes. A static bias field of 500 mT is applied along the
easy axis of the nanomagnet. Additionally, a weaker sinusoidal field is
applied to generate oscillations of the magnet. The sinusoidal field is
aligned parallel to the bias field for parametric excitation and perpendicular
to the bias field in case of direct excitation of a mode.

Figure 1: Geometry for exciting the mode with eigenfrequency $f_{0}$ of an
ellipse-shaped magnet (2b=a). In $a)$, the eigenmode is excited by its
eigenfrequency with a field perpendicular to the bias field (and thus falls in
the same plane as the oscillation). $b)$ As the spins’ precession orbit is
elliptical in this eigenmode, it is also possible to parametrically pump it
with a double-frequency ($f=2f_{0}$) excitation along the bias field’s
direction.

The relatively small nanomagnet size is chosen for two reasons. The quasi-
uniform oscillation creates the strongest stray field so the strongest
couplings are expected to nearby magnets. In addition to this, for such small
nanomagnets only the lowest-energy eigenmode is accessible with a
straightforwardly applicable $f<20$ GHz excitation frequency - this simplifies
the physical picture by removing the internal degrees of freedom.

For the calculations the Mumax simulation code ref:mumax  is used with
standard YIG parameters ($M_{s}$ = 1.40E+5 A/m, $A$ = 3.65E-12 J/m, $\alpha$ =
0.0005) and we assume that this thin film is precisely modeled by a two-
dimensional simulation (single layer of computing cells along $z$ axis, but
with 20 nm height). We used the temperature-dependent module of Mumax and most
simulations (unless otherwise indicated) done at room temperature ($T=300$ K).
It simulates thermal fluctuations by adding a white-noise-like effective
magnetic field to all the computing cells. The higher the temperature, the
more prominent the fluctuations becomes. Most simulations were repeated
multiple times using different seeds for random thermal field generation -
this removes simulation artifacts and ensures the effects we see are robust
against thermal noise. Thermal effects do influence the results: for example,
parametric excitations require significantly higher excitation power than they
would require at zero temperature.

###  II.2 Localizing eigenfrequencies of modes

Eigenfrequencies of a nanomagnet are determined by the effective magnetic
field, which includes the magnet’s own demagnetizing field and external field
sources.

We use a high-bandwidth pulse (impulse response) and the thermal spectrum to
identify eigenmode frequencies. Both methods excite a wide range of
frequencies, thus they excite all eigenfrequencies at once. Applying Fourier
transform (FFT) on the time-domain magnetization dynamics will show them as
peaks in the spectral domain. Although the two exciting methods may provide
similar results, looking at thermal fluctuations have some benefits. First, it
has more uniform spectral density so it excites all eigenfrequencies more
evenly. Secondly, it can be prolonged at any scale (e.g. for better FFT
resolution) with the same effectiveness, whereas the impulse response results
in an exponential decay. Thirdly, the high magnetic field of the impulse may
distort the system’s behaviour, as eigenfrequencies depend on the magnetic
field.

Eigenmodes may alternatively may identified by sweeping the frequency over
time and determining the frequency where maximum-amplitude oscillations occur
- this method is useful if the scanned frequency range is narrow.

###  II.3 Excitation of eigenmodes, parametric pumping

Parametric excitation of nanomagnet eigenmodes is widely studied, see e.g.
ref:demidov ; ref:efield . Here we focus on perhaps the simplest case of a
parametric process, the excitation of a quasi-uniform mode, leaving the
oscillation phase a free variable.

A simple picture of parametric excitation is illustrated in Figure 1b
contrasting it to the direct excitation of 1a. In direct excitation, a
resonant excitation field is applied perpendicular to static magnetization,
maximizing the torque. Although resonant excitation requires lower excitation
power, the resulting oscillation does not have a degree of freedom such as two
possible phases for parametric pumping.

In parametric excitation, the ellipsoidal-shaped nanomagnet is excited
parallel to the bias field with an oscillatory magnetic field of $B_{osc}$
(typically in the 25 mT range) and frequency $f=2f_{0}$. As Figure 1 shows, a
precessional motion with $f_{0}$ frequency and non-zero ellipticity will have
a component oscillating at $2f_{0}$ frequency along the biased easy axis. The
parametric pumping will couple to this component and sustain the precession
against dispersion losses. As illustrated in Figure 2a), a small
eigenoscillation (buried in thermal noise) occurring at $f_{0}$ will be
amplified to large amplitudes. Figure 2a) is an illustration, and Figure 2b)
is a result of actual simulations of an ellipsoidal nanomagnet, starting from
different, temperature-induced random states. It typically takes several
hundred oscillation cycles to reach the steady-state oscillation amplitude.

(a) Artificial buildup of a parametron.

(b) Resulting CNMP oscillations using different random seeds.

Figure 2: Parametric pumping allows oscillations with two different phase, and
the same amplitude. Subfigure b) shows that oscillation phase is more robust
to thermal fluctuations than amplitude. The magnet’s major axis was 160 nm,
the minor 80 nm and the magnetization precesses in a coherent way.

A key feature of parametric excitation, as shown in Figure 2, is that the
oscillations of the magnet may occur in one of exactly two possible locked
phases with respect to the excitation frequency. In stand-alone magnets the
phase is ’decided’ randomly by the initial random state. It is worthwhile to
note that in-larger sized magnets, non-uniform modes will be excited by
parametric pumping, and they add additional degrees of freedom to the system.
So locking to the subharmonic of the excitation could happen in multiple ways
as shown in Figure3. We chose the size of the nanomagnet in the deep submicron
regime to suppress the formation of these modes.

Figure 3: a) In case of larger-sized magnets, modes can be localized on one
side of the magnet. Thus parametrically excited eigenmodes may form with
different amplitude due to this internal degrees of freedom. The size of the
magnet was 640 nm x 320 nm, temperature was set to zero for these simulations.

##  III Mode coupling in coupled nanomagnets

In case of two magnets placed next to each other, the stray field shifts
eigenfrequencies. We can obtain the modified system’s eigenfrequencies with
the same methodology as for a stand-alone magnet. First we used the thermal
fluctuations as a uniform, high-bandwidth excitation, which excited all modes
at once. Then we applied FFT on the sampled average magnetization of each
magnet separately to localize the eigenfrequencies.

We observed that the presence of another magnet clearly affects the
eigenfrequencies. In case the magnets were placed next to each other along
their hard axis, the eigenfrequencies were lowered by a few tens of MHz. On
the other hand, when the magnets’ easy axis coincided, the effect was the
opposite, the eigenfrequencies increased. In both cases, the frequency shift
decreases as the pair’s distance increases, converging to the stand alone
magnet case. Additionally, we see new peaks, which faded as the gap increased.

Figure 4 shows the obtained frequency-domain around the first eigenfrequency
in a constellation, where the magnet pair was placed next to each other along
their hard axis (other eigenfrequencies’ or the other constellation’s domain
is quite similar, only higher in frequency). Two separate peaks, appear of
which the second one diminishes if we apply FFT on the full system’s average
magnetization rather than separately on each magnet. This indicates that the
second peak corresponds to the anti-phase oscillation of the magnets, where
they cancel out on average, whereas the first peak corresponds to the same-
phase oscillation.

If only thermal excitations drive the system, then the the two phases are
present simultaneously. If parametric pumping is applied, then one or the
other phase configuration (which is closer to $f_{0}$ will be amplified.

Figure 4: The geometry of two couples nanomagnet and their thermal spectrum.
The peaks correspond to eigenmodes coupled in different phases. The magnets
were placed next to each other along their hard ($y$) axis.

It is worthwhile to note that the modes’ spatial distribution slightly changes
compared to the stand alone magnet setup, they become more non-uniform, there
is a gradual increase in amplitude going from the magnets’ close ends towards
their far ends.

###  III.1 Sweeping the frequency around the resonance

Coupling of the magnets was studied by extracting their phases from the mumax
simulations. First we calculated the volume-averaged magnetization for the two
neighboring magnets. The magnetization values were normalized in the sliding
window, by the ratio of the maximum value (per magnet) and a predefined
constant. This step removes the amplitude-changes of the oscillations.
Secondly, we took the dot product of the two magnet’s normalized values in the
window. This dot product is positive for in-phase oscillations, as all members
are a multiplication of two same-sign values, and it is negative for anti-
phase oscillations, as all members are a multiplication of two different-sign
values. There is a strictly monotonic transition between the two.

(a)

(b)

Figure 5: Phase correlation of magnets at different frequencies for hard (a)
and easy (b) axis constellations. the black line is an indicative phase-
relation of the two magnets oscillation while the yellow texts in the middle
show the excitation frequencies at different time intervals. The magnetization
is relaxed (without RF driving) to a thermal state after each magnetization
interval.

(a)

(b)

Figure 6: Phase correlation of magnets placed in different distances. a) For
far-away magnets (80 nm), there is a relatively narrow frequency range where
the pumped magnets are in a definite phase-relation. This frequency regime
opens to much wider range when the magnets get closer to each other. b) For
even further-away magnets (1000 nm), the phase-relation is random and the
eigenfrequency shifts back to the stand alone magnet case, i.e. the magnets
don’t affect each other.

Exciting the CNMP with different excitation frequencies around the stand-alone
magnet eigenfrequency showed that depending on the frequency, both negative
(anti-phase) and positive (in-phase) couplings may occur. A clear boundary
separates the positive and negative couplings’ regimes. Figure 5 shows this
separation, using the above-mentioned indicative phase difference evaluation.
The figure also illustrates that the easy and hard axis constellations’
coupling regimes look similar, but the positive-negative coupling regimes are
reversed, i.e. the order in frequency is the following: hard axis
constellation’s positive coupling regime (15.60 GHz - 15.64 GHz), hard axis
constellation’s negative coupling regime (15.65 GHz - 15.69 GHz), stand-alone
magnet’s eigenfrequency peak (15.67 GHz - 15.69 GHz), easy axis
constellation’s negative coupling regime (15.69 GHz - 15.73 GHz), easy axis
constellation’s positive coupling regime (15.74 GHz - 15.79 GHz). So in both
cases the negative couplings are closer to the stand-alone eigenfrequency than
the positive couplings.

This separation can be explained by the eigenfrequencies’ dependence on the
magnetic field. The two magnet’s field affect each other’s effective field,
therefore its eigenfrequency as well. However this change depends on the
coupling phase, because the magnets demagnetizing field’s components and the
other magnet’s effect may sum up or cancel out depending on the sign of the
coupling. So that the positive and negative couplings have different
eigenfrequencies. The negative couplings might be closer to the stand-alone
eigenfrequency because more components cancel out, or the summed up components
have opposite effects on the eigenfrequencies.

The gap’s size between the magnets are crucial in regard of the coupling
regime’s separation. Figure 6 shows the same kind of simulation with a wider
gap (80 nm) and with a much wider gap (1000 nm) compared to the previous
results on Figure 5 (20 nm). One can see that the two regimes are more pushed
together at 80 nm, and completely coincide at 1000 nm (there is no
separation). Furthermore the resonant domain gets closer to the stand-alone
eigenfrequency. These observations are not surprising: as the gap size
increases the magnet’s effect on each other’s effective field decreases, so
they are getting closer to the stand-alone magnet case.

If the magnets are too far away then there is no coupling between them and
they randomly ’choose’ one of the two possible phases (forced by the
parametric excitation). Their phase difference is only stable because the
individual oscillations (parametrons) cannot switch phase after they reached a
sufficiently large amplitude. But in different simulations that use different
seeds for thermal field generation the positive-negative "coupling" pattern
would be completely different.

There might be a switch in case of coupling around the separation border,
where the lower-frequency coupling has small steady-state oscillation
amplitude. Thermal fluctuations can switch this small-amplitude oscillation
into the other coupling, but for the reverse switch, much higher fluctuations
are required, as the oscillation amplitude is much higher, so that more stable
to noise.

Finally a general rule is that, for any constellation and coupling, lower
frequencies - if still in the excitable regime- result in higher amplitude
oscillations. This is also due to the eigenfrequency - magnetic field
dependence and will be discussed in more detail in the following section.

##  IV Hysteretic behavior of phase coupling

In the previous sections (Figures 5) the frequency was changed by allowing the
magnets to relax (i.e. their phase to randomize) between the steps of the
parametric excitations.

Here we study the oscillation’s behaviour during a frequency sweep without
relaxing the magnets at frequency steps. The results are shown in Figure 7.
The phase relation shows a hysteretic behavior: a phase relation, once formed
between the magnets, remains stable over a wide range of frequencies, even at
frequencies where the opposite phase would be energetically favorable.

Apparently, CNMPs have a similar hysteresis than what is found in large-
amplitude oscillations of stand alone magnets ref:loubens : stabilized
oscillations can stay in the same coupling while sweeping through the other
coupling’s regime and in much lower frequencies, where the pair cannot be
excited in either phase without hysteresis. Even more the oscillation
amplitude increases quite notably until a sharp decay.

(a)

(b)

Figure 7: Oscillation amplitude of magnet pairs while sweeping the excitation
frequency (purple stepwise line) downwards. The initial frequency was set such
that it’s in the middle of the higher-frequency coupling regime, i.e. negative
coupling for the hard axis constellation (a), positive coupling for the easy
axis constellation (b). In both cases, the initial coupling was preserved
through a couple of tenth gigahertz wide frequency domain which is a multiple
of the width of the excitable domain without hysteresis. Note that the evenly-
spaced spikes in the phase difference are only visualization artifacts.

Even a parametrically excited stand-alone magnet can hold its phase once the
oscillation is strong enough, so it is reasonable that CNMPs do not switch
either, especially to a lower amplitude excitation.

The oscillation can retain and even increase its amplitude because of the
magnetic field dependence of the eigenfrequencies, notably the magnets’
demagnetizing fields. The greater the oscillation, the smaller the
magnetization component along the easy axis which lowers the eigenfrequency.
Thus, if the frequency is decreased slowly, the steady-state oscillation
amplitude increases and shifts the eigenfrequency downwards, so it stays close
to the excitation’s frequency. At high amplitudes it starts to become less
stable (see the increasing amplitude deviations in Figure 7 at high
amplitudes), and eventually the excitation cannot counter the growing
dispersion losses and fast decay starts. The decreasing oscillation shifts
back the eigenfrequency, further from the excitation’s frequency, so the decay
even accelerates itself.

Note that this hysteresis behaviour is much less prominent if we initially
start from the lower-frequency coupling in either constellation.

##  V Chains of coupled magnets

Phase couplings between CNMPs can be observed for longer nanomagnet chains as
well. Using a short chain of magnets result in quite more complex behaviour as
the subfigures of Figure 8 shows. First of all, the transient time is much
longer, even at the end of this 3 $\mu$s simulation, there are prominent
changes in some magnets’ oscillations, whereas stand alone magnets or CNMPs
had a couple hundred ns transient at maximum. During this transient the chain
repeatedly stucks in local minima and then switches relatively fast to higher-
amplitude oscillations overally creating a staircase-like increase of the
average oscillation amplitude. As there are still changes at the end, it is
not sure what the global optimum is.

(a) Average magnetization components of the whole chain.

(b) Oscillation amplitudes of each magnets of the chain.

Figure 8: Simulation of a chain of 9 magnets placed next to each other along
their hard axis.

By examining the pairwise phase of the neighbors, we concluded that these
steps indicate either the synchronization of one or more pairs (possibly
resulting in anti-synchronization of others) or coupling switches (in-phase to
anti-phase or vice versa) which in overall can lead to a higher energy
oscillation of the whole chain.

We also visualized a few periods of the chain’s oscillation in at least
temporarily stable states. From these movies we concluded that in-phase
couplings (what produce standing wave parts of the chain oscillation) usually
occur at the ends of the chain with low-amplitudes and they are more often for
lower excitation frequencies. Inversely, anti-phase couplings (what produce
cuts in the chain oscillation) are more common in the middle with high
amplitudes and they are more often for higher frequency excitations.

##  VI Conclusions: toward computing devices

In this paper we explored the rich dynamics of CNMPs - showing that in
parametrically excited, coupled nanomagnets the phase of oscillations can be
determined by field-coupling between the magnets. We envision that these
results may be significant both from a fundamental physics and as application
point of view.

On a physics level, CNMPs may be viewed as a phase-domain implementation of
spin ices - where couplings (potentially competing couplings) give rise to
complex magnetization patterns ref:adeyeye ; ref:jack . Spin ices are widely
studied model systems of ordering and frustration, arrays of CNMPs are
expected to show similarly complex behaviors. CNMPs likely offer more ’knobs’
to control the couplings by tuning the parametric excitation frequency. We
hope that this computational study inspires experimental investigation of the
rich phase dynamics of nanomagnet arrays.

On the application side, CNMPs are one implementation of phase-based Ising
systems ref:phase_ising , which are intensely studied to solve computationally
hard problems.

###### Acknowledgements.

The authors acknowledge financial support from the Horizon 2020 Framework
Program of the European Commission under FET-Open grant agreement no. 899646
(k-NET).

## Data Availability Statement

The data that support the findings of this study are available from the
corresponding author upon reasonable request.

## References

  * (1) Wigington, R. L. "A new concept in computing." Proceedings of the IRE 47, no. 4 (1959): 516-523.
  * (2) Shimizu, Hiroki, Tomosato Hioki, and Eiji Saitoh. "Numerical study on magnetic parametron under perpendicular excitation." Applied Physics Letters 120, no. 1 (2022): 012402.
  * (3) Elyasi, Mehrdad, Eiji Saitoh, and Gerrit EW Bauer. "Stochasticity of the magnon parametron." Physical Review B 105, no. 5 (2022): 054403.
  * (4) Csaba, Gyorgy, and Markus Becherer. "Nanomagnet logic: Computing by magnetic ordering." IEEE Nanotechnology Magazine 14, no. 1 (2019): 6-13.
  * (5) Srivastava, Titiksha, Hugo Merbouche, Igor Ngouagnia Yemeli, Nathan Beaulieu, Jamal Ben Youssef, Manuel Munoz, Ping Che et al. "Complete identification of spin-wave eigenmodes excited by parametric pumping in YIG microdisks." arXiv preprint arXiv:2301.13468 (2023).
  * (6) Vansteenkiste, Arne, Jonathan Leliaert, Mykola Dvornik, Mathias Helsen, Felipe Garcia-Sanchez, and Bartel Van Waeyenberge. "The design and verification of MuMax3." AIP advances 4, no. 10 (2014): 107133.
  * (7) Ulrichs, Henning, Vladislav E. Demidov, Sergej O. Demokritov, and Sergei Urazhdin. "Parametric excitation of eigenmodes in microscopic magnetic dots." Physical Review B 84, no. 9 (2011): 094401.
  * (8) Chen, Yu-Jin, Han Kyu Lee, Roman Verba, Jordan A. Katine, Igor Barsukov, Vasil Tiberkevich, John Q. Xiao, Andrei N. Slavin, and Ilya N. Krivorotov. "Parametric resonance of magnetization excited by electric field." Nano letters 17, no. 1 (2017): 572-577.
  * (9) Li, Yi, Vladimir V. Naletov, Olivier Klein, José Luis Prieto, Manuel Muñoz, Vincent Cros, Paolo Bortolotti, Abdelmadjid Anane, Claudio Serpico, and Grégoire De Loubens. "Nutation spectroscopy of a nanomagnet driven into deeply nonlinear ferromagnetic resonance." Physical Review X 9, no. 4 (2019): 041036.
  * (10) Talapatra, A., and A. O. Adeyeye. "Coupled magnetic nanostructures: Engineering lattice configurations." Applied Physics Letters 118, no. 17 (2021): 172404.
  * (11) Gartside, Jack C., Kilian D. Stenning, Alex Vanstone, Holly H. Holder, Daan M. Arroo, Troy Dion, Francesco Caravelli, Hidekazu Kurebayashi, and Will R. Branford. "Reconfigurable training and reservoir computing in an artificial spin-vortex ice via spin-wave fingerprinting." Nature Nanotechnology 17, no. 5 (2022): 460-469.
  * (12) Strinati, M.C., Bello, L., Pe’er, A. and Dalla Torre, E.G., 2019. Theory of coupled parametric oscillators beyond coupled Ising spins. Physical Review A, 100(2), p.023835.