\Phi_{\mathsf{eq}}\\\
\mathrm{set}(\mathscr{l}^{\prime})\cap\mathcal{F}_{\mathsf{per}}\subseteq\mathrm{set}(S)}{S\stackrel{{\scriptstyle\;\mathscr{a}^{\prime}\;}}{{\Longrightarrow}}_{\mathcal{R},\mathsf{E},\mathsf{eq}}S\setminus^{\mathsf{m}}(\mathscr{l}^{\prime}\cap^{\mathsf{m}}\mathcal{F}_{\mathsf{lin}})\cup^{\mathsf{m}}\mathscr{r}^{\prime}}$

where

$\Phi_{\mathsf{eq}}=\bigwedge_{f\in\Sigma_{\mathsf{eq}}\wedge
f(t_{1},\dots,t_{k})\in\mathscr{a}^{\prime}}\phi_{\mathsf{eq}}(f)(t_{1},\dots,t_{k}).$

Let $\mathrm{Tr}^{\prime}_{eq}(\mathcal{R})$ and
$\mathrm{Tr}_{\mathsf{t},eq}(\mathcal{R})$ be the associated set of traces,
respectively filtered and filtered without collisions, defined as for the
normal semantics. We have

$\mathrm{Tr}^{\prime}_{eq}(\mathcal{R})=\mathrm{Tr}^{\prime}(\mathcal{R})\cap\mathsf{R}_{\mathsf{eq}}\quad\text{and}\quad\mathrm{Tr}_{\mathsf{t},eq}(\mathcal{R})=\mathrm{Tr}_{\mathsf{t}}(\mathcal{R}).$

We prove the refinement results (Lemmas 1 and 2) on the modified semantics for
multiset rewriting, which enforces equality checks at each step rather than in
the end as a trace restriction. That is, we prove that the traces of the
composition of component systems are included in the traces of the original
multiset rewriting system _for the modified semantics_.

This is more convenient, as it allows us, when writing component systems as
guarded event systems, to incorporate the equality conditions directly in the
guard of each event. That is closer to the way these checks are performed in
the implementation, and therefore helps produce specifications that will be
easier to verify on the code.

Therefore, in the end, the global soundness result we obtain states that the
traces of the parallel composition of each role’s implementation are included
in the traces of the original MSR system _for the modified semantics_.

Thanks to Proposition 3, these are the same as the traces for the usual
semantics, with the equality restriction, which is the set of traces
considered by Tamarin.

###  E.2 Assumptions

We now recall in detail the formatting assumptions introduced in Section 3.1.

We fix sets of names $\mathit{pub}$, $\mathit{fresh}$, $\mathcal{V}$, a
signature $\Sigma$, and the set of terms $\mathcal{T}$ constructed on them,
with an equational theory $\mathsf{E}$. Let us also fix $n\geq 1$, the number
of roles in the system we consider.

We consider a fact signature of the form

$\Sigma_{\mathsf{facts}}=\Sigma_{\mathsf{act}}\uplus\Sigma_{\mathsf{env}}\uplus(\biguplus_{1\leq
i\leq n}\Sigma_{\mathsf{state}}^{i})$

for some arbitrary (but disjoint) sets of facts symbols
$\Sigma_{\mathsf{env}},\Sigma_{\mathsf{act}},\Sigma_{\mathsf{state}}^{i}$ for
$1\leq i\leq n$, intended to represent respectively environment facts, the
action facts, and each role’s internal states. Note that each of these sets
may contain linear and persistent facts. We additionally assume that
$\Sigma_{\mathsf{env}}$ contains subsets $\Sigma_{\mathsf{in}}$,
$\Sigma_{\mathsf{out}}$ which we call input and output fact symbols, with
$\mathsf{Fr},\mathsf{in}\in\Sigma_{\mathsf{in}}$,
$\mathsf{out}\in\Sigma_{\mathsf{out}}$, and
$\mathsf{K}\in\Sigma_{\mathsf{env}}\setminus(\Sigma_{\mathsf{in}}\cup\Sigma_{\mathsf{out}})$.
Furthermore, we assume that there is an initialization fact symbol
$\mathsf{Setup}_{i}\in\Sigma_{\mathsf{in}}$ for each protocol role $i$.

We then consider a multiset rewriting system $\mathcal{R}$ of the form

$\mathcal{R}=\mathcal{R}_{\mathsf{env}}\uplus(\biguplus_{1\leq i\leq
n}\mathcal{R}_{i}).$

where $\mathcal{R}_{i}$ and $\mathcal{R}_{\mathsf{env}}$ are arbitrary
(disjoint) sets of rules intended to represent respectively each role and
environment rules, and
$\mathit{MD}_{\Sigma}\cup\\{\mathit{Fresh}\\}\subseteq\mathcal{R}_{\mathsf{env}}$.

We assume that for all rule
$\mathscr{l}\xrightarrow{\mathscr{a}}\mathscr{r}\in\mathcal{R}$,
$\mathrm{facts}(\mathscr{a})\subseteq\Sigma_{\mathsf{act}}$. For all
environment rule
$\mathscr{l}\xrightarrow{\mathscr{a}}\mathscr{r}\in\mathcal{R}_{\mathsf{env}}$,
we assume that
$\mathrm{facts}(\mathscr{l}\cup\mathscr{r})\subseteq\Sigma_{\mathsf{env}}$. In
addition, the fact $\mathsf{Setup}_{i}$ is only allowed to occur as the only
fact produced by rules in $\mathcal{R}_{\mathsf{env}}$. For all $i$, for all
$\mathscr{l}\xrightarrow{\mathscr{a}}\mathscr{r}\in\mathcal{R}_{i}$, we
assume:

  * •

$\mathrm{facts}(\mathscr{l})\subseteq\Sigma_{\mathsf{in}}\cup\Sigma_{\mathsf{state}}^{i}$;

  * •

$\mathrm{facts}(\mathscr{r})\subseteq\Sigma_{\mathsf{out}}\cup\Sigma_{\mathsf{state}}^{i}$;

  * •

at least one state fact appears in $\mathscr{r}$;

  * •

the first $k_{i}\geq 1$ arguments of all state facts in
$\mathscr{l}\xrightarrow{\mathscr{a}}\mathscr{r}$, as well as the
$\mathsf{Setup}_{i}$ fact, are reserved for role $i$’s parameters, i.e. have
the same value in all state facts and all occurrences of $\mathsf{Setup}_{i}$
in the rule. In addition, the first of these $k$ parameters must be a thread
identifier, i.e. a value of $\mathit{fresh}$ called $\mathit{rid}$. These $k$
parameters are thus never changed once the $\mathsf{Setup}_{i}$ fact is
produced to start a run of role $i$. For readability, we will group all these
initial parameters as a tuple, denoted by $\overline{init}$.

For each $\mathit{rid}\in\mathit{fresh}$, and each $i$, we denote
$\mathcal{R}_{i,\mathit{rid}}$ the set of rules in $\mathcal{R}_{i}$ where the
first argument of all state facts is instantiated with $\mathit{rid}$.

###  E.3 Step 1: Interface model

As stated in Section 3, our goal will be to separate the multiset rewriting
system into several transition systems, representing each component. We first
introduce interfaces between each component (i.e., each role, and the
environment), to make this separation easier. These interfaces are additional
facts, which we call _buffer_ facts. We add buffers for all operations we wish
to consider as I/O, i.e. the input and output facts. These take the form of
additional rules, called _I/O rules_ , that transform each such fact into a
buffered version (for $\Sigma_{\mathsf{in}}$) or vice versa (for
$\Sigma_{\mathsf{out}}$).

We first extend the fact signature by adding, for each input or output fact
$F$, a “buffered” copy $F_{i}$ for each role $i$. We define

$\displaystyle\Sigma_{\mathsf{buf}}^{i}$ $\displaystyle=\\{F_{i}\mid
F\in\Sigma_{\mathsf{in}}\cup\Sigma_{\mathsf{out}}\\}$
$\displaystyle\Sigma_{\mathsf{role}}^{i}$
$\displaystyle=\Sigma_{\mathsf{state}}^{i}\cup\Sigma_{\mathsf{buf}}^{i}$
$\displaystyle\Sigma_{\mathsf{facts}}^{\prime}$
$\displaystyle=\Sigma_{\mathsf{act}}\uplus\Sigma_{\mathsf{env}}\uplus(\biguplus_{i}\Sigma_{\mathsf{role}}^{i}).$

We then replace the facts used by the protocol rules as follows. Let
$\Sigma_{\mathsf{in}}^{-}$ be the set of input facts without the role
initialisation facts $\mathsf{Setup}_{i}$. For each role $i$, let
$\mathcal{R}^{\prime}_{i}$ be the set of rules obtained by replacing, in all
rules in $\mathcal{R}_{i}$, each fact $F(t_{1},\dots,t_{k})$ (with
$F\in\Sigma_{\mathsf{in}}^{-}\cup\Sigma_{\mathsf{out}}$) with
$F_{i}(\mathit{rid},t_{1},\dots,t_{k})$, where $\mathit{rid}$ is the thread id
parameter present in the state facts in the rule.

We also introduce the set $\mathcal{R}_{\mathsf{io}}$ of _I/O rules_ , which
translate between input or output facts and their buffered versions. The set
$\mathcal{R}_{\mathsf{io}}$ contains the following rules, for each role $i$.

$\displaystyle[F(x_{1},\dots,x_{k})]\xrightarrow{[]}[F_{i}(\mathit{rid},x_{1},\dots,x_{k})]$
for $F\in\Sigma_{\mathsf{in}}^{-}$
$\displaystyle[G_{i}(\mathit{rid},x_{1},\dots,x_{k})]\xrightarrow{[]}[G(x_{1},\dots,x_{k})]$
for $G\in\Sigma_{\mathsf{out}}$

We also count the role setup rules, which generate the $\mathsf{Setup}_{i}$
facts, as I/O rules. Hence, we move them from the set
$\mathcal{R}_{\mathsf{env}}$ to $\mathcal{R}_{\mathsf{io}}$, calling the set
of remaining environment rules $\mathcal{R}_{\mathsf{env}}^{-}$.

We then consider the system

$\mathcal{R}_{\mathsf{intf}}=\mathcal{R}_{\mathsf{env}}^{-}\uplus\mathcal{R}_{\mathsf{io}}\uplus(\biguplus_{1\leq
i\leq n}\mathcal{R}^{\prime}_{i}).$

We can now prove the following lemma, which corresponds to Lemma 1 in Section
3.2.1 (formulated here for the semantics where equality checks are performed
in each transition, rather than as a restriction, which is more convenient
later on).

######  Lemma 3.

$\mathrm{Tr}^{\prime}_{eq}(\mathcal{R}_{\mathsf{intf}})\subseteq\mathrm{Tr}^{\prime}_{eq}(\mathcal{R})$

###### Proof.

We prove this inclusion by establishing a refinement, using a simulation
relation $\mathscr{R}$. That is, we show that

  1. (1)

$(\emptyset,\emptyset)\in\mathscr{R}$;

  2. (2)

for all states $(s_{1},s^{\prime}_{1})\in\mathscr{R}$, for all transition
steps
$s^{\prime}_{1}\stackrel{{\scriptstyle\;a^{\prime}\;}}{{\Longrightarrow}}_{\mathcal{R}_{\mathsf{intf}},\mathsf{E},\mathsf{eq}}s^{\prime}_{2}$
there exists a sequence of transitions
$s_{1}\stackrel{{\scriptstyle\;a_{1}\;}}{{\Longrightarrow}}_{\mathcal{R},\mathsf{E},\mathsf{eq}}\dots\stackrel{{\scriptstyle\;a_{m}\;}}{{\Longrightarrow}}_{\mathcal{R},\mathsf{E},\mathsf{eq}}s_{m}$
such that $(s_{m},s^{\prime}_{2})\in\mathscr{R}$, and $\langle
a_{i}\rangle_{1\leq i\leq m,a_{i}\neq\emptyset}=\langle a^{\prime}\rangle$. In
other words, there exists a sequence of transitions that reaches a state
related to $s^{\prime}_{2}$, and produces a sequence of $m$ actions, among
which one is equal to $a^{\prime}$, while the others are empty. In the proof
we will actually only have $m\in\\{0,1\\}$.

We use the relation $\mathscr{R}$ such that $(s,s^{\prime})\in\mathscr{R}$ if
and only if $s$ is the state obtained from $s^{\prime}$ by removing the
indices $i$ from all facts, as well as the first argument $\mathit{rid}$ added
to buffered facts. The first point, $(\emptyset,\emptyset)\in\mathscr{R}$, is
clear.

Let $(s_{1},s^{\prime}_{1})\in\mathscr{R}$, and consider a step
$s^{\prime}_{1}\stackrel{{\scriptstyle\;a\;}}{{\Longrightarrow}}_{\mathcal{R}_{\mathsf{intf}},\mathsf{E},\mathsf{eq}}s^{\prime}_{2}$.
We can distinguish several cases for the rule in $\mathcal{R}_{\mathsf{intf}}$
of which it is an instance.

  * •

if it is a rule
$\mathscr{l}^{\prime}\xrightarrow{\mathscr{a}^{\prime}}\mathscr{r}^{\prime}\in\mathcal{R}^{\prime}_{i}$:
the transition is thus

$s^{\prime}_{1}\stackrel{{\scriptstyle\;\mathscr{a}^{\prime}\theta\;}}{{\Longrightarrow}}_{\mathcal{R}_{\mathsf{intf}},\mathsf{E},\mathsf{eq}}s^{\prime}_{2}=s^{\prime}_{1}\setminus^{\mathsf{m}}(\mathscr{l}^{\prime}\theta\cap^{\mathsf{m}}\mathcal{F}_{\mathsf{lin}})\cup^{\mathsf{m}}\mathscr{r}^{\prime}\theta$

for some ground $\theta$ such that
$\mathscr{l}^{\prime}\theta\cap^{\mathsf{m}}\mathcal{F}_{\mathsf{lin}}\subseteq^{\mathsf{m}}s^{\prime}_{1}$
and
$\mathrm{set}(\mathscr{l}^{\prime}\theta)\cap\mathcal{F}_{\mathsf{per}}\subseteq\mathrm{set}(s^{\prime}_{1})$.
Let $\mathit{rid}$ be the name with which $\theta$ instantiates the first
argument (thread id) of the rule’s state facts and buffered facts. By
construction, there exists a rule
$\mathscr{l}\xrightarrow{\mathscr{a}}\mathscr{r}\in\mathcal{R}_{i}$ that can
be obtained from
$\mathscr{l}^{\prime}\xrightarrow{\mathscr{a}^{\prime}}\mathscr{r}^{\prime}$
by replacing each symbol $F_{i}$ with the unlabelled symbol $F$, and removing
its first argument (which is $\mathit{rid}$). Note that, by assumption,
$\mathscr{a}$ does not contain fact symbols in $\Sigma_{\mathsf{env}}$, and
thus $\mathscr{a}=\mathscr{a}^{\prime}$.

Since $(s_{1},s^{\prime}_{1})\in\mathscr{R}$ and
$\mathscr{l}^{\prime}\theta\cap^{\mathsf{m}}\mathcal{F}_{\mathsf{lin}}\subseteq^{\mathsf{m}}s^{\prime}_{1}$,
we have
$\mathscr{l}\theta\cap^{\mathsf{m}}\mathcal{F}_{\mathsf{lin}}\subseteq^{\mathsf{m}}s_{1}$.
For similar reasons, we also have
$\mathrm{set}(\mathscr{l}\theta)\cap\mathcal{F}_{\mathsf{per}}\subseteq\mathrm{set}(s_{1})$.
Hence, by applying rule
$(\mathscr{l}\xrightarrow{\mathscr{a}}\mathscr{r})\theta$, we have

$s_{1}\stackrel{{\scriptstyle\;\mathscr{a}\theta\;}}{{\Longrightarrow}}_{\mathcal{R},\mathsf{E},\mathsf{eq}}s_{1}\setminus^{\mathsf{m}}(\mathscr{l}\theta\cap^{\mathsf{m}}\mathcal{F}_{\mathsf{lin}})\cup^{\mathsf{m}}\mathscr{r}\theta.$

Since $(s_{1},s^{\prime}_{1})\in\mathscr{R}$, we also have
$(s_{1}\setminus^{\mathsf{m}}(\mathscr{l}\theta\cap^{\mathsf{m}}\mathcal{F}_{\mathsf{lin}})\cup^{\mathsf{m}}\mathscr{r}\theta,s^{\prime}_{1}\setminus^{\mathsf{m}}(\mathscr{l}^{\prime}\theta\cap^{\mathsf{m}}\mathcal{F}_{\mathsf{lin}})\cup^{\mathsf{m}}\mathscr{r}^{\prime}\theta)\in\mathscr{R}$.

  * •

if it is a rule
$\mathscr{l}^{\prime}\xrightarrow{\mathscr{a}^{\prime}}\mathscr{r}^{\prime}\in\mathcal{R}_{\mathsf{env}}^{-}$:
the transition is thus

$s^{\prime}_{1}\stackrel{{\scriptstyle\;\mathscr{a}^{\prime}\theta\;}}{{\Longrightarrow}}_{\mathcal{R}_{\mathsf{intf}},\mathsf{E},\mathsf{eq}}s^{\prime}_{2}=s^{\prime}_{1}\setminus^{\mathsf{m}}(\mathscr{l}^{\prime}\theta\cap^{\mathsf{m}}\mathcal{F}_{\mathsf{lin}})\cup^{\mathsf{m}}\mathscr{r}^{\prime}\theta$

for some ground $\theta$ such that
$\mathscr{l}^{\prime}\theta\cap^{\mathsf{m}}\mathcal{F}_{\mathsf{lin}}\subseteq^{\mathsf{m}}s^{\prime}_{1}$
and
$\mathrm{set}(\mathscr{l}^{\prime}\theta)\cap\mathcal{F}_{\mathsf{per}}\subseteq\mathrm{set}(s^{\prime}_{1})$.
By construction,
$\mathscr{l}^{\prime}\xrightarrow{\mathscr{a}^{\prime}}\mathscr{r}^{\prime}\in\mathcal{R}_{\mathsf{env}}$.
By the formatting assumptions,
$\mathrm{facts}(\mathscr{l}^{\prime}\cup\mathscr{r}^{\prime})\subseteq\Sigma_{\mathsf{env}}$.
Hence, the facts in $\mathscr{l}^{\prime}\theta$ and
$\mathscr{r}^{\prime}\theta$ are not touched by $\mathscr{R}$. Thus, since
$(s_{1},s^{\prime}_{1})\in\mathscr{R}$ and
$\mathscr{l}^{\prime}\theta\cap^{\mathsf{m}}\mathcal{F}_{\mathsf{lin}}\subseteq^{\mathsf{m}}s^{\prime}_{1}$,
we have
$\mathscr{l}^{\prime}\theta\cap^{\mathsf{m}}\mathcal{F}_{\mathsf{lin}}\subseteq^{\mathsf{m}}s_{1}$.
Similarly,
$\mathrm{set}(\mathscr{l}^{\prime}\theta)\cap\mathcal{F}_{\mathsf{per}}\subseteq\mathrm{set}(s_{1})$.
Thus, by applying rule
$\mathscr{l}^{\prime}\xrightarrow{\mathscr{a}^{\prime}}\mathscr{r}^{\prime}$,
we have

$s_{1}\stackrel{{\scriptstyle\;\mathscr{a}^{\prime}\theta\;}}{{\Longrightarrow}}_{\mathcal{R},\mathsf{E},\mathsf{eq}}s_{1}\setminus^{\mathsf{m}}(\mathscr{l}^{\prime}\theta\cap^{\mathsf{m}}\mathcal{F}_{\mathsf{lin}})\cup^{\mathsf{m}}\mathscr{r}^{\prime}\theta.$

Since $(s_{1},s^{\prime}_{1})\in\mathscr{R}$ and
$\mathrm{facts}(\mathscr{l}^{\prime}\cup\mathscr{r}^{\prime})\subseteq\Sigma_{\mathsf{env}}$,
we also have
$(s_{1}\setminus^{\mathsf{m}}(\mathscr{l}^{\prime}\theta\cap^{\mathsf{m}}\mathcal{F}_{\mathsf{lin}})\cup^{\mathsf{m}}\mathscr{r}^{\prime}\theta,s^{\prime}_{1}\setminus^{\mathsf{m}}(\mathscr{l}^{\prime}\theta\cap^{\mathsf{m}}\mathcal{F}_{\mathsf{lin}})\cup^{\mathsf{m}}\mathscr{r}^{\prime}\theta)\in\mathscr{R}$.

  * •

Finally, the case of I/O rules remains. We write the proof for the case of an
input rule in $\Sigma_{\mathsf{in}}$, as the output case is similar, and the
setup case is similar to the previous case ($\mathcal{R}_{\mathsf{env}}^{-}$).
Assume the transition rule applied is
$[F(x_{1},\dots,x_{k})]\xrightarrow{[]}[F_{i}(\mathit{rid},x_{1},\dots,x_{k})]$.
In that case the transition is

$s^{\prime}_{1}=s^{\prime}\cup^{\mathsf{m}}\\{|F(M_{1},\dots,M_{k})|\\}\stackrel{{\scriptstyle\;\emptyset\;}}{{\Longrightarrow}}_{\mathcal{R}_{\mathsf{intf}},\mathsf{E},\mathsf{eq}}s_{2}^{\prime}=s^{\prime}\cup^{\mathsf{m}}\\{|F_{i}(\mathit{rid},M_{1},\dots,M_{k})|\\}$

for some $s^{\prime}$, $M_{1},\dots,M_{k}$, $\mathit{rid}$. Since
$(s_{1},s^{\prime}_{1})\in\mathscr{R}$, there exists $s$ such that
$s_{1}=s\cup^{\mathsf{m}}\\{|F(M_{1},\dots,M_{k})|\\}$ and
$(s,s^{\prime})\in\mathscr{R}$. Hence we also have
$(s_{1},s^{\prime}_{2})\in\mathscr{R}$, and no transition needs to be
performed on $s_{1}$.

∎

###  E.4 Step 2: express the MSR system as an event system

Before we separate our monolithic system into the composition of several
component systems, we switch to the formalism of guarded event systems, which
will be more appropriate when extracting an I/O specification.

We associate to $\mathcal{R}_{\mathsf{intf}}$ a guarded transition system
$\mathscr{E}=(\mathcal{S},\mathcal{E},\mathcal{G},\mathcal{U})$:

  * •

$\mathcal{S}$ is the set of multisets of ground facts from the signature
$\Sigma_{\mathsf{facts}}^{\prime}$;

  * •

$\mathcal{E}=(\bigcup_{1\leq i\leq n,\text{ for each
}\mathit{rid}}\mathcal{E}^{s}_{i,\mathit{rid}})\cup\mathcal{E}^{e}\cup\mathcal{E}^{\mathsf{io}}$
with

$\begin{array}[]{l@{}l}\mathcal{E}^{s}_{i,\mathit{rid}}=\\{\mathsf{skip}\\}\cup\\{e^{s}_{i,\mathit{rid},j}(\theta,\mathscr{l}^{\prime},\mathscr{a}^{\prime},\mathscr{r}^{\prime})\;|&\mathscr{l}^{\prime},\mathscr{a}^{\prime},\mathscr{r}^{\prime}\text{
multisets of ground facts},\\\ &\theta\text{ ground inst. of
}\mathrm{vars}(\mathscr{l})\cup\mathrm{vars}(\mathscr{a})\cup\mathrm{vars}(\mathscr{r})\\\
&\text{where }\mathscr{l}\xrightarrow{\mathscr{a}}\mathscr{r}\text{ is the
$j$th rule in }\mathcal{R}^{\prime}_{i}\text{ with the first}\\\
&\text{parameter of all state and setup facts}\\\ &\text{instantiated with
}\mathit{rid}\\}\end{array}$

and

$\begin{array}[]{l@{}l}\mathcal{E}^{e}=\\{\mathsf{skip}\\}\cup\\{e^{e}_{j}(\theta,\mathscr{l}^{\prime},\mathscr{a}^{\prime},\mathscr{r}^{\prime})\;|&\mathscr{l}^{\prime},\mathscr{a}^{\prime},\mathscr{r}^{\prime}\text{
multisets of ground facts},\\\ &\theta\text{ ground inst. of
}\mathrm{vars}(\mathscr{l})\cup\mathrm{vars}(\mathscr{a})\cup\mathrm{vars}(\mathscr{r})\\\
&\text{where }\mathscr{l}\xrightarrow{\mathscr{a}}\mathscr{r}\text{ is the
$j$th rule in }\mathcal{R}_{\mathsf{env}}^{-}\\}\\\ \end{array}$

and

$\begin{array}[]{l@{}l}\mathcal{E}^{\mathsf{io}}=\\{\lambda_{F,i,\mathit{rid}}(\theta,\mathscr{l}^{\prime},\mathscr{a}^{\prime},\mathscr{r}^{\prime})\;|&F\in\Sigma_{\mathsf{in}}\cup\Sigma_{\mathsf{out}}\\\
&\mathscr{l}^{\prime},\mathscr{a}^{\prime},\mathscr{r}^{\prime}\text{
multisets of ground facts},\\\ &\theta\text{ ground inst. of
}\mathrm{vars}(\mathscr{l})\cup\mathrm{vars}(\mathscr{a})\cup\mathrm{vars}(\mathscr{r})\\\
&\text{where }\mathscr{l}\xrightarrow{\mathscr{a}}\mathscr{r}\text{ is the
rule associated to fact $F$ and}\\\ &\text{role $i$ in
$\mathcal{R}_{\mathsf{io}}$, with its first parameter instantiated with
$\mathit{rid}$}\\}\\\ \end{array}$

  * •

$\mathcal{G}$: the guard for a parametric event
$e(\theta,\mathscr{l}^{\prime},\mathscr{a}^{\prime},\mathscr{r}^{\prime})$
associated to a rule
$\mathscr{l}\xrightarrow{\mathscr{a}}\mathscr{r}\in\mathcal{R}^{\prime}$, in
the current state $s$, is

$\mathscr{l}^{\prime}=_{\mathsf{E}}\mathscr{l}\theta\;\wedge\;\mathscr{a}^{\prime}=_{\mathsf{E}}\mathscr{a}\theta\;\wedge\;\mathscr{r}^{\prime}=_{\mathsf{E}}\mathscr{r}\theta\;\wedge\;G(\mathscr{l}^{\prime},s)\;\wedge\;\Phi_{\mathsf{eq}}(\mathscr{a}^{\prime})$

where

$G(\mathscr{l}^{\prime},s)=(\mathscr{l}^{\prime}\cap^{\mathsf{m}}\mathcal{F}_{\mathsf{lin}}\subseteq^{\mathsf{m}}s)\;\wedge\;(\mathrm{set}(\mathscr{l}^{\prime})\cap\mathcal{F}_{\mathsf{per}}\subseteq\mathrm{set}(s))$

is the actual condition for the rule and

$\Phi_{\mathsf{eq}}(\mathscr{a}^{\prime})=\bigwedge_{f\in\Sigma_{\mathsf{eq}}\wedge
f(t_{1},\dots,t_{k})\in\mathscr{a}^{\prime}}\phi_{\mathsf{eq}}(f)(t_{1},\dots,t_{k})$

is the equality check.

  * •

$\mathcal{U}$: a parametric event
$e(\theta,\mathscr{l}^{\prime},\mathscr{a}^{\prime},\mathscr{r}^{\prime})$
associated to a rule
$\mathscr{l}\xrightarrow{\mathscr{a}}\mathscr{r}\in\mathcal{R}^{\prime}$
updates the state $s$ to
$s^{\prime}=U(\mathscr{l}^{\prime},\mathscr{r}^{\prime},s)$, where

$U(\mathscr{l}^{\prime},\mathscr{r}^{\prime},s)=s\setminus^{\mathsf{m}}(\mathscr{l}^{\prime}\cap^{\mathsf{m}}\mathcal{F}_{\mathsf{lin}})\cup^{\mathsf{m}}\mathscr{r}^{\prime}.$

Note that the event label
$\lambda_{F,i,\mathit{rid}}(\theta,\mathscr{l}^{\prime},\mathscr{a}^{\prime},\mathscr{r}^{\prime})$
we assign to events associated with rules in $\mathcal{R}_{\mathsf{io}}$
corresponds to the synchronisation label $\lambda_{F}(\overline{x})$ described
in Section 3.2.2. Since we use the LTS formalism here, it is now an event
name, rather than a fact annotating a rewrite rule. We include more parameters
here compared to that section to make the form of all our events uniform –
even though, since the form of the rules in $\mathcal{R}_{\mathsf{io}}$ is
known, by construction, it would be sufficient to only give the instantiation
of each parameter of $F$, as was done in the paper.

We let $\xrightarrow{\;\cdot\;}$ denote the reduction relation defined by
checking the guards and applying the updates for each event in $\mathcal{E}$.
Formally, $s\xrightarrow{\;E\;}s^{\prime}$ if $E$ is an event
$e(\theta,\mathscr{l}^{\prime},\mathscr{a}^{\prime},\mathscr{r}^{\prime})$
associated to a rule
$\mathscr{l}\xrightarrow{\mathscr{a}}\mathscr{r}\in\mathcal{R}_{\mathsf{intf}}$,
such that
$\mathscr{l}^{\prime}=_{\mathsf{E}}\mathscr{l}\theta\;\wedge\;\mathscr{a}^{\prime}=_{\mathsf{E}}\mathscr{a}\theta\;\wedge\;\mathscr{r}^{\prime}=_{\mathsf{E}}\mathscr{r}\theta\;\wedge\;G(\mathscr{l}^{\prime},s)\;\wedge\;\Phi_{\mathsf{eq}}(\mathscr{a}^{\prime})$,
and $s^{\prime}=U(\mathscr{l}^{\prime},\mathscr{r}^{\prime},s)$.

Let $\pi$ denote the mapping from $\mathcal{E}$ to multisets of facts, that
associates to each parametric event
$e(\theta,\mathscr{l}^{\prime},\mathscr{a}^{\prime},\mathscr{r}^{\prime})\in\mathcal{E}$
the multiset of facts $\mathscr{a}^{\prime}$.

We denote $\tilde{\pi}$ the extension of $\pi$ to sequences of events and
multisets, which applies $\pi$ and removes empty multisets of facts, i.e. for
any sequence $e=\langle e_{1},\dots,e_{n}\rangle$ of events,

$\tilde{\pi}(e)=\langle\pi(e_{i})\;|\;i=1,\dots,n\;\wedge\;\pi(e_{i})\neq\emptyset\rangle.$

Note that Section 3.3 introduced the same mapping, but in the MSR formalism.

The traces of the event system are defined as

$\mathrm{Tr}(\mathscr{E})=\\{e_{1},\dots,e_{m}\;|\;(\forall
i.\;e_{i}\in\mathcal{E})\;\wedge\;\exists
s_{1},\dots,s_{m}\in\mathcal{S}.\;\emptyset\xrightarrow{\;e_{1}\;}s_{1}\xrightarrow{\;e_{2}\;}\dots\xrightarrow{\;e_{m}\;}s_{m}\\}.$

######  Lemma 4.

$\tilde{\pi}(\mathrm{Tr}(\mathscr{E}))=\mathrm{Tr}^{\prime}_{eq}(\mathcal{R}_{\mathsf{intf}})$

###### Proof.

We show this lemma by proving that for any state $s$:

  1. (a)

for any event $e\in\mathcal{E}$ and any $s^{\prime}$, if
$s\xrightarrow{\;e\;}s^{\prime}$ then
$s\stackrel{{\scriptstyle\;\pi(e)\;}}{{\Longrightarrow}}_{\mathcal{R}_{\mathsf{intf}},\mathsf{E},\mathsf{eq}}s^{\prime}$

  2. (b)

for any reduction step
$s\stackrel{{\scriptstyle\;\mathscr{a}\;}}{{\Longrightarrow}}_{\mathcal{R}_{\mathsf{intf}},\mathsf{E},\mathsf{eq}}s^{\prime}$,
there exists $e$ such that $s\xrightarrow{\;e\;}s^{\prime}$ and
$\pi(e)=\mathscr{a}$.

Once these two properties are established, the lemma follows easily by
applying them successively to each reduction step – a proves the first
inclusion $(\subseteq)$ and b proves the second one $(\supseteq)$.

We first show a. Consider states $s,s^{\prime}$ and an event $e\in\mathcal{E}$
such that $s\xrightarrow{\;e\;}s^{\prime}$. By construction of $\mathcal{E}$,
there exist $e^{\prime}$, $\theta$, $\mathscr{l}^{\prime}$,
$\mathscr{a}^{\prime}$, $\mathscr{r}^{\prime}$ such that
$e=e^{\prime}(\theta,\mathscr{l}^{\prime},\mathscr{a}^{\prime},\mathscr{r}^{\prime})$.
In addition, $e$ is associated to some rule
$\mathscr{l}\xrightarrow{\mathscr{a}}\mathscr{r}\in\mathcal{R}_{\mathsf{intf}}$.
By definition of the guard associated to $e$, we have
$(\mathscr{l}^{\prime},\mathscr{a}^{\prime},\mathscr{r}^{\prime})=_{\mathsf{E}}(\mathscr{l},\mathscr{a},\mathscr{r})\theta$,
$\mathscr{l}^{\prime}\cap^{\mathsf{m}}\mathcal{F}_{\mathsf{lin}}\subseteq^{\mathsf{m}}s$,
the equality conditions $\Phi_{\mathsf{eq}}(\mathscr{a}^{\prime})$ are
satisfied, and
$s^{\prime}=\mathrm{set}(\mathscr{l}^{\prime})\cap\mathcal{F}_{\mathsf{per}}\subseteq\mathrm{set}(s)$.
By definition of the update associated to $e$, we have
$s^{\prime}=s\setminus^{\mathsf{m}}(\mathscr{l}^{\prime}\cap^{\mathsf{m}}\mathcal{F}_{\mathsf{lin}})\cup^{\mathsf{m}}\mathscr{r}^{\prime}$.
Thus by multiset rewriting,
$s\stackrel{{\scriptstyle\;\mathscr{a}^{\prime}\;}}{{\Longrightarrow}}_{\mathcal{R}_{\mathsf{intf}},\mathsf{E},\mathsf{eq}}s^{\prime}$.
Finally, by definition of $\pi$ we have $\pi(e)=\mathscr{a}^{\prime}$, which
proves a.

Let us now show b. Consider a reduction step
$s\stackrel{{\scriptstyle\;\mathscr{a}\;}}{{\Longrightarrow}}_{\mathcal{R}_{\mathsf{intf}},\mathsf{E},\mathsf{eq}}s^{\prime}$.
By definition of multiset rewriting, there exists a rule
$\mathscr{l}\xrightarrow{\mathscr{a}}\mathscr{r}\in\mathcal{R}_{\mathsf{intf}}$,
a ground instantiation $\theta$ of
$\mathrm{vars}(\mathscr{l})\cup\mathrm{vars}(\mathscr{a})\cup\mathrm{vars}(\mathscr{r})$,
and multisets of ground facts
$\mathscr{l}^{\prime},\mathscr{a}^{\prime},\mathscr{r}^{\prime}$ such that
$(\mathscr{l}^{\prime},\mathscr{a}^{\prime},\mathscr{r}^{\prime})=_{\mathsf{E}}(\mathscr{l},\mathscr{a},\mathscr{r})\theta$,
$\mathscr{l}^{\prime}\cap^{\mathsf{m}}\mathcal{F}_{\mathsf{lin}}\subseteq^{\mathsf{m}}s$,
$\mathrm{set}(\mathscr{l}^{\prime})\cap\mathcal{F}_{\mathsf{per}}\subseteq\mathrm{set}(s)$,
the equality conditions $\Phi_{\mathsf{eq}}(\mathscr{a}^{\prime})$ hold, and
$s^{\prime}=\mathrm{set}(\mathscr{l}^{\prime})\cap\mathcal{F}_{\mathsf{per}}\subseteq\mathrm{set}(s)$.

By construction of $\mathcal{R}_{\mathsf{intf}}$,
$\mathscr{l}\xrightarrow{\mathscr{a}}\mathscr{r}$ is either in
$\mathcal{R}^{\prime}_{i}$ for some $i$, in $\mathcal{R}_{\mathsf{env}}^{-}$,
or in $\mathcal{R}_{\mathsf{io}}$. In either case, there exists a parametric
event $e$ such that the family of events

$\\{e(\theta^{\prime\prime},\mathscr{l}^{\prime\prime},\mathscr{a}^{\prime\prime},\mathscr{r}^{\prime\prime})\;|\;\theta^{\prime\prime}\text{
gr. inst. of
}\mathrm{vars}(\mathscr{l})\cup\mathrm{vars}(\mathscr{a})\cup\mathrm{vars}(\mathscr{r}),\mathscr{l}^{\prime\prime},\mathscr{a}^{\prime\prime},\mathscr{r}^{\prime\prime}\text{
multisets of gr. facts}\\}$

is in $\mathcal{E}$. The three cases differ only by the event name, which is
inconsequential here.

Consider the instance
$e(\theta,\mathscr{l}^{\prime},\mathscr{a}^{\prime},\mathscr{r}^{\prime})$:
its guard is satisfied, and it updates $s$ into
$\mathrm{set}(\mathscr{l}^{\prime})\cap\mathcal{F}_{\mathsf{per}}\subseteq\mathrm{set}(s)$,
i.e. $s^{\prime}$. Hence
$s\xrightarrow{\;e(\theta,\mathscr{l}^{\prime},\mathscr{a}^{\prime},\mathscr{r}^{\prime})\;}s^{\prime}$.
Since
$\pi(e(\theta,\mathscr{l}^{\prime},\mathscr{a}^{\prime},\mathscr{r}^{\prime}))=\mathscr{a}^{\prime}$,
this proves b. ∎

From now on, we will actually slightly strengthen the guards of the protocol
events in $\mathcal{E}$, i.e. those in $\mathcal{E}^{s}_{i,\mathit{rid}}$, to
use true equality instead of equality modulo $\mathsf{E}$. This only reduces
the set of possible executions, and thus preserves the previous trace
inclusion.

###  E.5 Step 3: separating the event system into each component

We are now ready to split the event system into its components.

We will separate it into one system $\mathscr{E}^{s}_{i,\mathit{rid}}$ for
each role instance, and a system $\mathscr{E}^{e}$ for the environment. The
interface events, from $\mathcal{E}^{\mathsf{io}}$ (associated to rule in
$\mathcal{R}_{\mathsf{io}}$), will be split in two halves, one to be added to
$\mathscr{E}^{e}$, and the other to one of the
$\mathscr{E}^{s}_{i,\mathit{rid}}$.

For each role instance $(i,\mathit{rid})$ we consider the event system
$\mathscr{E}^{s}_{i,\mathit{rid}}$ containing the events in
$\mathcal{E}^{s}_{i,\mathit{rid}}$ and the associated guards and updates, as
well as events, guards and updates encoding the additional rules

$\begin{array}[]{rcl@{\quad}l}{[F_{i}(\mathit{rid},\overline{x})]}&\xrightarrow{[]}&[]&\text{for
$F\in\Sigma_{\mathsf{out}}$}\\\
{[]}&\xrightarrow{[]}&[F_{i}(\mathit{rid},\overline{x})]&\text{for
$F\in\Sigma_{\mathsf{in}}$}\\\ \end{array}$

We denote the events for these transitions $\lambda^{s}_{F,i,\mathit{rid}}$.
Formally:

  * •

if $F\in\Sigma_{\mathsf{out}}$, the guard for
$\lambda^{s}_{F,i,\mathit{rid}}(\overline{x})$ requires that the state
contains $F_{i}(\mathit{rid},\overline{x})$, and its update simply removes
that fact from the state or leaves it, depending on whether
$F\in\mathcal{F}_{\mathsf{lin}}$ or not;

  * •

if $F\in\Sigma_{\mathsf{in}}$, the guard for
$\lambda^{s}_{F,i,\mathit{rid}}(\overline{x})$ is always satisfied, and its
update adds fact $F_{i}(\mathit{rid},\overline{x})$ to the state.

We also consider the event system $\mathscr{E}^{e}$ containing the events in
$\mathcal{E}^{e}$ and the associated guards and updates, augmented with events
encoding the rules

$\begin{array}[]{rcl@{\quad}l}{[F(\overline{x})]}&\xrightarrow{[]}&[]&\text{for
$F\in\Sigma_{\mathsf{in}}^{-}$}\\\
{[\overline{F^{\prime}(\overline{x})}]}&\xrightarrow{[]}&[]&\text{for
$F=\mathsf{Setup}_{i}$ for some $i$}\\\ &&&\text{where
$\overline{F^{\prime}(\overline{x})}$ are the premises of the setup rule for
$F$}\\\ {[]}&\xrightarrow{[]}&[F(\overline{x})]&\text{for
$F\in\Sigma_{\mathsf{out}}$.}\end{array}$

We denote the events associated to these rules
$\lambda^{e}_{F,i,\mathit{rid}}(\overline{x})$ (i.e. we include one copy of
the event for each $i,\mathit{rid}$). Formally:

  * •

if $F\in\Sigma_{\mathsf{in}}^{-}$, the guard for
$\lambda^{e}_{F,i,\mathit{rid}}(\overline{x})$ requires that the state
contains $F(\overline{x})$, and its update either removes this fact from the
state or leaves it, depending on whether $F\in\mathcal{F}_{\mathsf{lin}}$ or
not;

  * •

if $F=\mathsf{Setup}_{i}$, the guard for
$\lambda^{e}_{F,i,\mathit{rid}}(\overline{x})$ requires that the state
contains $[\overline{F^{\prime}(\overline{x})}]$, and its update removes from
the state the facts in this list that are in $\mathcal{F}_{\mathsf{lin}}$;

  * •

if $F\in\Sigma_{\mathsf{out}}$, the guard for
$\lambda^{e}_{F,i,\mathit{rid}}(\overline{x})$ is always satisfied, and its
update adds $F(\overline{x})$ to the state.

We define the partial function
$\chi:(\bigcup_{i,\mathit{rid}}\mathscr{E}^{s}_{i,\mathit{rid}})\times\mathscr{E}^{e}\rightarrow\mathcal{E}$
(conflating $\mathscr{E}^{e}$ with its state space, and similarly for
$\mathscr{E}^{s}$) that synchronises labels $\lambda_{F}$, i.e.

  * •

$\chi(\lambda^{s}_{F,i,\mathit{rid}}(\overline{m}),\lambda^{e}_{F,i,\mathit{rid}}(\overline{x}))=\lambda_{F,i,\mathit{rid}}([\overline{x}\mapsto\overline{m}],\mathscr{l}^{\prime},\mathscr{a}^{\prime},\mathscr{r}^{\prime})$,
where $\mathscr{l}\xrightarrow{\mathscr{a}}\mathscr{r}$ is the rule associated
with $F$ in $\mathcal{R}_{\mathsf{io}}$, instantiated with $\mathit{rid}$,
$\overline{x}$ are its variables, and
$\mathscr{l}^{\prime}\xrightarrow{\mathscr{a}^{\prime}}\mathscr{r}^{\prime}$
is its instantiation with $\overline{m}$;

  * •

$\chi(\mathsf{skip},e)=e$ when $e$ is not of the form
$\lambda^{s}_{F,i,\mathit{rid}}$;

  * •

$\chi(e,\mathsf{skip})=e$ when $e$ is not of the form
$\lambda^{e}_{F,i,\mathit{rid}}$.

  * •

$\chi(e,e^{\prime})$ is undefined in all other cases.

We introduce two composition operators. $|||$ is parallel composition, i.e.
the state space of $A|||B$ is the product of those of $A$ and $B$, and its
events are $e_{A}$ updating state $(s_{A},s_{B})$ to $(s_{A}^{\prime},s_{B})$
if $e_{A}$ updates $s_{A}$ to $s_{A}^{\prime}$ in $A$, and similarly for
$e_{B}$ in $B$. ${||}_{\chi}$ is synchronising composition, and is defined
similarly: the state space of $A||_{\chi}B$ is the product of those of $A$ and
$B$, and its events are $\chi(e_{A},e_{B})$, updating state $(s_{A},s_{B})$ to
$(s_{A}^{\prime},s_{B}^{\prime})$, if $e_{A}$ updates $s_{A}$ to
$s_{A}^{\prime}$ in $A$, and similarly for $e_{B}$ in $B$.

We can then state the following composition lemma, which corresponds to Lemma
2 in Section 3.2.2 (when chaining it by transitivity with Lemma 4).

######  Lemma 5.

$\mathrm{Tr}(({|||}_{i,\mathit{rid}}\mathscr{E}^{s}_{i,\mathit{rid}}){||}_{\chi}\mathscr{E}^{e})\subseteq\mathrm{Tr}(\mathscr{E}).$

###### Proof.

We prove this lemma by establishing a refinement with a simulation relation
$\mathscr{R}$ between abstract states (from $\mathscr{E}$) and concrete ones
(from
$({|||}_{i}\mathscr{E}^{s}_{i,\mathit{rid}}){||}_{\chi}\mathscr{E}^{e}$). The
concrete states are of the form $((s_{i,\mathit{rid}})_{1\leq i\leq n,\text{
for each }\mathit{rid}},s_{e})$, i.e. they are composed of one multiset of
facts for each $i,\mathit{rid}$, and one for the environment.

The refinement relation we use is defined by $(s,s^{\prime})\in\mathscr{R}$
iff
$s=(\cup^{\mathsf{m}}_{i,\mathit{rid}}s^{\prime}_{i,\mathit{rid}})\cup^{\mathsf{m}}s^{\prime}_{e}$,
where $s^{\prime}=((s^{\prime}_{i,\mathit{rid}}),s^{\prime}_{e})$.

For better legibility we will denote
$\mathscr{E}^{\prime}=({|||}_{i}\mathscr{E}^{s}_{i,\mathit{rid}}){||}_{\chi}\mathscr{E}^{e}$
the composed system, and $\xrightarrow{\;\cdot\;}_{\mathscr{E}^{\prime}}$,
$\xrightarrow{\;\cdot\;}_{\mathscr{E}}$,
$\xrightarrow{\;\cdot\;}_{i,\mathit{rid}}$, $\xrightarrow{\;\cdot\;}_{e}$ the
transition relations defined respectively by $\mathscr{E}^{\prime}$,
$\mathscr{E}$, $\mathscr{E}^{s}_{i,\mathit{rid}}$ and $\mathscr{E}^{e}$.

It is clear that the initial states of $\mathscr{E}^{\prime}$ and
$\mathscr{E}$ are related:
$(((\emptyset,\dots,\emptyset),\emptyset),\emptyset)\in\mathscr{R}$. We now
show that for all states $(s_{1},s^{\prime}_{1})\in\mathscr{R}$, for all
transition steps
$s^{\prime}_{1}\xrightarrow{\;e\;}_{\mathscr{E}^{\prime}}s^{\prime}_{2}$ there
exists a transition $s_{1}\xrightarrow{\;e\;}_{\mathscr{E}}s_{2}$ such that
$(s_{2},s^{\prime}_{2})\in\mathscr{R}$. We will denote
$s^{\prime}_{j}=((s^{\prime}_{j,i,\mathit{rid}})_{1\leq i\leq n,\text{ for
each }\mathit{rid}},s^{\prime}_{j,e})$ for $j\in\\{1,2\\}$.

Following the definition of $\chi$, we can distinguish several cases for the
transition step
$s^{\prime}_{1}\xrightarrow{\;e\;}_{\mathscr{E}^{\prime}}s^{\prime}_{2}$.

  * •

if $e=\chi(e^{\prime},\mathsf{skip})$ for some
$e^{\prime}\in\mathcal{E}^{s}_{i,\mathit{rid}}$: then $e^{\prime}=e$, and by
definition of $||_{\chi}$ and $|||$, since
$s^{\prime}_{1}\xrightarrow{\;e\;}_{\mathscr{E}^{\prime}}s^{\prime}_{2}$, we
have
$s^{\prime}_{1,i,\mathit{rid}}\xrightarrow{\;e\;}_{i,\mathit{rid}}s^{\prime}_{2,i,\mathit{rid}}$,
$s^{\prime}_{2,j,\mathit{rid}^{\prime}}=s^{\prime}_{1,j,\mathit{rid}^{\prime}}$
for all $(j,\mathit{rid}^{\prime})\neq(i,\mathit{rid})$, and
$s^{\prime}_{2,e}=s^{\prime}_{1,e}$.

By definition of $\mathscr{E}^{s}_{i,\mathit{rid}}$, the guard and update of
$e$ in that system are the same as in $\mathscr{E}$. In addition, since
$(s^{\prime}_{1},s_{1})\in\mathscr{R}$, we have
$s^{\prime}_{1,i,\mathit{rid}}\subseteq^{\mathsf{m}}s_{1}$. It is immediate
from the form of the guard in $\mathscr{E}$ that it is stable by
supermultiset, and thus holds for $s_{1}$. It is also clear from the form of
the update in $\mathscr{E}$ that applying it to the whole state is exactly the
same as applying it to a submultiset of the state that satisfies the guard,
here $s^{\prime}_{1,i,\mathit{rid}}$, and leaving the rest of the state
untouched.

Therefore, we have

$s_{1}=(\cup^{\mathsf{m}}_{j,\mathit{rid}^{\prime}}s^{\prime}_{1,j,\mathit{rid}^{\prime}})\cup^{\mathsf{m}}s^{\prime}_{1,e}\;\xrightarrow{\;e\;}_{\mathscr{E}}\;(\cup^{\mathsf{m}}_{(j,\mathit{rid}^{\prime})\neq(i,\mathit{rid})}s^{\prime}_{1,j,\mathit{rid}^{\prime}})\cup^{\mathsf{m}}s^{\prime}_{2,i,\mathit{rid}}\cup^{\mathsf{m}}s^{\prime}_{1,e}.$

As noted earlier, we have $s^{\prime}_{2,e}=s^{\prime}_{1,e}$ and
$s^{\prime}_{2,j,\mathit{rid}^{\prime}}=s^{\prime}_{1,j,\mathit{rid}^{\prime}}$
for all $(j,\mathit{rid}^{\prime})\neq(i,\mathit{rid})$, hence
$(s^{\prime}_{2},(\cup^{\mathsf{m}}_{(j,\mathit{rid}^{\prime})\neq(i,\mathit{rid})}s^{\prime}_{1,j,\mathit{rid}^{\prime}})\cup^{\mathsf{m}}s^{\prime}_{2,i,\mathit{rid}}\cup^{\mathsf{m}}s^{\prime}_{1,e})\in\mathscr{R}$,
which concludes the proof in this case.

  * •

if $e=\chi(\mathsf{skip},e^{\prime})$ for some $e^{\prime}\in\mathcal{E}^{e}$:
this case is similar to the previous one.

  * •

The remaining case is the synchronisation case, where
$e=\chi(\lambda^{s}_{F,i,\mathit{rid}}(\overline{m}),\lambda^{e}_{F,i,\mathit{rid}}(\overline{m}))$
for some $F,i,\mathit{rid},\overline{m}$.

Then
$e=\lambda_{F,i,\mathit{rid}}(\theta_{m},\mathscr{l}^{\prime},\mathscr{a}^{\prime},\mathscr{r}^{\prime})$
where $\theta_{m}=[\overline{x}\mapsto\overline{m}]$,
$\mathscr{l}\xrightarrow{\mathscr{a}}\mathscr{r}$ is the rule associated with
$F$ in $\mathcal{R}_{\mathsf{io}}$, instantiated with $\mathit{rid}$,
$\overline{x}$ are its variables, and
$\mathscr{l}^{\prime}\xrightarrow{\mathscr{a}^{\prime}}\mathscr{r}^{\prime}$
is its instantiation with $\theta_{m}$.

By definition of $||_{\chi}$ and $|||$, since
$s^{\prime}_{1}\xrightarrow{\;e\;}_{\mathscr{E}^{\prime}}s^{\prime}_{2}$, we
have
$s^{\prime}_{1,i,\mathit{rid}}\xrightarrow{\;\lambda^{s}_{F,i,\mathit{rid}}(\overline{m})\;}_{i,\mathit{rid}}s^{\prime}_{2,i,\mathit{rid}}$,
$s^{\prime}_{1,e}\xrightarrow{\;e^{e,in}(m)\;}_{e}s^{\prime}_{2,e}$, and
$s^{\prime}_{2,j,\mathit{rid}^{\prime}}=s^{\prime}_{1,j,\mathit{rid}^{\prime}}$
for all $(j,\mathit{rid}^{\prime})\neq(i,\mathit{rid})$.

We now need to distinguish the cases where $F\in\Sigma_{\mathsf{in}}^{-}$,
$F=\mathit{Setup}_{i}$, and $F\in\Sigma_{\mathsf{out}}$. We write the proof
for the case $F\in\Sigma_{\mathsf{out}}$ and $F\in\mathcal{F}_{\mathsf{lin}}$,
as the other cases are similar.

We then have $\mathscr{l}^{\prime}=\\{|F_{i}(\mathit{rid},\overline{m})|\\}$,
$\mathscr{a}^{\prime}=[]$, and $\mathscr{r}^{\prime}=\\{|F(\overline{m})|\\}$.

By definition of $\lambda^{s}_{F,i,\mathit{rid}}(\overline{m})$, we have
$F_{i}(\mathit{rid},\overline{m})\in$
$s^{\prime}_{2,i,\mathit{rid}}=s^{\prime}_{1,i,\mathit{rid}}$, and
$s^{\prime}_{1,i,\mathit{rid}}\setminus^{\mathsf{m}}\\{|F_{i}(\mathit{rid},\overline{m})|\\}$.

By definition of $\lambda^{e}_{F,i,\mathit{rid}}(\overline{m})$, we have
$s^{\prime}_{2,e}=s^{\prime}_{1,e}\cup^{\mathsf{m}}\\{|F(\overline{m})|\\}$.
Therefore,
$s_{1}=(\cup^{\mathsf{m}}_{k,\mathit{rid}^{\prime}}s^{\prime}_{1,k,\mathit{rid}^{\prime}})\cup^{\mathsf{m}}s^{\prime}_{1,e}$
satisfies the guard of the event
$\lambda_{F,i,\mathit{rid}}(\theta_{m},\\{|F_{i}(\mathit{rid},\overline{m})|\\},\emptyset,\\{|F(\overline{m})|\\})$
associated with rule
$[F_{i}(\mathit{rid},\overline{m})]\rightarrow[F(\overline{m})]$ in
$\mathscr{E}$.

Hence we have

$\begin{array}[]{l}s_{1}\;\xrightarrow{\;\lambda_{F,i,\mathit{rid}}(\theta_{m},\\{|F_{i}(\mathit{rid},\overline{m})|\\},\emptyset,\\{|F(\overline{m})|\\})\;}_{\mathscr{E}}\\\
\qquad\qquad((\cup^{\mathsf{m}}_{(k,\mathit{rid}^{\prime})}s^{\prime}_{1,k,\mathit{rid}^{\prime}})\cup^{\mathsf{m}}s^{\prime}_{1,e}\setminus^{\mathsf{m}}\\{|F_{i}(\mathit{rid},\overline{m})|\\})\cup^{\mathsf{m}}\\{|F(\overline{m})|\\}.\end{array}$

As noted earlier, we have
$s^{\prime}_{2,i,\mathit{rid}}=s^{\prime}_{1,i,\mathit{rid}}\cup^{\mathsf{m}}\\{|F(\overline{m})|\\}$,
$s^{\prime}_{2,e}=s^{\prime}_{1,e}\setminus^{\mathsf{m}}\\{|F_{i}(\mathit{rid},\overline{m})|\\}$,
and
$s^{\prime}_{2,k,\mathit{rid}^{\prime}}=s^{\prime}_{1,k,\mathit{rid}^{\prime}}$
for all $(k,\mathit{rid}^{\prime})\neq(i,\mathit{rid})$. Thus
$(s^{\prime}_{2},((\cup^{\mathsf{m}}_{(k,\mathit{rid}^{\prime})}s^{\prime}_{1,k,\mathit{rid}^{\prime}})\cup^{\mathsf{m}}s^{\prime}_{1,e}\setminus^{\mathsf{m}}\\{|F_{i}(\mathit{rid},\overline{m})|\\})\cup^{\mathsf{m}}\\{|F(\overline{m})|\\})\in\mathscr{R}$,
which concludes the proof in this case.

∎


# Non-adiabatic dynamics in Rydberg gases with random atom positions

Ritesh Pant  Department of Physics, Indian Institute of Science Education and
Research, Bhopal, Madhya Pradesh 462 066, India  Rajat Agrawal  Max Planck
Institute for the Physics of Complex Systems, Nöthnitzer Strasse 38, 01187
Dresden, Germany  Sebastian Wüster  Department of Physics, Indian Institute of
Science Education and Research, Bhopal, Madhya Pradesh 462 066, India  Jan-
Michael Rost  Max Planck Institute for the Physics of Complex Systems,
Nöthnitzer Strasse 38, 01187 Dresden, Germany

###### Abstract

Assemblies of highly excited Rydberg atoms in an ultracold gas can be set into
motion by a combination of van-der-Waals and resonant dipole-dipole
interactions. Thereby, the collective electronic Rydberg state might change
due to non-adiabatic transitions, in particular if the configuration
encounters a conical interaction. For the experimentally most accessible
scenario, in which the Rydberg atoms are initially randomly excited in a
three-dimensional bulk gas under blockade conditions, we numerically show that
non-adiabatic transitions can be common when starting from the most energetic
repulsive BO-surface. We outline how this state can be selectively excited
using a microwave resonance, and demonstrate a regime where almost all
collisional ionization of Rydberg atoms can be traced back to a prior non-
adiabatic transition. Since Rydberg ionisation is relatively straightforward
to detect, the excitation and measurement scheme considered here renders non-
adiabatic effects in Rydberg motion easier to demonstrate experimentally than
in scenarios considered previously.

##  I Introduction

Collections of a small number of highly excited Rydberg atoms in a cold gas or
even BEC are nowadays routinely created in laboratories. The motion of these
atoms can often be neglected on the time scale of experiments, justifying the
so-called frozen gas approximation. However, under generic circumstances,
namely for lighter atoms and initial close proximity, they are easily set into
motion on time-scales of interest, by non-resonant van-der Waals (vdW) or
resonant dipole-dipole (DD) interactions Gensemer and Gould (1998); Li et al.
(2005); Fioretti et al. (1999); Overstreet et al. (2007); Robicheaux et al.
(2004a). The motion of a randomly distributed assembly of Rydberg atoms in
three dimensions (3D) has been studied in experiments, however, so far mainly
due to interactions involving a single Rydberg state at a time Viteau et al.
(2008); Amthor et al. (2007a, b); Celistrino Teixeira et al. (2015);
Thaicharoen et al. (2015), permanent dipoles Gonçalves et al. (2016);
Thaicharoen et al. (2016) or transition dipole-dipole interactions of two
Rydberg atoms Park et al. (2011a, b).

Figure 1:  Sketch of a randomly distributed assembly of Rydberg atoms
(spherical balls) in a 3D bulk gas (gray shade) at locations
$\mathbf{R}_{1},....,\mathbf{R}_{6}$. $R_{bl}$ is the blockade radius shown by
the smaller transparent sphere, representing the initial minimal distance.
After passing through a conical interaction (double cones) or region of strong
non-adiabatic coupling, atomic repulsion can be overcome and the collision of
two Rydberg atoms (here $4$ and $5$) results in ionization.

More complex dynamics arises when transition dipole-dipole interactions
involve a large number of atoms, giving rise to collective exciton states with
a delocalized excitation Ates et al. (2008); Wüster and Rost (2018). While a
single Rydberg dimer possesses only strongly repulsive or attractive
electronic states, the multi-atom system has states in which the resonant DD
contribution vanishes for the closest pair of atoms. If the remaining
repulsive van-der-Waals interactions are too weak to counteract kinetic energy
initially gained from dipole-dipole repulsion, atoms paired in these states
can collisionally ionize if they hit a neighboring Rydberg atom.

An additional feature of collective dipole-dipole interactions are conical
intersections (CIs) between adjacent electronic states of the multi-atom
Rydberg assembly Wüster et al. (2011). Near a conical intersection, non-
adiabatic transition necessarily become likely. Even if initialised in a state
in which nearest atoms should repel, non-adiabatic transitions or passages
through conical intersections can transfer their electronic state to a non-
repelling one. After that transfer, Rydberg atoms can ionize. We demonstrate
that, for a suitable choice of parameters, most ionization events can be
traced back to at least one non-adiabatic transition implying conversely that
ionization is an easily accessible experimental signature for a non-adiabatic
transition. In comparison to earlier proposals to investigate conical
intersections in Rydberg systems Wüster et al. (2011); Leonhardt et al. (2014,
2016, 2017), the scenario discussed in this article lifts the challenges of
constraining the motion of atoms through trapping, tightly localizing the
Rydberg excitation and high resolution Rydberg position measurements.

Nonadiabatic effects due to conical intersections play a key role in many
quantum chemical processes Dantus and Zewail (2004) such as photochemistry of
vision Hahn and Stock (2000) or DNA protection from UV radiation damage Perun
et al. (2005). While computational methods can nowadays provide an impressive
level of detail for multi-dimensional nuclear wavefunctions of molecules
Burghardt et al. (2008); Worth et al. (2008), such detail may be hard to
achieve when interrogating molecules experimentally. More detail may be
accessible, when studying dynamics around conical intersections with cold
atoms or molecules Wallis et al. (2009); Moiseyev et al. (2008); Zhu et al.
(2007); Larson and Sjöqvist (2009), Rydberg atoms Wüster et al. (2011); Wüster
and Rost (2018) or ions Gambetta et al. (2021).

This article is organized as follows: In section II, we introduce the model
for collective dipole-dipole interactions of Rydberg atoms, the quantum-
classical propagation scheme employed and our phenomenological model of the
excitation sequence. In section III we explore non-adiabatic dynamics with
individual trajectories of the classical motion of Rydberg atoms, to clearly
connect ionisation with non-adiabatic transitions. Finally, in section IV, we
portray the dynamics in the trajectory averaged energy spectrum of the system.

##  II Dipole-dipole interactions in 3D Rydberg Gases

We consider an assembly of $N$ Lithium Rydberg atoms each with mass $M\approx
11000$ au. and principal quantum number $\nu$. All atoms can move freely in
3D, with their collective positions described by the $3N$-component vector
$\mathbf{R}=(\mathbf{R}_{1},\cdots,\mathbf{R}_{N})^{T}$, where
$\mathbf{R}_{k}$ is the position of atom number $k$. We are interested in the
joint effect of DD and vdW interactions. Hence, besides constraining $\nu$, we
consider angular momentum states $|\,{s(l=0)}\,\rangle$ and
$|\,{p(l=1),m}\,\rangle$. For scenarios with only a single Rydberg atom in a
$|\,{p}\,\rangle$ state, the collective electronic basis can then be written
as $\\{|\,{\pi_{n}(m)}\,\rangle\\}$, where,

$\displaystyle|\,{\pi_{n}(m)}\,\rangle=|\,{s...(p,m)...s}\,\rangle,$ (1)

represents the state where the $n$’th atom carries the p-excitation with
magnetic quantum number $m$, and all other atoms are in the $|\,{s}\,\rangle$
state. We thus neglect spin-orbit coupling, a reasonable approximation for
light atoms such as Lithium.

The resulting Hamiltonian for our system reads

$\displaystyle\hat{H}=-\frac{\hbar^{2}}{2M}\nabla_{\mathbf{R}}^{2}+\hat{H}_{el}(\mathbf{R}),$
(2)

where the first term accounts for the kinetic energy of the Rydberg atoms and
$\hat{H}_{el}(\mathbf{R})={\hat{H}}_{\mbox{\\!\\! \scriptsize
dd}}(\mathbf{R})+{\hat{H}}_{\mbox{\\!\\! \scriptsize vdw}}(\mathbf{R})$, with
the resonant dipole-dipole interactions

$\displaystyle\hat{H}_{dd}(\mathbf{R})=\sum_{\stackrel{{\scriptstyle
n,n^{\prime}=1}}{{m,m^{\prime}}}}^{N}V^{(dd)}_{mm^{\prime}}(\mathbf{R}_{n,n^{\prime}})|\,{\pi_{n}(m)}\,\rangle\langle\,{\pi_{n^{\prime}}(m^{\prime})}\,|\,.$
(3)

Here, $V^{(dd)}_{mm^{\prime}}(\mathbf{R}_{n,n^{\prime}})$ are the matrix
elements for the dipole-dipole interactions between atoms $n$ and
$n^{\prime}$. They depend on
$\mathbf{R}_{nn^{\prime}}{=}\mathbf{R}_{n}{-}\mathbf{R}_{n^{\prime}}$ and are
explicitly given by Robicheaux et al. (2004b)

$\displaystyle V^{(dd)}_{mm^{\prime}}(\mathbf{R}_{nn^{\prime}})$
$\displaystyle=-\sqrt{\frac{8\pi}{3}}\frac{\mu^{2}}{4\pi\epsilon_{0}{R}_{nn^{\prime}}^{3}}(-1)^{m^{\prime}}$
(4) $\displaystyle\begin{pmatrix}1&1&2\\\
m&-m^{\prime}&m^{\prime}-m\end{pmatrix}{Y}_{2,m^{\prime}-m}(\theta_{nn^{\prime}},\phi_{nn^{\prime}}),$

where $R_{nn^{\prime}}=|\mathbf{R}_{nn^{\prime}}|$, $\theta_{nn^{\prime}}$ and
$\phi_{nn^{\prime}}$ are the polar angle and azimuthal angle of the inter
atomic distance vector, respectively, as shown in Fig. 1, and the six numbers
in the parentheses denote the Wigner $3-j$ symbol. Note that resonant dipole-
dipole interactions are in general anisotropic due to the dependence on
$\theta$ and $\phi$ in (4) and mix the different azimuthal sublevels $m$. The
anisotropy and the azimuthal state mixing could be suppressed using Zeeman
shifts Leonhardt et al. (2016), however, here we are interested in the
pristine scenario.

The term ${\hat{H}}_{\mbox{\\!\\! \scriptsize vdw}}(\mathbf{R})$ in
$\hat{H}_{el}(\mathbf{R})$ pertains to the non-resonant van-der-Waals
interaction

$\displaystyle\hat{H}_{vdw}(\mathbf{R})=-\frac{1}{2}\sum_{n,n^{\prime}=1}^{N}\frac{C_{6}}{R_{nn^{\prime}}^{6}}\mathbb{I},$
(5)

where $\mathbb{I}$ is the unit operator in the electronic space and $C_{6}$ is
the dispersion coefficient which characterizes the strength of van-der-Waals
interactions dependent on the principal quantum number $\nu$. Throughout this
article, we shall assume atoms in $\nu=80$ and hence $C_{6}=-1.7\times
10^{22}$ au, from Singer et al. (2005) and $\mu=4096$ au in (4).

A full fledged quantum mechanical simulation of the time dependent Schrödinger
equation for the Hamiltonian defined in Eq. (2) is computationally not
possible for useful atom numbers $N$. Hence we employ Tully’s surface hopping
algorithm Tully (1990); Möbius et al. (2011a), a quantum-classical method in
which the motion of the Rydberg atoms is simulated classically using Newton’s
equation of motion,

$\displaystyle M\frac{\partial^{2}\mathbf{R}}{\partial
t^{2}}=-\nabla_{\mathbf{R}}U_{s}(\mathbf{R}(t)),$ (6)

where $s$ is the index of the Born-Oppenheimer (BO) surface
$U_{k=s}(\mathbf{R}(t))$ on which the Rydberg system is presently evolving.
The surfaces follow from the eigenvalue equation

$\displaystyle\hat{H}_{el}(\mathbf{R})|\,{\varphi_{k}(\mathbf{R})}\,\rangle=U_{k}(\mathbf{R})|\,{\varphi_{k}(\mathbf{R})}\,\rangle,$
(7)

where we order eigenstates according to increasing energy with increasing
index $k$.

In contrast to the positions, the electronic state of the Rydberg assembly
$|\,{\psi(t)}\,\rangle=\sum_{nm}{c}_{nm}(t)|\,{\pi_{n}(m)}\,\rangle$ is
evolved quantum mechanically with Schrödinger’s equation

$\displaystyle i\hbar\frac{\partial}{\partial
t}{c}_{nm}(t)=\sum_{n^{\prime}m^{\prime}}\langle\,{\pi_{n}(m)}\,|\hat{H}_{el}(\mathbf{R})|\,{\pi_{n^{\prime}}(m^{\prime})}\,\rangle{c}_{n^{\prime}m^{\prime}}(t).$
(8)

It is instructive to also express (8) in the adiabatic basis
$|\,{\psi(t)}\,\rangle=\sum_{k}\tilde{c}_{k}(t)|\,{\varphi_{k}{(\mathbf{R})}}\,\rangle$
formed by solutions of (7). In terms of this basis the TDSE reads

$\displaystyle i\hbar\frac{\partial}{\partial
t}\tilde{c}_{k}(t)=U_{k}(\textbf{R}(t))\tilde{c}_{k}(t)-i\hbar\sum_{l}d_{kl}(t)\tilde{c}_{l}(t),$
(9)

with non-adiabatic coupling vectors

$\displaystyle
d_{kl}\approx-\frac{1}{M}\langle\,{\varphi_{k}(\textbf{R})}\,|\boldsymbol{\nabla}_{\mathbf{R}}|\,{\varphi_{l}(\textbf{R})}\,\rangle\cdot\frac{\partial\mathbf{R}}{\partial
t}.$ (10)

The latter couple the different BO surfaces, which is implemented into the
motional dynamics (6) of Tully’s method by allowing stochastic jumps of the
index $s\rightarrow s^{\prime}$ with a probability set by $d_{ss^{\prime}}$.
The adiabatic and the diabatic coefficients are connected by the relation
$\tilde{c}_{k}=\sum_{nm}c_{nm}\mbox{$\langle\,{\varphi_{k}{(\mathbf{R})}}\,|\,{\pi_{n}(m)}\,\rangle$}$.
Our simulations employ Tully’s method with Eq. (8) coupled to Eq. (6), but one
can refer to Eq. (9) for understanding non-adiabatic transitions.

###  II.1 Excitation process and blockade

The initial excitation of Rydberg atoms to states involving
$|\,{\pi_{n}(m)}\,\rangle$ is a two step process. Firstly, within a bulk
ultra-cold gas, ground state atoms are excited to the Rydberg state
$|\,{s}\,\rangle$, typically using a two-photon excitation Löw et al. (2012).
Due to the strong vdW interactions between Rydberg atoms in the state
$|\,{s}\,\rangle$, this step is affected by the dipole-blockade, which
prohibits the excitation of more than one atom within a sphere with blockade
radius $R_{bl}$. We estimate $R_{bl}$ as the distance at which the strength of
van der Waals interactions becomes equal to the broadened linewidth of a laser
with Rabi frequency ${\Omega}_{\mbox{\\!\\! \scriptsize las}}$ Lukin et al.
(2001); Urban et al. (2009), resulting in

$\displaystyle R_{bl}=\left(\frac{|C_{6}|}{{\Omega}_{\mbox{\\!\\! \scriptsize
las}}}\right)^{1/6}\,.$ (11)

For our simulation we assume ${\Omega}_{\mbox{\\!\\! \scriptsize
las}}/(2\pi)\approx 60$ MHz, which for $\nu=80$ results in $R_{bl}=5.9$ $\mu
m$. The bulk excitation and blockade are then phenomenologically taken into
account by drawing random positions from a sphere of radius $R=4R_{bl}$ in 3D,
and discarding those with $R_{nm}<R_{bl}$ for any pair of Rydberg atoms. A
more sophisticated approach could model the excitation process using classical
rate equations Ates et al. (2007). After completing this first step of the
process, we have an assembly of $N$ Rydberg atoms all in the state
$|\,{s}\,\rangle$ (hence in a many-body state $|\,{s..s..}\,\rangle$) at
random positions ${\mathbf{R}}_{\mbox{\\!\\! \scriptsize ini}}$ consistent
with the excitation blockade.

In the second step we induce a $p$-excitation to enable resonant dipole-dipole
interactions with a near resonant microwave pulse to
$|\,{\pi_{n}(m)}\,\rangle$, linearly polarized along the quantisation axis.
The corresponding Hamiltonian reads

$\displaystyle\hat{H}_{mw}$
$\displaystyle=\sum_{n}\frac{\Omega}{2}\Big{(}|\,{\pi_{n}(0)}\,\rangle\langle\,{s}\,|+\mbox{c.c.}\Big{)}$
$\displaystyle-\sum_{n}\Delta|\,{\pi_{n}(0)}\,\rangle\langle\,{\pi_{n}(0)}\,|,$
(12)

where $\Omega$ is the Rabi-frequency of the microwave and $\Delta$ its
detuning from the bare $sp$ transition. By this detuning, it is possible to
selectively excite a chosen exciton state $|\,{\varphi_{k}}\,\rangle$ in (7),
while avoiding more than one $p$-excitation Möbius et al. (2011b).

In practice, after atoms have been excited to Rydberg $s$-states at random
initial positions ${\mathbf{R}}_{\mbox{\\!\\! \scriptsize ini}}$ as discussed
above, the relative excitation probability $P_{r}(k)$ of state
$|\,{\varphi_{k}({\mathbf{R}}_{\mbox{\\!\\! \scriptsize ini}})}\,\rangle$ will
depend on two factors: (i) The transition matrix element between
$|\,{s..s..}\,\rangle$ and $|\,{\varphi_{k}({\mathbf{R}}_{\mbox{\\!\\!
\scriptsize ini}})}\,\rangle$, which depends on the microwave polarisation
direction and (ii) the microwave frequency (detuning). We incorporate both
effects phenomenologically in Tully’s algorithm by randomly starting the
simulation in exciton state $k$ with relative probability

$\displaystyle P_{r}(k)={\cal
N}e^{-\frac{(U_{k}-\Delta)^{2}}{2\sigma_{U}^{2}}}\tilde{P}_{r}(k)\,,$ (13)

where $U_{k}$ are the exciton energies defined in Eq. (7), $\Delta$ is the
microwave detuning, $\sigma_{U}$ is the microwave linewidth and
$\tilde{P}_{r}(k)$ is a polarisation dependent factor, discussed in appendix
A, that takes into account the matrix element. The normalisation factor ${\cal
N}$ ensures $\sum_{k}P_{r}(k)=1$, and trajectories with
$|U_{k}-\Delta|>2\sigma_{U}$ for all $k$ are discarded. Importantly,
$P_{r}(k)$ contains a twofold dependence on the initial positions of Rydberg
atoms after they have been excited to $|\,{s..s..}\,\rangle$: Through the
exciton energies $U_{k}$ and the interplay of microwave polarisation and
locations encoded in $\tilde{P}_{r}(k)$.

##  III Nonadiabatic dynamics from random initial positions

We are now in a position to study the motional dynamics of $N=6$ Rydberg
atoms, starting from initial locations ${\mathbf{R}}_{\mbox{\\!\\! \scriptsize
ini}}$ as discussed in section II.1 to explore how motion depends on the
choice of the initially excited repulsive BO surface $k$ defined in Eq. (7).
Such a configuration is illustrated in Fig. 2(a), where the colored spheres
represent the initial positions of Rydberg atoms. A single realization of the
time evolution of atomic positions when the system is prepared in the highest
energy repulsive state (i.e. $k=3N=18$) is shown by the solid lines in 3D with
the projection of trajectories onto the XY plane indicated by the dotted
lines. Fig. 2(b) shows the time evolution of all the electronic energy
surfaces $U_{k}(\mathbf{R}(t))$ on the left y-axis, together with the minimum
distance ${d}_{\mbox{\\!\\! \scriptsize min}}=\mbox{min}_{nm}R_{nm}$ between
the atoms, shown as thick grey line using the right y-axis. We have selected a
trajectory without non-adiabatic transition, staying on the highest energy
repulsive surface. Even when the initially accelerated atoms now encounter new
collision partners, which happens around $t\approx 5$ $\mu$s and causes
${d}_{\mbox{\\!\\! \scriptsize min}}$ to exhibit a local minimum, the
repulsion prevents a close encounter with ionisation.

Figure 2:  Electronic and motional Rydberg dynamics for the system prepared in
the highest energy electronic state. (a,b) Trajectory without non-adiabatic
transition. (c,d) Trajectory with non-adiabatic transition. (a) Initial
configuration (colored balls) and trajectories (solid lines) of the atomic
positions $\mathbf{R}_{k}(t)$. Red circles and blue dashed lines show the
projection of initial positions and trajectories onto the XY plane. (b) Time
evolution of potential energies $U_{k}(\mathbf{R}(t))$ and the minimum
distance ${d}_{\mbox{\\!\\! \scriptsize min}}$ between atoms (thick gray line,
right axis) without non-adiabatic coupling. ${d}_{\mbox{\\!\\! \scriptsize
ion}}$ is the ionization distance defined in Eq. (14) (gray dotted line). (c)
Adiabatic populations on the four highest energy repulsive surfaces, showing
non-adiabatic dynamics. (d) Time evolution of potential energies
$U_{k}(\mathbf{R}(t))$ similar to (b). The presently propagated surface $s$ in
Eq. (6) is shown as red-dashed line, and the three highest potential energies
and ${d}_{\mbox{\\!\\! \scriptsize ion}}$ are color coded as in (c).

A qualitatively different trajectory is shown in panel (c,d), where the system
undergoes a sequence of non-adiabatic transitions from the highest energy
repulsive surface to the surface with index $k=15$ as shown by the adiabatic
populations in Fig. 2(c) and the red dashed lines in Fig. 2 (d). The
transitions are due to significant non-adiabatic coupling terms $d_{kl}$ in
Eq. (9), usually when adjacent BO surfaces approach each other closely in
energy. We find that on the surface $k=15$, atoms no longer repel, hence the
the minimal distance ${d}_{\mbox{\\!\\! \scriptsize min}}$ decreases
continuously after $\approx 2\mu$s when two Rydberg atoms encounter one
another. If that happens, they would typically ionise, which is
phenomenologically modelled by declaring atoms collisionally ionized when they
come closer than an ionisation distance $d_{\rm ion}$ where the simulation is
aborted, as shown in panels (c,d). We take $d_{\rm ion}$ as the distance below
which the Rydberg energy spectra become dense when taking all electronic
states into account. For such close distances, our effective state model based
solely on $|\,{s}\,\rangle$ and $|\,{p}\,\rangle$ would break down. A rough
estimate of $d_{\rm ion}$ is provided by the formula Wüster and Rost (2018)

$\displaystyle{d}_{\mbox{\\!\\! \scriptsize
ion}}(n)=2\left(\frac{\mu^{2}n^{3}}{\Delta E_{pd}(n)}\right)^{1/3},$ (14)

where $\Delta E_{pd}$ is the energy difference between $|\,{p}\,\rangle$ and
the nearest Rydberg state not included in the model, $|\,{d(l=2)}\,\rangle$.
For the example shown in Fig. 2, the non-adiabatic transition therefore
ultimately leads to ionization of the Rydberg atoms after $t=4$ $\mu s$, much
earlier than the lifetime $\tau\approx 50$ $\mu$s of our $6$-atom system foo ;
Wüster and Rost (2018).

Next we show, that qualitatively similar dynamics can be found when the
Rydberg assembly is initialised on the next few less energetic energy
surfaces, starting in Fig. 3 from $k=17$. The figure illustrates the atomic
dynamics up to the ionisation time, in (a) together with the time evolution of
the electronic energy eigenstates and in (b,d) with the minimum distance
between atoms. We see in Fig. 3 (c,d) that due to the non-adiabatic coupling
the system can quickly jump from surface $k=17$ to $k=15$, where it is later
ionized. To underscore the need for non-adiabatic transitions, we also show in
Fig. 3 (b) the time evolution of eigenstates and minimal distance when non-
adiabatic jumps of the surface index $s$ in Eq. (6) are disabled, but using
the same initial configuration as in (c,d). As a consequence, the system
remains on the surface $k=17$, maintaining repulsive dynamics without
ionization.

Figure 3:  The same as Fig. 2, but starting from the the second most energetic
electronic eigenstate $k=17$, instead of the highest energy one, $k=18$.

The scenario is qualitatively similar when starting on the surface $k=16$. In
all cases, the first surface for which repulsion is lost and the Rydberg atoms
can ionize is $k=15$ for $N=6$. Consequently, we find that when starting on
$k=15$, ionisation is possible even without a prior non-adiabatic transition.
This is not the case from any of the higher surfaces.

Our inspection of single trajectories starting on the three highest energy
surfaces with indices $k=16,17,18$ has revealed that ionization of Rydberg
atoms must be preceded by at least one non-adiabatic transition. Therefore,
the observation of collisional ionization of Rydberg atoms after initialising
the system repulsively can be used as a signature of non-adiabatic transitions
in the experiment.

##  IV Averaged dynamics

The single trajectory simulations in section III from selected electronic
states provide a more detailed picture of the dynamics, but they would not be
individually experimentally accessible. Instead one has to average over many
repetitions of an experiment and address exciton states through the microwave
detuning, corresponding to multi-trajectory averages with random initial
electronic states according to (13). We present these averaged simulations in
this section.

In the proposed experiment with random Rydberg excitation location in a bulk
gas, initialising a specific exciton state $k$, will pose practical
challenges. The most straightforward approach would be detuning a microwave as
discussed in section II.1 such that it is resonant with that state:
$\Delta=U_{k}$. However, the exciton energies $U_{k}$ depend on all Rydberg
positions ${\mathbf{R}}_{\mbox{\\!\\! \scriptsize ini}}$, which are random
subject to constraints by the blockade. As an initial step to address this
challenge, we show the histogram of initial exciton energies for those random
positions in Fig. 4.

Figure 4: (a) Probability distribution $\rho_{k}$ of energies $U_{k}$, $1\leq
k\leq 18$, for 5000 random configurations ($\mathbf{R})$ of atoms. We show a
zoom on the high energy flank in (b,c), together with a certain microwave line
profile $P_{r}$ (thick red line) with detuning (b) $\Delta=120$ MHz and (c)
$\Delta=200$ MHz respectively. The inset shows the resultant surface index
distribution after excitation, according to Eq. (13).

While the energy distribution of energetically neighboring excitons usually
overlap, we can see that the tails contain energy regions where only the
highest energy surface is present. Choosing a detuning in that region, e.g.
$\Delta=200$ MHz and narrow line-width $\sigma_{U}=15.0$ MHz, we can achieve
excitation of the Rydberg assembly almost entirely on the highest energy
surface, as shown in Fig. 4 (c). For realisations of positions in which the
atoms are too far apart to provide an exciton with these high energies, no
excitation would happen for this detuning in an experiment. We model only the
cases where excitation of a $|\,{p}\,\rangle$ state is successful. For the
distribution of excited surfaces we phenomenologically model the microwave
excitation probability (13) with more details in appendix A. Lowering the
detuning to $\Delta=120$ MHz and $\sigma_{U}=15.0$ MHz allows a tuning of the
distribution of surfaces $k$, with almost equal contributions of the three
highest ones, $k=16,17,18$.

We now present multi-trajectory surface-hopping simulations starting from
random initial state distributions as shown in Fig. 4, using $\Delta=200$ MHz
such that the probability of excitation onto the highest energy repulsive
surface is $90\%$, see inset of Fig. 5(a). The figure shows the time and
surface resolved potential energy density $\rho_{s}(t)$, which we construct by
binning the potential energy $U_{s}(t)$ of the currently propagated BO surface
$s(t)$ regarding energy and surface, and by averaging the result over all the
trajectories, see also Leonhardt et al. (2017).

We see, that from the highest energy surface, the system jumps non-
adiabatically to lower energy surfaces and then ultimately can be ionized
after reaching the surface with index $k=15$. Since ionisation is implemented
by stopping the time-evolution and sampling constant quantities thereafter, it
shows up in these histograms as (unphysical) horizontal stripes, which are to
be taken simply as a pointer towards the ionisation event (where the stripes
intersect the bulk distribution).

Figure 5:  Mean time-resolved potential energy density on the (a) second, (b)
third and (c) fourth most energetic BO surface, starting with the microwave
detuned to $\Delta=200$ MHz so that the system most likely begins on the first
surface. To emphasize low density features, we plot the square root of energy
densities and adjust the colorbar range. The insets show (a) the relative
initial excitation probability of each surface, (b) adiabatic populations and
(c) the mean number of ions per trajectory as a function of time.

If the detuning is reduced to $\Delta=120$ MHz with linewidth
$\sigma_{U}=15.0$ MHz, one significantly excites three of the highest energy
surfaces as shown in Fig. 4(b). This relative transition probability is again
shown in the inset of Fig. 6(a). Starting from such an initial state, Fig. 6
shows the evolution of time-resolved potential energy density for the three
most strongly participating surfaces, similarly to Fig. 5. Since fewer non-
adiabatic transitions are required on average to reach the ionising surface,
this scenario exhibits an about three times higher ionisation signal than the
one of Fig. 5. Spectra as shown in Fig. 5 and Fig. 6 are experimentally
accessible through microwave spectroscopy as in Celistrino Teixeira et al.
(2015).

Figure 6:  Mean time-resolved potential energy density similar to Fig. 5 but
for the microwave detuning of $\Delta=120$ MHz, such that more surfaces are
populated initially.

Overall we have shown that for both these microwave detunings, ionization of
Rydberg atoms is strongly linked to non-adiabatic transitions, since the
system will be initialised solely on surfaces on which ionisation does not
occur directly, as shown in section III. We also demonstrated that on the high
energy tails of the initial energy distribution, a reasonable control over the
initial exciton state is possible through the microwave detuning. The control
over the initial state translates into control over the ionization
probability.

The rate of ionisation for the simulations presented here remains relatively
low is an artefact of our restriction to just $N=6$ atoms to keep simulations
tractable. For only six atoms it is relatively unlikely that a pair of atoms
initially repels, the system then undergoes non-adiabatic transitions to leave
the repelling surfaces, and an atom subsequently still encounters a new
collision partner on its outwards journey in order to ionize. The situation
would be very different in an experiment, where a much larger number of
Rydberg atoms can be easily excited. If the initially repelling atoms are
surrounded in all direction by a larger number of Rydberg atoms, it is
reasonable to expect that the ionisation probability after a non-adiabatic
transition could approach unity.

##  V Conclusions

We have modelled the joint electronic and motional dynamics of an assembly of
few ($N=6$) Rydberg excitations that are created at random 3D positions in an
ultra-cold gas. Atoms subsequently move according to resonant dipole-dipole
interactions. With a simple phenomenological model for microwave excitation
with a fixed detuning, we have shown that experiments can selectively
initialise this motional dynamics in dipole-dipole exciton eigenstates that
have entirely repulsive character. We have modelled the motion of the Rydberg
assembly with a quantum classical surface hopping algorithm, that permits non-
adiabatic transitions between exciton states.

These simulations reveal frequent non-adiabatic transitions for the parameters
selected, rendering it likely that the group of Rydberg atoms reaches a Born-
Oppenheimer surface that is no longer repulsive and therefore permits
collisional ionisation of Rydberg atoms. This causal chain of events turns an
ion count into an experimentally accessible flag for non-adiabatic
transitions.

Earlier simulations of non-adiabatic dynamics near conical intersections in
Rydberg systems assumed trapped Rydberg atoms Wüster et al. (2011); Leonhardt
et al. (2014, 2016) or tightly localized excitation beams Leonhardt et al.
(2017), and require high resolution Rydberg position measurements for the
observation of the results. While posssible with a dedicated apparatus Lampen
et al. (2018); Thaicharoen et al. (2015, 2016); Günter et al. (2013), these
requirements pose a challenge to most ultra cold Rydberg experiments. In
contrast, the results presented here should be observable using routinely
applied random Rydberg excitation in a thermal gas and interrogation via ion
counting.

###### Acknowledgements.

We thank Karsten Leonhardt for contributions to the codes used and the Max-
Planck society for financial support under the MPG-IISER partner group
program. RP is grateful to the Council of Scientific and Industrial Research
(CSIR), India, for a Shyama Prasad Mukherjee (SPM) fellowship for pursuing the
PhD (File No. SPM-07/1020(0304)/2019-EMR-I).

##  Appendix A Microwave transitions

The exciton states defined in (7) can be expressed explicitly in the basis (1)
as

$\displaystyle|\,{\varphi_{k}}\,\rangle=\sum_{m,n}f^{(k)}_{nm}|\,{\pi_{n}(m)}\,\rangle\,,$
(15)

where $f_{nm}^{(k)}=\mbox{$\langle\,{\varphi_{k}}\,|\,{\pi_{n}(m)}\,\rangle$}$
are the component amplitudes in the basis state $|\,{\pi_{n}(m)}\,\rangle$ for
the system eigenstate $|\,{\varphi_{k}}\,\rangle$. With (15) the transition
probability $P_{k}$ from the $|\,{s..s..}\,\rangle$ state to the exciton state
Eq. (15), using Eq. (II.1), follows the proportionality

$\displaystyle
P_{k}\propto|\langle\,{\varphi_{k}}\,|\hat{H}_{mw}|\,{s..s..}\,\rangle|^{2}\propto\Big{[}\sum_{n}f_{n0}^{(k)}\Big{]}^{*}\Big{[}\sum_{n}f_{n0}^{(k)}\Big{]}\,.$
(16)

We are not interested in absolute probabilities for the simulation, since we
only want to model trajectories where _some_ exciton state has been excited,
but (16) is sufficient to infer the relative transition probability
$\tilde{P}_{r}(k)$ onto the BO surface $k$ as

$\displaystyle\tilde{P}_{r}(k)=\frac{P_{k}}{\sum_{k}P_{k}}.$ (17)

Using Eq. (17) the relative transition probability for different microwave
detunings $\Delta$ is shown in Fig. 4(b) and (c). For simulations in Fig. 5
and Fig. 6 we remove trajectories for which all exciton energies are far from
the microwave resonance, $|U_{k}-\Delta|>2\sigma_{U}$ $\forall k$, since when
using an absolute excitation probability these cases would simply not show any
excitation of Rydberg $p$ states.

## References

  * Gensemer and Gould (1998) S. Gensemer and P. Gould, Phys. Rev. Lett. 80, 936 (1998).
  * Li et al. (2005) W. Li, P. J. Tanner, and T. F. Gallagher, Phys. Rev. Lett. 94, 173001 (2005).
  * Fioretti et al. (1999) A. Fioretti, D. Comparat, C. Drag, T. Gallagher, and P. Pillet, Phys. Rev. Lett. 82, 1839 (1999).
  * Overstreet et al. (2007) K. R. Overstreet, A. Schwettmann, J. Tallant, and J. P. Shaffer, Phys. Rev. A 76, 011403 (2007).
  * Robicheaux et al. (2004a) F. Robicheaux, J. V. Hernandez, T. Topcu, and L. D. Noordam, Phys. Rev. A 70, 042703 (2004a).
  * Viteau et al. (2008) M. Viteau, A. Chotia, D. Comparat, D. A. Tate, T. Gallagher, and P. Pillet, Phys. Rev. A 78, 040704 (2008).
  * Amthor et al. (2007a) T. Amthor, M. Reetz-Lamour, S. Westermann, J. Denskat, and M. Weidemüller, Phys. Rev. Lett. 98, 023004 (2007a).
  * Amthor et al. (2007b) T. Amthor, M. Reetz-Lamour, C. Giese, and M. Weidemüller, Phys. Rev. A 76, 054702 (2007b).
  * Celistrino Teixeira et al. (2015) R. Celistrino Teixeira, C. Hermann-Avigliano, T. Nguyen, T. Cantat-Moltrecht, J. Raimond, S. Haroche, S. Gleyzes, and M. Brune, Phys. Rev. Lett. 115, 013001 (2015).
  * Thaicharoen et al. (2015) N. Thaicharoen, A. Schwarzkopf, and G. Raithel, Phys. Rev. A 92, 040701 (2015).
  * Gonçalves et al. (2016) L. F. Gonçalves, N. Thaicharoen, and G. Raithel, J. Phys. B: At. Mol. Opt. Phys. 49, 154005 (2016).
  * Thaicharoen et al. (2016) N. Thaicharoen, L. F. Gonçalves, and G. Raithel, Phys. Rev. Lett. 116, 213002 (2016).
  * Park et al. (2011a) H. Park, P. Tanner, B. Claessens, E. Shuman, and T. Gallagher, Phys. Rev. A 84, 022704 (2011a).
  * Park et al. (2011b) H. Park, E. Shuman, and T. Gallagher, Phys. Rev. A 84, 052708 (2011b).
  * Ates et al. (2008) C. Ates, A. Eisfeld, and J. M. Rost, New J. Phys. 10, 045030 (2008).
  * Wüster and Rost (2018) S. Wüster and J. M. Rost, J. Phys. B: At. Mol. Opt. Phys. 51, 032001 (2018).
  * Wüster et al. (2011) S. Wüster, A. Eisfeld, and J. M. Rost, Phys. Rev. Lett. 106, 153002 (2011).
  * Leonhardt et al. (2014) K. Leonhardt, S. Wüster, and J. Rost, Phys. Rev. Lett. 113, 223001 (2014).
  * Leonhardt et al. (2016) K. Leonhardt, S. Wüster, and J. M. Rost, Phys. Rev. A 93, 022708 (2016).
  * Leonhardt et al. (2017) K. Leonhardt, S. Wüster, and J. M. Rost, J. Phys. B: At. Mol. Opt. Phys. 50, 054001 (2017).
  * Dantus and Zewail (2004) M. Dantus and A. Zewail, _Introduction: femtochemistry_ (2004).
  * Hahn and Stock (2000) S. Hahn and G. Stock, J.Phys. Chem. B 104, 1146 (2000).
  * Perun et al. (2005) S. Perun, A. L. Sobolewski, and W. Domcke, J. Am. Chem. Soc. 127, 6257 (2005).
  * Burghardt et al. (2008) I. Burghardt, K. Giri, and G. A. Worth, J. Chem. Phys. 129, 174104 (2008).
  * Worth et al. (2008) G. A. Worth, H. D. Meyer, H. Köppel, L. S. Cederbaum, and I. Burghardt, Int. Rev. Phys. Chem. 27, 569 (2008).
  * Wallis et al. (2009) A. Wallis, S. Gardiner, and J. Hutson, Phys. Rev. Lett. 103, 83201 (2009).
  * Moiseyev et al. (2008) N. Moiseyev, M. Šindelka, and L. S. Cederbaum, J. Phys. B: At. Mol. Opt. Phys. 41, 221001 (2008).
  * Zhu et al. (2007) S. L. Zhu, B. Wang, and L.-M. Duan, Phys. Rev. Lett. 98, 260402 (2007).
  * Larson and Sjöqvist (2009) J. Larson and E. Sjöqvist, Phys. Rev. A 79, 043627 (2009).
  * Gambetta et al. (2021) F. M. Gambetta, C. Zhang, M. Hennrich, I. Lesanovsky, and W. Li (2021), https://arxiv.org/abs/2012.01834.
  * Robicheaux et al. (2004b) F. Robicheaux, J. Hernández, T. Topçu, and L. Noordam, Phys. Rev. A 70, 042703 (2004b).
  * Singer et al. (2005) K. Singer, J. Stanojevic, M. Weidemüller, and R. Côté, J. Phys. B: At. Mol. Opt. Phys. 38, S295 (2005).
  * Tully (1990) J. C. Tully, J. Chem. Phys. 93, 1061 (1990).
  * Möbius et al. (2011a) S. Möbius, S. Wüster, C. Ates, A. Eisfeld, and J. Rost, J. Phys. B: At. Mol. Opt. Phys. 44, 184011 (2011a).
  * Löw et al. (2012) R. Löw, H. Weimer, J. Nipper, J. B. Balewski, B. Butscher, H. P. Büchler, and T. Pfau, J. Phys. B: At. Mol. Opt. Phys. 45, 113001 (2012).
  * Lukin et al. (2001) M. D. Lukin, M. Fleischhauer, R. Cote, L. M. Duan, D. Jaksch, J. I. Cirac, and P. Zoller, Phys. Rev. Lett. 87, 037901 (2001).
  * Urban et al. (2009) E. Urban, T. A. Johnson, T. Henage, L. Isenhower, D. Yavuz, T. Walker, and M. Saffman, Nature Physics 5, 110 (2009).
  * Ates et al. (2007) C. Ates, T. Pohl, T. Pattard, and J. M. Rost, Phys. Rev. A 76, 013413 (2007).
  * Möbius et al. (2011b) S. Möbius, S. Wüster, C. Ates, A. Eisfeld, and J. M. Rost, J. Phys. B: At. Mol. Opt. Phys. 44, 184011 (2011b).
  * (40) The lifetime of $N$ Rydberg atoms $\tau_{n,l}$ at zero temperature can be estimated by $\tau_{n,l}=\tau_{0}^{(l)}n^{3}/N$, where $\tau_{0}^{(l)}$ is the lifetime of a single Rydberg atom. For $n=80$ we have $\tau_{0}^{(l)}\approx 0.058$ $\mu s$ from Beterov et al. (2009), hence for $N=6$, $\tau_{0}^{(l)}\approx 50\mu s$.
  * Lampen et al. (2018) J. Lampen, H. Nguyen, L. Li, P. R. Berman, and A. Kuzmich, Phys. Rev. A 98, 033411 (2018).
  * Günter et al. (2013) G. Günter, H. Schempp, M. Robert-de-Saint-Vincent, V. Gavryusev, S. Helmrich, C. S. Hofmann, S. Whitlock, and M. Weidemüller, Science 342, 954 (2013).
  * Beterov et al. (2009) I. Beterov, I. Ryabtsev, D. Tretyakov, and V. Entin, Phys. Rev. A 79, 052504 (2009).