# The dynamics of Tonks-Girardeau gas excited by a pulse drive

Jia Ligbsn(李佳)  Department of Physics and Institute of Theoretical Physics,
University of Science and Technology Beijing, Beijing 100083, P. R. China
Yajiang Haogbsn(郝亚江<EMAIL_ADDRESS>Department of Physics and Institute of
Theoretical Physics, University of Science and Technology Beijing, Beijing
100083, P. R. China

###### Abstract

In this paper we study the dynamics of Tonks-Girardeau (TG) gases in a
harmonic potential driven by Gaussian pulse, which is a correspondence of the
excitation dynamics of electrons in matters driven by ultrashort laser pulse.
The evolving dynamics of TG gas are obtained with Bose-Fermi mapping method
combined with the numerical techniques. We calculate the evolving dynamics of
occupation distribution of single-particle energy levels, density distribution
and momentum distribution of the system. It is shown that the system arrived
at a dynamically stable state at the end of driving. At high-frequency regime
TG gases return back to ground state while at low-frequency regime the
population inversion exhibits and all atoms occupy high levels.

††preprint: APS/123-QED

##  I INTRODUCTION

Since cold atoms were realized in experiments, ultra-cold atoms have become a
popular platform to investigate basic physical processes in many fields
including condensed matter physics, quantum information processing, plasma
physics, etc. Particularly, the rapid progress in cold atoms techniques make
it play crucial roles to simulate many body quantum system. The experiment
development of optical lattices deepens the understanding of not only the
ground state quantum phase transition but also the non-equilibrium dynamics in
periodical interacting system [1]. Cold atoms in periodical driving optical
lattices were investigated as the important practical platform for Floquet
engineering. The studies on the artificial gauge fields [2], the dynamical
localization [3, 4], the dynamical quantum phase transition [5], topology
physics [6, 7, 8] have made great progress with the rapid advance in
experiment techniques in cold atoms. Besides the dynamics in optical lattice
[9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21], modulated dynamics in
harmonic trap [22], the temperature effect [23], the disorder effect for
strong periodic forced bose gas [24] and the nonequilibrium quantum
thermodynamics [23] were also studied.

In cold atoms the atomic interaction can be tuned in the whole interacting
regime from the weak interaction to the strong interaction with the Feschbach
resonance and confined induced resonance techniques [25, 26]. With anisotropic
trap or optical lattices the cold atoms can be confined strongly in transverse
direction and therefore the system become an one dimensional (1D) quantum
system in the longitudinal direction [27, 28, 29, 30]. The tunability of
atomic interaction, the controllability of dimension and time-dependent
parameters offer us new opportunities that the traditional research areas
cannot arrive at. The 1D cold atoms system has been paid great attentions by
both experimentalists and theorists [31, 32, 33].

For Bose-Einstein condensates (BECs) with weakly interaction we can obtain the
ground state and dynamics by solving the Gross-Pitaevskii equation [34]. The
tunneling dynamics of BECs in a double-well can be described by two coupled
nonlinear equations [35]. When the atomic interaction is strong the system
that can be solved analytically is very rare and the asymptotic analytical
results exist only in specific limits. For example, Scopa et al. [36] proposed
an exact analytical formula for the single particle density matrix of the non-
equilibrium TG gases [37, 38] at zero temperature in the limit of large $N$.
Moreno et al. [39] showed that the momentum distribution of TG gases at the
high momentum limit is a power law form of $k^{-4}$, and their formula can
replace numerical simulation in the high momentum region. For the 1D quantum
system, non-perturbation method is necessary for its strong correlation
effect. The generalized hydrodynamics method has been developed for the
integrable system [40] and is applicable in 1D cold atoms. Another effective
approach for 1D system is the shortcuts to adiabaticity approach [41, 42].

Although the above experimental techniques and theoretical methods have
greatly stimulate the development of cold atom research, the new experiment
protocols and theoretical tools are still expected. One of the important
topics in the study on the quantum statistical physics, for example the
eigenstates thermalization, is the preparation of long-lived excited states
[43]. In the present paper, we will study the evolving dynamics of TG gases in
a harmonic potential driven by a Gaussian pulse, which is a correspondence of
the excitation dynamics of electrons in matters driven by ultrashort laser
pulse. It will be shown that under the pulse drive the TG gases will arrived
at a dynamically stable excited state and occupation distribution inversion
appears at the end of the pulse. The pulse optical drive is expected to be a
candidate tool to obtain the stable excited state of TG gases.

In section II, we develop the numerical techniques based on the Bose-Fermi
mapping method. In Section III, we show the explicit formula of the density
distribution in coordinate space, the reduced one-body density matrix, the
momentum distribution in momentum space and the occupation distribution of
single particle levels. The numerical result for them are displayed in section
IV. Finally, the conclusion are given in Sec. V.

##  II Model and method

We consider the dynamics of $N$ indistinguishable Bose atoms of mass $m$ in 1D
that satisfy the following time-dependent Schrödinger equation

$\displaystyle{\rm{i}}\hbar\frac{{\partial{\Psi_{B}}}}{{\partial t}}=$
$\displaystyle\sum\limits_{i=1}^{N}{\left[{-\frac{{{\hbar^{2}}}}{{2m}}\frac{{{\partial^{2}}}}{{\partial
x_{i}^{2}}}+V\left({{x_{i}},t}\right)}\right]}{\Psi_{B}}$
$\displaystyle+{g_{1D}}\sum\limits_{1\leq i<j\leq
N}{\delta\left({{x_{i}}-{x_{j}}}\right)}{\Psi_{B}},$

in which the external potential is a harmonic potential superimposed by a
drive potential, i.e.,

$V\left({x,t}\right)=\frac{1}{2}m\omega_{0}^{2}{x^{2}}-xS(t)\theta(t),$

where $g_{1D}$ and ${\omega_{0}}$ is the effective 1D interacting constants
and trapping frequency, respectively. The second term $xS(t)$ in $V(x,t)$ is a
time-dependent drive, which added to the system at time $t=0$. $\theta(t)$ is
unit step function, which is 0 and 1 for $t<0$ and $t\geq 0$, respectively. In
the present paper, we will focus on the strongly interacting limit
${g_{1D}}\to+\infty$. The solution to this system can be obtained with the
Fermi-Bose mapping method from the wavefunction of noninteracting fermions
$\Psi_{F}(x_{1},x_{2},\cdots,x_{N};t)$ [44]

${\Psi_{B}}\left({{x_{1}},\cdots,{x_{N}};t}\right)=A\left({{x_{1}},\cdots,{x_{N}}}\right){\Psi_{F}}\left({{x_{1}},\cdots,{x_{N}};t}\right)$

with the mapping function

$A\left({{x_{1}},\cdots,{x_{N}}}\right)=\prod\limits_{1\leq i<j\leq
N}{{\rm{sign}}\left({{x_{i}}-{x_{j}}}\right)}.$

Its effect is to map the exchange antisymmetric wave function of fermions into
an exchange symmetric wave function of bosons. sign($x$) is sign function and
is equal to 1, 0, and -1, for $x$ $>0$, $=0$, and $<0$, respectively. We just
need to solve the Schrödinger equation,

${\rm{i}}\hbar\frac{{\partial{\Psi_{F}}}}{{\partial
t}}=\sum\limits_{i=1}^{N}{\left[{-\frac{{{\hbar^{2}}}}{{2m}}\frac{{{\partial^{2}}}}{{\partial
x_{i}^{2}}}+\frac{1}{2}m\omega_{0}^{2}{x_{i}^{2}}-{x_{i}}S(t)}\right]}{\Psi_{F}}$
(1)

with respect to ${\Psi_{F}}\left({{x_{1}},\cdots,{x_{N}};t}\right)$, and
${\Psi_{B}}\left({{x_{1}},\cdots,{x_{N}};t}\right)$ is obtained by Bose-Fermi
mapping.

The general wave function to the above time-dependent problem can be
formulated as

${\Psi_{F}}=\sum_{n}{{c_{n}}{\psi_{n}}\left({{x_{1}},\cdots,{x_{N}}}\right){e^{-{\rm{i}}{E_{n}}t/\hbar}}},$
(2)

where $n$ specify different eigen functions
${\psi_{n}\left({{x_{1}},\cdots,{x_{N}}}\right)}$ with ${E_{n}}$ being the
corresponding eigen energy and ${c_{n}}$ is the superposition coefficient. The
energies ${E_{n}}$ are listed in order from the smallest to the largest.
Theoretically it is a summation of infinite terms, but it is reasonable to
assume that in a finite time the probability is very small for a particle to
be excited to very high energy levels. So we can truncate the infinite eigen
space into a finite space. The eigen function is compactly written in a form
of the Slater determinant,

${\psi_{n}}\left({{x_{1}},\cdots,{x_{N}}}\right)=\frac{1}{{\sqrt{N!}}}\mathop{\det}\limits_{l,k=1}^{N}\left[{{\varphi_{l-1}}\left({{x_{k}}}\right)}\right],$

where ${\varphi_{l}}(x)$ is the 1D harmonic oscillator eigenfunction. The
different eigen functions correspond to different atom occupation
configuration and can be simply denoted by the Dirac symbol
$\left|\psi_{1}\right\rangle=\left|{0,1\cdots,N-2,N-1}\right\rangle$,
$\left|{\psi_{2}}\right\rangle=\left|{0,1,\cdots N-2,N}\right\rangle$,
$\left|{\psi_{3}}\right\rangle=\left|{0,1,\cdots N-2,N+1}\right\rangle$,
$\left|{\psi_{4}}\right\rangle=\left|{0,1,\cdots N-3,N-1,N}\right\rangle$, and
etc.. Here the set of numbers in $\left|n_{1},n_{2},\cdots,n_{N}\right\rangle$
denote the occupied single particle energy levels of harmonic trap.

Combining Eq. (2) with Eq. (1), we have

${\rm{i}}\hbar{{\dot{c}}_{m}}=-\sum\limits_{n=1}{{c_{n}}(t){\Gamma_{mn}}}{e^{-{\rm{i(}}{E_{n}}-{E_{m}})t/\hbar}}$

with the transition matrix elements

${\Gamma_{mn}}=S(t)\sum\limits_{j=1}^{N}{\int{{\psi_{m}}{x_{j}}{\psi_{n}}}}\prod\limits_{i=1}^{N}{{\rm{d}}{x_{i}}}.$
(3)

It can be proved that $\Gamma$ is a sparse matrix (Appendix A)

$\displaystyle{\Gamma_{mn}}=$ $\displaystyle\begin{aligned}
&\frac{{{\alpha_{0}}}}{{\sqrt{2}}}S(t)\sum\limits_{i=1}^{N}{\sqrt{{n_{i}}+1}\left|{\begin{array}[]{*{20}{c}}{{\delta_{{n_{1}},{m_{1}}}}}&{{\delta_{{n_{i}}+1,{m_{1}}}}}&{{\delta_{{n_{N}},{m_{1}}}}}\\\
{{\delta_{{n_{1}},{m_{i}}}}}&{{\delta_{{n_{i}}+1,{m_{i}}}}}&{{\delta_{{n_{N}},{m_{i}}}}}\\\
{{\delta_{{n_{1}},{m_{N}}}}}&{{\delta_{{n_{i}}+1,{m_{N}}}}}&{{\delta_{{n_{N}},{m_{N}}}}}\end{array}}\right|}\\\
+&\frac{{{\alpha_{0}}}}{{\sqrt{2}}}S(t)\sum\limits_{i=1}^{N}{\sqrt{{n_{i}}}\left|{\begin{array}[]{*{20}{c}}{{\delta_{{n_{1}},{m_{1}}}}}&{{\delta_{{n_{i}}-1,{m_{1}}}}}&{{\delta_{{n_{N}},{m_{1}}}}}\\\
{{\delta_{{n_{1}},{m_{i}}}}}&{{\delta_{{n_{i}}-1,{m_{i}}}}}&{{\delta_{{n_{N}},{m_{i}}}}}\\\
{{\delta_{{n_{1}},{m_{N}}}}}&{{\delta_{{n_{i}}-1,{m_{N}}}}}&{{\delta_{{n_{N}},{m_{N}}}}}\end{array}}\right|},\end{aligned}$

with
${\alpha_{0}}=\sqrt{{\hbar\mathord{\left/{\vphantom{\hbar{m{\omega_{0}}}}}\right.\kern-1.2pt}{m{\omega_{0}}}}}$.
For simplicity, in the following numerical calculations we will take
$m=\hbar={\omega_{0}}={\alpha_{0}}=1$ and the dimension of time is
$1/\omega_{0}$.

##  III The density profile and momentum distribution

The density distribution of many particles in real space is defined as

$\displaystyle\rho(x,t)$
$\displaystyle=N\int{\rm{d}}x_{2}{\rm{d}}x_{3}\cdots{\rm{d}}x_{N}$
$\displaystyle\times\Psi_{B}^{*}(x,x_{2},\cdots,x_{N};t)\Psi_{B}(x,x_{2},\cdots,x_{N};t).$

Following the definition in Sec. II, the density distribution can be
formulated as

$\displaystyle\rho(x,t)=N\sum\limits_{m=1}^{N}{\sum\limits_{n=1}^{N}{c_{m}^{*}}}{c_{n}}{D_{mn}}{e^{{\rm{i}}\left({{E_{m}}-{E_{n}}}\right)t}},$

in which (see Appendix B for details)

$\displaystyle{D_{mn}}=\frac{1}{N}\sum\limits_{i=1}^{N}{\sum\limits_{j=1}^{N}{{\varphi_{{n_{i}}}}{\varphi_{{m_{j}}}}}\left(x\right){{\left({-1}\right)}^{i+j}}\prod\limits_{k,l\neq
i,j}^{N}{{\delta_{{n_{k}},{m_{l}}}}}}.$

With the many-body wave function, the reduced onebody density matrix (ROBDM)
is formulated as

$\displaystyle\rho(x,y,t)$
$\displaystyle=N\int{\rm{d}}x_{2}{\rm{d}}x_{3}\cdots{\rm{d}}x_{N}$ (5)
$\displaystyle\times\Psi_{B}^{*}(x,\cdots,{x_{N}};t)\Psi_{B}(y,\cdots,{x_{N}};t)$

and following the same procedure as the above calculation of density
distribution $\rho(x,y,t)$ can be expressed as

$\rho(x,y,t)=N\sum\limits_{m=1}^{N}{\sum\limits_{n=1}^{N}{c_{m}^{*}}}{c_{n}}{P_{mn}}{e^{{\rm{i}}\left({{E_{m}}-{E_{n}}}\right)t}}.$

Here $P_{mn}$ is the integral of different eigen functions

$\displaystyle{P_{mn}}=$
$\displaystyle\int\prod\limits_{i=2}^{N}{{\rm{d}}{x_{i}}}{{\rm{sign}}\left({x-{x_{i}}}\right){\rm{sign}}\left({y-{x_{i}}}\right)}$
$\displaystyle\times{{\psi_{m}}\left({x,\cdots,{x_{N}}}\right){\psi_{n}}\left({y,\cdots,{x_{N}}}\right)}$

and the integral can be given in a concise form (see Appendix B for details)
[45]

${P_{mn}}=\sum\limits_{i=1}^{N}{\sum\limits_{j=1}^{N}{{\varphi_{{n_{i}}}}(x)}{\varphi_{{m_{j}}}}(y){A_{ij}}}$

with

${A_{ij}}={(-1)^{i+j}}\det{{{M}}_{kl}}$

and

${M_{kl}}(x,y)={\delta_{kl}}-2\int_{x}^{y}{{\varphi_{k}}(\alpha){\varphi_{l}}(\alpha){\rm{d}}\alpha}.$

While we obtain the ROBDM, the momentum distribution can be obtained by its
Fourier transformation

$n(k,t)=\frac{1}{{2\pi}}\int{{\rm{d}}x}\int{{\rm{d}}y\rho(x,y,t){e^{-{\rm{i}}k(x-y)}}}.$

It is also interesting to investigate the occupation distribution evolution of
the single particle eigen states of harmonic potential induced by the external
driving, which is denoted by $p_{j}$ in the following. Obviously, summing the
number of particles over all energy levels give the total number of particles
$N$. The relationship between $p_{j}$ and $c_{n}$ is

${p_{j}}=\sum\limits_{n}{{{\left|{{c_{n}}}\right|}^{2}}}p_{nj},$

if the energy level $j$ is a harmonic oscillator state of the constituent
quantum states $\left|{\psi_{n}}\right\rangle$ then $p_{nj}=1$, otherwise
$p_{nj}=0$.

##  IV Numerical results

(a)  (b)  (c)  (d)  (e)

Figure 1: The evolving dynamics of TG gases with $N$ = 4, $S_{A}$=3, $\Delta$
= 5 and $\omega$ = 4 $\omega_{0}$. (a) The laser pulse $S(t)$; (b) The
occupations of the initially occupied levels: $p_{j}$ for $j$ = 0, 1, 2, and
3; (c) The occupations of the initially unoccupied levels: $p_{j}$ for $j$ =
4, 5, 6 and the total occupations $p_{e}$; (d) The density distribution
$\rho(x,t)$; (e) The momentum distribution $n(k,t)$.

In this section, we will show the evolution of density distribution, momentum
distribution and occupation distribution of single particle energy levels
induced by the external drive potential. In order to solve the problem of high
computational cost because of the enormous eigen space, we truncate the eigen
space at a certain energy threshold (the total energy of the specified eigen
state of many particles), and thus greatly reduce the dimension of Hilbert
space.

In the present paper we focus on a non-periodical driving to simulate the
excited dynamics of matter radiated by ultrashort pulse laser. For a general
drive pulse
$S(t)=S_{A}\exp\left({-{{(t-t_{0})}^{2}}/\Delta}\right)\sin\left({\omega(t-t_{0})+\phi_{0}}\right)$,
where $S_{A}$ is the driving strength, $\omega/2\pi$ is the center or carrier
frequency and $\sqrt{\Delta/2}$ determines the bandwidth of the pulse, such as
the drive shown in Fig. 1a, in which the blue solid lines display the pulse
drive of a Gaussian envelope (the red solid lines). In the subsequent
calculation, we stipulate that $t_{0}=7$ and $\phi_{0}=\pi/2$, which are not
sensitive for the present study.

The occupations of single particle energy level, the density distributions,
and momentum distributions for Tonks-Girardeau gases of $N=4$ are displayed in
Fig. 1b-Fig. 1d. Initially, the TG gases stay at its ground state in which
four atoms occupy at the lowest four energy levels with $p_{j}=1$
($j=0,1,2,3$). Under the external drive, the atom at the highest occupied
energy level (HOEL) ($j=3$ here) is excited at first and the excitation of the
atoms at lower energy levels follow up. The occupations of initially occupied
levels decrease oscillatingly in the first half of Gaussian drive and increase
oscillatingly in the second half. The occupation distribution evolution of the
initial unoccupied levels is just the reverse. The lowest unoccupied energy
level (LUEL) ($j=4$ here) is occupied firstly and those higher unoccupied
levels are occupied successively. During the evolution the occupation of HOEL
and LUEL exhibit the larger amplitudes comparing with other initial occupied
energy levels and unoccupied energy levels. The total occupations of all
single particle excited states ($p_{e}=\sum_{j\geq N}p_{j}/N$) are also ploted
in red solid lines in Fig 1c (the total atom number is divided here to match
the whole figure). During the pulse drive the oscillation amplitude of
occupations increase and decrease as the pulse drive become strong and weak.
All the evolution take place during the pulse drive and the evolution dynamics
stop at the end of the pulse drive. It is interesting to notice that the whole
system evolves back into the initial states completely once the pulse drive
closes.

The density distribution (Fig. 1d) and momentum distributions (Fig. 1e) also
oscillate strongly or weakly with the change of the pulse drive amplitude. The
center of the distribution oscillate with the change of pulse drive but both
of them preserve their initial distribution properties. In the coordinate
space the TG gases behave in the same way as noninteracting fermions and
exhibit a shell structure of $N$ peaks. While in momentum space they display
single peak structure that is a typical property of Bosons [46].

(a)  (b)  (c)

Figure 2: The evolving dynamics of TG gases with $N$ = 4, $S_{A}$=2, $\Delta$
= $\infty$ and $\omega$ = 2$\omega_{0}$. (a) The occupations of the initially
occupied levels: $p_{j}$ for $j$ = 0, 1, 2, and 3; (b) The occupations of the
initially unoccupied levels: $p_{j}$ for $j$ = 4, 5, 6 and the total
occupations $p_{e}$; (c) The momentum distribution $n(k,t)$.

In the following we investigate the evolution dynamics under the drive
potential in two limiting case, i.e., the periodical drive
$S(t)=S_{A}\sin\left({\omega t+\phi_{0}}\right)$ (in the infinite bandwidth
limit $\Delta\rightarrow\infty$) and the Gaussian drive (in the zero frequency
limit $\omega\rightarrow 0$).

The density distribution in coordinate space will not be displayed because TG
gases always oscillate as an entity with the same properties as those of the
pulse drive. We plot the evolving dynamics of the occupations of single
particle energy levels and momentum distribution for TG gases driven by the
periodical potential in Fig. 2. It is shown that all of them evolve
periodically with the period being twice that of the drive potential. It is
same as the case in Fig. 1, in which the occupation of HOEL oscillate at first
with a larger amplitude and that of other lower initially occupied level start
to oscillate later with smaller amplitude. For the initial occupied levels,
the higher the level, the greater the amplitude and the earlier the
oscillation begins. For the initially unoccupied levels, the lower the level,
the greater the amplitude and the earlier the oscillation begins. The
occupation of LUEL start to oscillate earliest and has the maximum amplitude.
The momentum distribution evolve periodically with the same period as that of
occupation. During the evolution the momentum distribution preserve the
typical single peak structure of Bosons. The only difference from those in
Fig. 1 is that the dynamics are periodical in the present situation. The above
results are consistent with those obtained by the analytical method [47],
which fully demonstrates the correctness of the present numerical method and
it can be calculated for arbitrary external drive.

(a)  (b)  (c)

Figure 3: The evolving dynamics of TG gases with $N$ = 4, $S_{A}$ = 3,
$\Delta$ = 5 and $\omega$ = 0. (a) The occupations of the initially occupied
levels: $p_{j}$ for $j$ = 0, 1, 2, and 3; (b) The occupations of the initially
unoccupied levels: $p_{j}$ for $j$ = 4, 5, 6 and the total occupations
$p_{e}$; (c) The momentum distribution $n(k,t)$.

When $\omega\rightarrow 0$, the pulse becomes a single Gaussian pulse drive
$S(t)=S_{A}\exp\left({-{{(t-t_{0})}^{2}}/\Delta}\right)$. The evolution of
occupations and momentum distribution are plotted in Fig. 3 for Gaussian
drive. In this situation, the evolution of occupation still begin at the HOEL
and the LUEL. The occupations of initially occupied levels are shown in Fig.
3a. They decrease at the first half of the Gaussian drive and arrive at the
smallest as the Gaussian drive approach to the strongest. Later the
occupations increase and reach the stable values at the end of the pulse drive
and the occupation of low level is higher than that of high level. The
occupation evolution of the initially unoccupied level is plotted in Fig. 3b.
These levels also arrive at a stable occupations at the end of drive. It is
interesting that the LUEL is not occupied with the largest probability
finally. The total occupation of all initial unoccupied levels is also
exhibited in Fig. 3b in red solid lines, which arrive at the peak value near
the maximum drive and become stable as the Gaussian drive terminates. In a
word, the Gaussian pulse drive excite the TG gases to the excited state in
which atoms populate in more energy levels with definite probabilities. In
this case the momentum distribution still exhibits the typical single peak
structure of Bosons during the evolution, which is plotted in Fig. 3c. Because
the TG gas is excited, its momentum distribution oscillate periodically around
the zero momentum and arrives at a dynamical stable state. This is obviously
different from the cases in Fig. 1 and in Fig. 2.

(a)  (b)

Figure 4: The occupations for the TG gases with $N$ = 2, $S_{A}$=3 and
$\Delta$ = 5. (a) The final stable occupations dependence on the pulse driving
frequency; (b) The evolving occupation distribution for $\omega$ =
$\omega_{0}$.

The numerical calculations demonstrate that occupation distribution of energy
levels always arrive at stable as long as the external drive come to the end.
It is only under the periodical drive that the occupation distribution
oscillates periodically. It is interesting to investigate the final stable
occupation distribution of different levels after the end of pulse drive. We
display the occupation distribution dependence on the driving frequency
$\omega$ in Fig. 4a for $N=2$, in which the occupation of lower levels $p_{j}$
($j=0,1,2,3$) and the total occupation of high levels ($j>2$) are plotted, and
as a representative of high levels $p_{14}$ is also plotted. It is shown that
under the high frequency driving ($\omega>3\omega_{0}$) the TG gases return
back to the ground state and $N$ atoms occupy the lowest $N$ levels with one
atom being on one level. Under the low frequency driving, the occupation
inversion take place. In the region of $\omega<0.5\omega_{0}$, atoms are
excited to high levels ($j>N-1$) with larger probability and occupy the low
levels ($j=0,...,N-1$) with smaller probability. As the driving frequency is
close to trap frequency of harmonic trap
($0.5\omega_{0}<\omega<1.5\omega_{0}$) all atoms occupy high levels (for
example, the level $j=14$) and $p_{e}$ arrive at 1, while the lower levels are
vacant ($j=0,1,2,3$). The exciting process of atoms from the low levels to
high levels for $\omega=\omega_{0}$ is displayed in Fig. 4b. In the first
period (around $t<6$) the occupation of HOEL decreases at first followed by
the decrease of level $j=0$, and the occupation of HUEL increases at first
followed by the increase of higher levels sequentially. In the second period
(around $t=9$), atoms distribute on levels of $8\leq j\leq 19$ with almost
equal probability. Finally the occupation evolve into two branches with upper
levels around $j=24$ and down levels around $j=14$.

(a)  (b)

Figure 5: The occupations at the end of the pulse when $\omega=\omega_{0}$ for
different particle numbers: $N=3$ (a) and $N=4$ (b). The blue bar is the
calculated data, and the red line is the fitting curve of Gaussian function.

When the driving frequency is close to the level space of harmonic potential,
i.e., $\omega\sim\omega_{0}$, no particle occupies the lowest $N$ levels and
all atoms are completely excited to high levels (complete excitation). The
peak number of final stable multi-peak structure is the number of atoms. In
Fig. 5 we display the occupation distribution of $N$=3 and 4. Each peak is a
Gaussian, which can be confirmed by fitting the occupations to the Gaussian
functions
$p(j)=\sum\limits_{i=1}^{N}{{a_{i}}\exp\left({-{{{\left({j-{b_{i}}}\right)}^{2}}}/{{c_{i}}}}\right)}$.
The fitted lines are plotted in Fig. 5 in red solid lines. The special
occupation distribution is related with the larger transition coefficient for
the higher energy level. The higher transition result in the faster
transition, so that after a longer excitation, each particle displays a
separate peak.

In complete excitation, the distribution of occupy number is no longer
sensitive to the change of pulse parameters, and always presents a Gaussian
distribution. However, the higher the pulse intensity and pulse width, the
overall distribution will move to the higher energy level. At the same time,
due to the continuous increase of the transition coefficient, the Gaussian
distribution of the occupancy number will become shorter and wider (Fig. 6a),
and the distance between the multi-particle peak centers will also increase
(Fig. 6b).

(a)  (b)

Figure 6: The final occupation: The orange bar doubles the pulse intensity
relative to the blue bar for $N=1$ (a); The orange bar doubles the pulse
intensity and pulse width relative to the blue bar for $N=2$ (b).

##  V Conclusion

We study the dynamics of Tonks-Girardeau gases confined in a harmonic
potential driven by a pulse driving. The time-dependent many-body wave
function is obtained based on the Bose-Fermi mapping method combined with
numerical method. The occupation distribution of single particle levels, and
the density distribution and momentum distribution are exhibited. It is shown
that during driving the density distribution always exhibits a shell structure
and momentum distribution exhibits a typical single peak structure and the
structures will not deform. The TG gases oscillate around the initial position
as a whole with the change of driving potential. The oscillation amplitude
also increase and decrease with the increase and decrease of the driving
strength except that under the periodical driving. The occupation evolution of
single particle energy levels always begin from the HOEL and LUEL and both of
them has the biggest oscillation amplitude. It is interesting to note that
under pulse drive TG gases always arrive at a dynamically stable state in
which the momentum distribution oscillate around the point $k=0$ periodically
and the occupation distribution exhibit the behaviour of multi-Gaussian
distribution with peak number being the atom number. Under the high-frequency
driving TG gases return back to ground state at the end of the driving and
under the low-frequency driving TG gases are excited to stable excited states
and occupation inversion is displayed. As the driving frequency approximate to
the trap frequency atoms are excited completely and the lower levels will not
be occupied.

##  Appendix A Calculation of transition matrix elements

In this appendix, we will give a detailed derivation of the transition matrix
elements $\Gamma_{mn}$ in section II. Let’s first consider one of the integral
terms,

$\displaystyle\Gamma_{mn}^{j}=$
$\displaystyle\int{{\psi_{m}\left({{x_{1}},\cdots,{x_{N}}}\right)}{x_{j}}{\psi_{n}\left({{x_{1}},\cdots,{x_{N}}}\right)}}\prod\limits_{i=1}^{N}{{\rm{d}}{x_{i}}}$
$\displaystyle=$
$\displaystyle\left\langle{{m_{1}}{m_{2}}\cdots{m_{N}}}\right|{x_{j}}\left|{{n_{1}}{n_{2}}\cdots{n_{N}}}\right\rangle$
$\displaystyle=$
$\displaystyle\frac{{{\alpha_{0}}}}{{\sqrt{2}}}\left\langle{{m_{1}}{m_{2}}\cdots{m_{N}}}\right|\left({a_{j}^{+}+a_{j}^{-}}\right)\left|{{n_{1}}{n_{2}}\cdots{n_{N}}}\right\rangle,$
$\left|{{n_{1}}{n_{2}}\cdots{n_{N}}}\right\rangle=\frac{1}{{\sqrt{N!}}}\left|{\begin{array}[]{*{20}{c}}{{{\left|{{n_{1}}}\right\rangle}_{1}}}&{{{\left|{{n_{1}}}\right\rangle}_{2}}}&\cdots&{{{\left|{{n_{1}}}\right\rangle}_{N}}}\\\
{{{\left|{{n_{2}}}\right\rangle}_{1}}}&{{{\left|{{n_{2}}}\right\rangle}_{2}}}&\cdots&{{{\left|{{n_{2}}}\right\rangle}_{N}}}\\\
\vdots&\vdots&\ddots&\vdots\\\
{{{\left|{{n_{N}}}\right\rangle}_{1}}}&{{{\left|{{n_{N}}}\right\rangle}_{2}}}&\cdots&{{{\left|{{n_{N}}}\right\rangle}_{N}}}\end{array}}\right|,$

where subscripts inside Dirac symbols represent the ordering of quantum
states, while subscripts outside Dirac symbols represent the ordering of
particles. The result of $x_{i}$ acting on a $N$ particles state
$\left|{{n_{1}}\cdots{n_{i}}\cdots{n_{N}}}\right\rangle$ is

$\displaystyle\frac{{{\alpha_{0}}}}{{\sqrt{2N!}}}\left|{\begin{array}[]{*{20}{c}}{{{\left|{{n_{1}}}\right\rangle}_{1}}}&{\sqrt{{n_{1}}+1}{{\left|{{n_{1}}+1}\right\rangle}_{i}}}&{{{\left|{{n_{1}}}\right\rangle}_{N}}}\\\
{{{\left|{{n_{i}}}\right\rangle}_{1}}}&{\sqrt{{n_{i}}+1}{{\left|{{n_{i}}+1}\right\rangle}_{i}}}&{{{\left|{{n_{i}}}\right\rangle}_{N}}}\\\
{{{\left|{{n_{N}}}\right\rangle}_{1}}}&{\sqrt{{n_{N}}+1}{{\left|{{n_{N}}+1}\right\rangle}_{i}}}&{{{\left|{{n_{N}}}\right\rangle}_{N}}}\end{array}}\right|$
$\displaystyle+$
$\displaystyle\frac{{{\alpha_{0}}}}{{\sqrt{2N!}}}\left|{\begin{array}[]{*{20}{c}}{{{\left|{{n_{1}}}\right\rangle}_{1}}}&{\sqrt{{n_{1}}+0}{{\left|{{n_{1}}-1}\right\rangle}_{i}}}&{{{\left|{{n_{1}}}\right\rangle}_{N}}}\\\
{{{\left|{{n_{i}}}\right\rangle}_{1}}}&{\sqrt{{n_{i}}+0}{{\left|{{n_{i}}-1}\right\rangle}_{i}}}&{{{\left|{{n_{i}}}\right\rangle}_{N}}}\\\
{{{\left|{{n_{N}}}\right\rangle}_{1}}}&{\sqrt{{n_{N}}+0}{{\left|{{n_{N}}-1}\right\rangle}_{i}}}&{{{\left|{{n_{N}}}\right\rangle}_{N}}}\end{array}}\right|.$

When taking the inner product of
${\left|{{m_{1}}\cdots{m_{i}}\cdots{m_{N}}}\right\rangle^{\dagger}}$ and
$x_{i}\left|{{n_{1}}\cdots{n_{i}}\cdots{n_{N}}}\right\rangle$, expand the
determinant of the first term above. This will result in $(N-1)!$ subterms
with coefficients $\sqrt{{n_{i}}+1}$. Let’s focus only on the subterms with
coefficients $\sqrt{{n_{1}}+1}$,

$\gamma_{1}=\frac{{{\alpha_{0}}}}{{\sqrt{2N!}}}\sqrt{{n_{1}}+1}{\left|{{n_{1}}+1}\right\rangle_{i}}{\left|{{n_{2}}\cdots{n_{N}}}\right\rangle_{i}},$
${\left|{{n_{2}}\cdots{n_{N}}}\right\rangle_{i}}=\left|{\begin{array}[]{*{20}{c}}{{{\left|{{n_{2}}}\right\rangle}_{1}}}&{{{\left|{{n_{2}}}\right\rangle}_{i-1}}}&{{{\left|{{n_{2}}}\right\rangle}_{i+1}}}&{{{\left|{{n_{2}}}\right\rangle}_{N}}}\\\
{{{\left|{{n_{i-1}}}\right\rangle}_{1}}}&{{{\left|{{n_{i-1}}}\right\rangle}_{i-1}}}&{{{\left|{{n_{i-1}}}\right\rangle}_{i+1}}}&{{{\left|{{n_{i-1}}}\right\rangle}_{N}}}\\\
{{{\left|{{n_{i}}}\right\rangle}_{1}}}&{{{\left|{{n_{i}}}\right\rangle}_{i-1}}}&{{{\left|{{n_{i}}}\right\rangle}_{i+1}}}&{{{\left|{{n_{i}}}\right\rangle}_{N}}}\\\
{{{\left|{{n_{N}}}\right\rangle}_{1}}}&{{{\left|{{n_{N}}}\right\rangle}_{i-1}}}&{{{\left|{{n_{N}}}\right\rangle}_{i+1}}}&{{{\left|{{n_{N}}}\right\rangle}_{N}}}\end{array}}\right|.$

The inner product of
${\left|{{m_{1}}\cdots{m_{i}}\cdots{m_{N}}}\right\rangle^{\dagger}}$ and
$\gamma_{1}$ is

$\frac{{{\alpha_{0}}}}{{\sqrt{2}N}}\sqrt{{n_{1}}+1}\left|{\begin{array}[]{*{20}{c}}{{\delta_{{n_{1}}+1,{m_{1}}}}}&{{\delta_{{n_{i}},{m_{1}}}}}&{{\delta_{{n_{N}},{m_{1}}}}}\\\
{{\delta_{{n_{1}}+1,{m_{i}}}}}&{{\delta_{{n_{i}},{m_{i}}}}}&{{\delta_{{n_{N}},{m_{i}}}}}\\\
{{\delta_{{n_{1}}+1,{m_{N}}}}}&{{\delta_{{n_{i}},{m_{N}}}}}&{{\delta_{{n_{N}},{m_{N}}}}}\end{array}}\right|$

and after adding up all the different coefficient terms we have

$\displaystyle\left\langle{{m_{1}}{m_{2}}\cdots{m_{N}}}\right|{x_{i}}\left|{{n_{1}}{n_{2}}\cdots{n_{N}}}\right\rangle$
$\displaystyle=$
$\displaystyle\frac{{{\alpha_{0}}}}{{\sqrt{2}}N}\sum\limits_{i=1}^{N}{\sqrt{{n_{i}}+1}\left|{\begin{array}[]{*{20}{c}}{{\delta_{{n_{1}},{m_{1}}}}}&{{\delta_{{n_{i}}+1,{m_{1}}}}}&{{\delta_{{n_{N}},{m_{1}}}}}\\\
{{\delta_{{n_{1}},{m_{i}}}}}&{{\delta_{{n_{i}}+1,{m_{i}}}}}&{{\delta_{{n_{N}},{m_{i}}}}}\\\
{{\delta_{{n_{1}},{m_{N}}}}}&{{\delta_{{n_{i}}+1,{m_{N}}}}}&{{\delta_{{n_{N}},{m_{N}}}}}\end{array}}\right|}$
$\displaystyle+$
$\displaystyle\frac{{{\alpha_{0}}}}{{\sqrt{2}}N}\sum\limits_{i=1}^{N}{\sqrt{{n_{i}}+0}\left|{\begin{array}[]{*{20}{c}}{{\delta_{{n_{1}},{m_{1}}}}}&{{\delta_{{n_{i}}-1,{m_{1}}}}}&{{\delta_{{n_{N}},{m_{1}}}}}\\\
{{\delta_{{n_{1}},{m_{i}}}}}&{{\delta_{{n_{i}}-1,{m_{i}}}}}&{{\delta_{{n_{N}},{m_{i}}}}}\\\
{{\delta_{{n_{1}},{m_{N}}}}}&{{\delta_{{n_{i}}-1,{m_{N}}}}}&{{\delta_{{n_{N}},{m_{N}}}}}\end{array}}\right|}.$

Only the calculation of $x_{i}$ is given and the result in section II can be
obtained by summing over all $x_{i}$.

##  Appendix B Density distribution and ROBDM

The original expression of Eq. (III) is

$\displaystyle D_{mn}=$
$\displaystyle\int\prod\limits_{i=2}^{N}{{\rm{d}}{x_{i}}}{{\psi_{m}}\left({x,\cdots,{x_{N}}}\right){\psi_{n}}\left({x,\cdots,{x_{N}}}\right)}$
$\displaystyle=$
$\displaystyle\int\prod\limits_{i=2}^{N}{{\rm{d}}{x_{i}}}{\frac{1}{{N!}}}\left({\sum\limits_{P}{{\varepsilon_{P}}{\varphi_{{p_{1}}}}\left(x\right)\cdots{\varphi_{{p_{N}}}}\left({{x_{N}}}\right)}}\right)$
$\displaystyle\times\qquad\left({\sum\limits_{Q}{{\varepsilon_{Q}}{\varphi_{{q_{1}}}}\left(x\right)\cdots{\varphi_{{q_{N}}}}\left({{x_{N}}}\right)}}\right),$

where ${\varepsilon_{P}}$ (${\varepsilon_{Q}}$) is the signature of
$P=\left({{p_{1}},\cdots,{p_{N}}}\right)$
(Q=$\left({{q_{1}},\cdots,{q_{N}}}\right)$) which corresponds to the
permutation of the occupation configuration
$\left({{n_{1}},{n_{2}},\cdots,{n_{N}}}\right)$ (
$\left({{m_{1}},{m_{2}},\cdots,{m_{N}}}\right)$) for
$\left|\psi_{m}\right\rangle$ ($\left|\psi_{n}\right\rangle$). Due to the
orthogonality of the single particle wave function $\varphi_{l}(x)$, the
integral will be not zero only in two cases. For the case of
$\left|{\psi_{m}}\right\rangle=\left|{\psi_{n}}\right\rangle$, the summation
term is nonzero only for the term of $P=Q$. In other cases, $N-1$ particles
must occupy in the same single particle levels for
$\left|{\psi_{m}}\right\rangle$ and $\left|{\psi_{n}}\right\rangle$, i.e.,
only one element in the set of ${n_{i}}$ is not same as those in the set of
${m_{j}}$.

Finally, we give a simple calculation of equation (5) as following

$\displaystyle P_{mn}=$
$\displaystyle\int{{\psi_{m}}\left({x,\cdots,{x_{N}}}\right){\psi_{n}}\left({y,\cdots,{x_{N}}}\right)}$
$\displaystyle\prod\limits_{j=2}^{N}{{\rm{sign}}\left({x-{x_{j}}}\right){\rm{sign}}\left({y-{x_{j}}}\right)}\prod\limits_{i=2}^{N}{{\rm{d}}{x_{i}}}$
$\displaystyle=$
$\displaystyle\int\prod\limits_{j=2}^{N-1}{{\rm{sign}}\left({x-{x_{j}}}\right){\rm{sign}}\left({y-{x_{j}}}\right)}{\prod\limits_{i=2}^{N-1}{{\rm{d}}{x_{i}}}}$
$\displaystyle\quad\int_{-\infty}^{+\infty}{{\psi_{m}}\left({x,\cdots,{x_{N}}}\right){\psi_{n}}\left({y,\cdots,{x_{N}}}\right)}{\rm{d}}{x_{N}}$
$\displaystyle-$ $\displaystyle
2\int\prod\limits_{j=2}^{N-1}{{\rm{sign}}\left({x-{x_{j}}}\right){\rm{sign}}\left({y-{x_{j}}}\right)}{\prod\limits_{i=2}^{N-1}{{\rm{d}}{x_{i}}}}$
$\displaystyle\quad\int_{x}^{y}{{\psi_{m}}\left({x,\cdots,{x_{N}}}\right){\psi_{n}}\left({y,\cdots,{x_{N}}}\right)}{\rm{d}}{x_{N}},$

where the signature on $x_{N}$ has been removed. Repeating the above process
we can have the formula in the main text. To show the process of the above
calculation more clearly, we give the example $P_{12}$ for two particles
system, i.e., $\left|\psi_{1}\right\rangle=\left|{0,1}\right\rangle$ and
$\left|\psi_{2}\right\rangle=\left|{0,2}\right\rangle$

$\displaystyle\int_{-\infty}^{+\infty}$
$\displaystyle{{\psi_{1}}\left({x,{x_{2}}}\right)}{\psi_{2}}\left({y,{x_{2}}}\right){\rm{sign}}\left({x-{x_{2}}}\right){\rm{sign}}\left({y-{x_{2}}}\right){\rm{d}}{x_{2}}$
$\displaystyle=\int_{-\infty}^{+\infty}{{\psi_{1}}\left({x,{x_{2}}}\right)}{\psi_{2}}\left({y,{x_{2}}}\right){\rm{d}}{x_{2}}$
$\displaystyle\quad-2\int_{x}^{y}{{\psi_{1}}\left({x,{x_{2}}}\right)}{\psi_{2}}\left({y,{x_{2}}}\right){\rm{d}}{x_{2}}$
$\displaystyle={\varphi_{0}}\left(x\right){\varphi_{0}}\left(y\right)\left[{0-2\int_{x}^{y}{{\varphi_{1}}\left({{x_{2}}}\right)}{\varphi_{2}}\left({{x_{2}}}\right){\rm{d}}{x_{2}}}\right]$
$\displaystyle-{\varphi_{0}}\left(x\right){\varphi_{2}}\left(y\right)\left[{0-2\int_{x}^{y}{{\varphi_{1}}\left({{x_{2}}}\right)}{\varphi_{0}}\left({{x_{2}}}\right){\rm{d}}{x_{2}}}\right]$
$\displaystyle-{\varphi_{1}}\left(x\right){\varphi_{0}}\left(y\right)\left[{0-2\int_{x}^{y}{{\varphi_{0}}\left({{x_{2}}}\right)}{\varphi_{2}}\left({{x_{2}}}\right){\rm{d}}{x_{2}}}\right]$
$\displaystyle+{\varphi_{1}}\left(x\right){\varphi_{2}}\left(y\right)\left[{1-2\int_{x}^{y}{{\varphi_{0}}\left({{x_{2}}}\right)}{\varphi_{0}}\left({{x_{2}}}\right){\rm{d}}{x_{2}}}\right].$

## References

  * Eckardt [2017a] A. Eckardt, Rev. Mod. Phys. 89, 011004 (2017a).
  * Sorensen  _et al._ [2005] A. S. Sorensen, E. Demler, and M. D. Lukin, Phys. Rev. Lett. 94, 086803 (2005).
  * Lignier  _et al._ [2007a] H. Lignier, C. Sias, D. Ciampini, Y. Singh, A. Zenesini, O. Morsch, and E. Arimondo, Phys. Rev. Lett. 99, 220403 (2007a).
  * Eckardt  _et al._ [2009a] A. Eckardt, M. Holthaus, H. Lignier, A. Zenesini, D. Ciampini, O. Morsch, and E. Arimondo, Phys. Rev. A 79, 013611 (2009a).
  * Zenesini  _et al._ [2009a] A. Zenesini, H. Lignier, D. Ciampini, O. Morsch, and E. Arimondo, Phys. Rev. Lett. 102, 100403 (2009a).
  * Jotzu  _et al._ [2014a] G. Jotzu, M. Messer, T. U. R. Desbuquois, M. Lebrat, D. Greif, and T. Esslinger, Nature (London) 515, 237 (2014a).
  * Aidelsburger  _et al._ [2015a] M. Aidelsburger, M. Lohse, C. Schweizer, M. Atala, J. T. Barreiro, S. Nascimbéne, N. R. Cooper, I. Bloch, and N. Goldman, Nat. Phys. 11, 162 (2015a).
  * Wintersperger  _et al._ [2020a] K. Wintersperger, C. Braun, F. NurÜnal, A. Eckardt, M. D. Liberto, N. Goldman, I. Bloch, and M. Aidelsburger, Nat. Phys. 16, 1058 (2020a).
  * Eckardt [2017b] A. Eckardt, Rev. Mod. Phys. 89, 011004 (2017b).
  * Sorensen  _et al._ [2005] A. S. Sorensen, E. Demler, and M. Lukin, Phys. Rev. Lett. 94, 086803 (2005).
  * Lignier  _et al._ [2007b] H. Lignier, C. Sias, D. Ciampini, Y. Singh, A. Zenesini, O. Morsch, and E. Arimondo, Phys. Rev. Lett. 99, 220403 (2007b).
  * Eckardt  _et al._ [2009b] A. Eckardt, M. Holthaus, H. Lignier, A. Zenesini, D. Ciampini, O. Morsch, and E. Arimondo, Phys. Rev. A 79, 013611 (2009b).
  * Zenesini  _et al._ [2009b] A. Zenesini, H. Lignier, D. Ciampini, O. Morsch, and E. Arimondo, Phys. Rev. Lett. 102, 100403 (2009b).
  * Jotzu  _et al._ [2014b] G. Jotzu, M. Messer, T. U. R. Desbuquois, M. Lebrat, D. Greif, and T. Esslinger, Nature 515, 237 (2014b).
  * Aidelsburger  _et al._ [2015b] M. Aidelsburger, M. Lohse, C. Schweizer, M. Atala, J. T. Barreiro, S. Nascimbéne, N. R. Cooper, I. Bloch, and N. Goldman, Nat. Phys. 11, 162 (2015b).
  * Wintersperger  _et al._ [2020b] K. Wintersperger, C. Braun, F. NurÜnal, A. Eckardt, M. D. Liberto, N. Goldman, I. Bloch, and M. Aidelsburger, Nat. Phys. 16, 1059 (2020b).
  * Colcelli  _et al._ [2019] A. Colcelli, G. Mussardo, G. Sierra, and A. Trombettoni, Phys. Rev. Lett. 123, 130401 (2019).
  * Colcelli  _et al._ [2020] A. Colcelli, G. Mussardo, G. Sierra, and A. Trombettoni, Phys. Rev. A 102, 033310 (2020).
  * Oka and Kitamura [2019] T. Oka and S. Kitamura, Ann. Rev. Cond. Mat. Phys. 10, 387 (2019).
  * Görg  _et al._ [2018] F. Görg, M. Messer, K. Sandholzer, G. Jotzu, R. Desbuquois, and T. Esslinger, Nature 553, 481 (2018).
  * Kaur  _et al._ [2024] P. Kaur, K. Suthar, D. Angom, and S. Gautam, Phys. Rev. A 109, 013308 (2024).
  * Quinn and Haque [2014] E. Quinn and M. Haque, Phys. Rev. A 90, 053609 (2014).
  * Atas  _et al._ [2020] Y. Y. Atas, A. Safavi-Naini, and K. V. Kheruntsyan, Phys. Rev. A 102, 043312 (2020).
  * Martirosyan  _et al._ [2024] G. Martirosyan, C. Ho, J. Etrych, Z. Y, A. Cao, Z. Hadzibabic, and C. Eigen, Phys. Rev. Lett. 132, 113401 (2024).
  * Chin  _et al._ [2010] C. Chin, R. Grimm, P. Julienne, and E. Tiesinga, Rev. Mod. Phys. 82, 1225 (2010).
  * Haller  _et al._ [2010] E. Haller, M. J. Mark, R. Hart, J. G. Danzl, L. Reichsöllner, V. Melezhik, P. Schmelcher, and H.-C. Nägerl, Phys. Rev. Lett. 104, 153203 (2010).
  * Paredes  _et al._ [2004] B. Paredes, A. Widera, V. Murg, O. Mandel, S. Fölling, I. Cirac, G. V. Shlyapnikov, T. W. Hänsch, and I. Bloch, Nature 429, 277 (2004).
  * Kinoshita  _et al._ [2004] T. Kinoshita, T. Wenger, and D. S. Weiss, Science 305, 1125 (2004).
  * van Druten and Ketterle [1997] N. J. van Druten and W. Ketterle, Phys. Rev. Lett. 79, 549 (1997).
  * Jacqmin  _et al._ [2011] T. Jacqmin, J. Armijo, T. Berrada, K. V. Kheruntsyan, and I. Bouchoule, Phys. Rev. Lett. 106, 230405 (2011).
  * Cazalilla  _et al._ [2011] M. A. Cazalilla, R. Citro, T. Giamarchi, E. Orignac, and M. Rigol, Rev. Mod. Phys. 83, 1405 (2011).
  * Imambekov  _et al._ [2012] A. Imambekov, T. L. Schmidt, and L. I. Glazman, Rev. Mod. Phys. 84, 1253 (2012).
  * Guan  _et al._ [2013] X.-W. Guan, M. T. Batchelor, and C. Li, Rev. Mod. Phys. 85, 1633 (2013).
  * Dalfovo and Stringari [1995] F. Dalfovo and S. Stringari, Phys. Rev. A 53, 4 (1995).
  * Smerzi  _et al._ [1997] A. Smerzi, S. Fantoni, S. Giovanazzi, and S. Shenoy2, Phys. Rev. Lett. 79, 25 (1997).
  * Scopa  _et al._ [2023] S. Scopa, P. Ruggiero, P. Calabrese, and J. Dubail, Phys. Rev. A 108, 013324 (2023).
  * Tonks [1936] L. Tonks, Phys. Rev. 50, 955 (1936).
  * Girardeau [1960] M. Girardeau, J. Math. Phys. 1, 516 (1960).
  * Moreno [2009] G. Moreno, Phys. Lett. A 373, 3897 (2009).
  * Malvania  _et al._ [2021] N. Malvania, Y. Zhang, Y. Le, J. Dubail, M. Rigol, and D. S. Weiss, Science 373, 1129 (2021).
  * Hasan  _et al._ [2024] M. Hasan, T. Fogarty, J. Li, A. Ruschhaupt, and T. Busch, arXiv:2402.00349v4 (2024).
  * Odelli  _et al._ [2023] M. Odelli, V. Stojanović, and A. Ruschhaupt, Phys. Rev. Appl. 20, 054038 (2023).
  * Kao  _et al._ [2021] W. Kao, K.-Y. Li, K.-Y. Lin, S. Gopalakrishnan, and B. L. Lev, Topological pumping of a 1d dipolar gas into strongly correlated prethermal states, Science 371, 296 (2021).
  * Buljan  _et al._ [2007] H. Buljan, K. Lelas, R. Pezer, and M. Jablan, Phys. Rev. A 76, 043609 (2007).
  * Pezer and Buljan [2007] R. Pezer and H. Buljan, Phys. Rev. Lett. 98, 240403 (2007).
  * Chakrabarti  _et al._ [2024] B. Chakrabarti, A. Gammal, N. Chavda, and M. Lekala, arXiv:2402.00372 (2024).
  * Hao [2023] Y. Hao, Eur. Phys. J. D 77, 127 (2023).


This construction, which will be described in more detail in the following,
also works out for the variants of B-TSO where player B is allowed to update
either only before or only after her move. In the former case, this is clear,
since the construction never requires her to perform an update between her
move and the next one of player A. In the latter case, this is due to the fact
that the construction gives her enough opportunities to update during
auxiliary $\mathtt{skip}$ transitions, which would not be needed in the B-TSO
game with full buffer control.

In particular, consider the transition
$\mathsf{q}_{1}\mathop{\xrightarrow{~{}\mathtt{rd}(\mathsf{x}_{\mathtt{wr}},\mathsf{m})~{}}}\mathsf{q}_{\mathsf{m}}$
in $\mathsf{Proc}^{2}$ as an example. If player B wants to take this
transition while the $\langle\mathsf{x}_{\mathtt{wr}},\mathsf{m}\rangle$
message is still in the buffer, she can instead move to $\mathsf{h}_{1}$ and
perform an update after her move. Player A then immediately needs to respond
with going back to $\mathsf{q}_{1}$, since $\mathsf{q}_{F}$ is winning for
player B. For the same reason, player A cannot transition to $\mathsf{h}_{1}$
herself, which prevents the potential of entering an infinite loop.

Furthermore, consider $\mathsf{q}_{L}$ in $\mathsf{Proc}^{2}$. Note that it is
immediately losing for player B, since the final state $\mathsf{q}_{F}$ is not
reachable from there.

######  Theorem 8.

Consider the B-TSO game or one of its variants. The set of final states
$\mathsf{S}_{F}$ of $\mathcal{L}$ is reachable from
$\mathsf{s}_{0}\in\mathsf{S}$ if and only if player B wins the game
$\mathcal{G}(\mathcal{P},\mathsf{Q}_{F}^{\mathcal{P}})$ starting from the
configuration
$\mathsf{c}_{0}=\langle\langle\mathsf{s}_{0},\mathsf{q}_{1}\rangle,\langle\varepsilon,\varepsilon\rangle,\\{\mathsf{x}_{\mathtt{wr}}\mapsto\bot,\mathsf{x}_{\mathtt{rd}}\mapsto\bot,\mathsf{y}\mapsto
0\\}\rangle_{B}\in\mathsf{C}_{B}$.

###  C.1 From $\mathcal{L}$-Reachability to a Winning Strategy in B-TSO

Proceeding as in the case of A-TSO games, suppose $\mathsf{S}_{F}$ is
reachable from $\mathsf{s}_{0}$. Given a run
$\mathsf{c}_{0}^{\mathcal{L}},\dots,\mathsf{c}_{n}^{\mathcal{L}}$ in the PCS,
recall the definitions of $\mathsf{c}_{k}^{\mathcal{L}}$ in Appendix B. For
all $k=0,\dots,n$, we define a game configuration
$\mathsf{c}_{k}=\langle\mathcal{S}_{k},\mathcal{B}_{k},\mathcal{M}_{k}\rangle_{B}$:

  1. 1.

$\mathcal{S}_{k}=\langle\mathsf{s}_{k},\mathsf{q}_{1}\rangle$

  2. 2.

$\mathcal{B}_{k}=\langle\langle\langle\mathsf{y},1\rangle,\langle\mathsf{x}_{\mathtt{wr}},\mathsf{w}_{k}[1]\rangle,\dots,\langle\mathsf{y},1\rangle,\langle\mathsf{x}_{\mathtt{wr}},\mathsf{w}_{k}[|\mathsf{w}_{k}|]\rangle,\langle\mathsf{y},1\rangle\rangle,\varepsilon\rangle$

  3. 3.

$\mathcal{M}_{k}=\\{\mathsf{x}_{\mathtt{wr}}\mapsto\bot,\mathsf{x}_{\mathtt{rd}}\mapsto\bot,\mathsf{y}\mapsto
0\\}$

We describe a strategy for player B that forces the play into visiting all
configurations $\mathsf{c}_{1},\dots,\mathsf{c}_{n}$. Since
$\mathsf{c}_{n}\in\mathsf{C}_{F}$, this means that the strategy is winning. To
achieve this, we show by induction over k that starting from $\mathsf{c}_{0}$,
Player B can force a play that visits either $\mathsf{c}_{k}$ or
$\mathsf{C}_{F}$. For $k=0$, this is true since $\mathsf{c}_{0}$ is the
initial configuration. Let the induction hypothesis be that the claim holds
true for some arbitrary but fixed $0\leq k<n$. For the induction step, we can
assume that the game is in configuration $\mathsf{c}_{k}$.

In the following, we assume that player A avoids immediate defeats. This does
not lose generality, since otherwise the game would be in $\mathsf{C}_{F}$ and
the induction would still hold.

If $\mathsf{op}_{k+1}=\mathtt{skip}$, then player B first takes the transition
$\mathsf{s}_{k}\mathop{\xrightarrow{~{}\mathtt{skip}~{}}}\mathsf{h}$ in
$\mathsf{Proc}^{1}$. Since all other outgoing transitions are disabled, player
A has to follow up with the transition
$\mathsf{h}\mathop{\xrightarrow{~{}\mathtt{skip}~{}}}\mathsf{s}_{k+1}$. As
there is no change in the states of $\mathsf{Proc}^{2}$, the buffers, or the
memory, we can conclude that the current configuration of the game is
$\mathsf{c}_{k+1}$.

Next, consider the case where $\mathsf{op}_{k+1}=!\mathsf{m}$, which is
similar to the previous one. Player B takes
$\mathsf{s}_{k}\mathop{\xrightarrow{~{}\mathtt{wr}(\mathsf{x}_{\mathtt{wr}},\mathsf{m})~{}}}\mathsf{h}$
and the only option for player A is
$\mathsf{h}\mathop{\xrightarrow{~{}\mathtt{wr}(\mathsf{y},1)~{}}}\mathsf{s}_{k+1}$.
The buffer of $\mathsf{Proc}^{1}$ has now two additional pending write
operations, which correspond to the channel message $\mathsf{m}$, i.e. the
last letter of $\mathsf{w}_{k+1}$. Thus, the game is in configuration
$\mathsf{c}_{k+1}$.

The last case is where $\mathsf{op}_{k+1}=?\mathsf{m}$, which is more
complicated. Player B starts by updating the message
$\langle\mathsf{x}_{\mathtt{wr}},\mathsf{m}\rangle$ and taking the transition
$\mathsf{q}_{1}\mathop{\xrightarrow{~{}\mathtt{rd}(\mathsf{x}_{\mathtt{wr}},\mathsf{m})~{}}}\mathsf{q}_{\mathsf{m}}$
in $\mathsf{Proc}^{2}$ (recall the remark about the B-TSO variants above – she
might need to take a detour over $\mathsf{h}_{1}$). Player A has to respond
with
$\mathsf{q}_{\mathsf{m}}\mathop{\xrightarrow{~{}\mathtt{wr}(\mathsf{x}_{\mathtt{rd}},\mathsf{m})~{}}}\mathsf{q}_{3}$,
since otherwise player B could move to $\mathsf{q}_{F}$ and win. Now, player B
is in a similar situation, where she needs to leave $\mathsf{q}_{3}$, or else
player A can move to $\mathsf{q}_{L}$ which prevents the game from ever
reaching $\mathsf{q}_{F}$. So, player B empties the buffer of
$\mathsf{Proc}^{2}$ (possibly using $\mathsf{h}_{2}$) and takes the transition
$\mathsf{q}_{3}\mathop{\xrightarrow{~{}\mathtt{mf}~{}}}\mathsf{q}_{4}$. Player
A has to respond with
$\mathsf{q}_{4}\mathop{\xrightarrow{~{}\mathtt{wr}(\mathsf{x}_{\mathtt{wr}},\bot)~{}}}\mathsf{q}_{5}$.
At this point, player B cannot further proceed in $\mathsf{Proc}^{2}$, since
player A could respond with
$\mathsf{q}_{6}\mathop{\xrightarrow{~{}\mathtt{skip}~{}}}\mathsf{q}_{L}$ and
win. Thus, she has to continue in $\mathsf{Proc}^{1}$ instead, where the only
enabled transition is
$\mathsf{s}_{k}\mathop{\xrightarrow{~{}\mathtt{rd}(\mathsf{x}_{\mathtt{rd}},\mathsf{m})~{}}}\mathsf{h}$.
Now, $\mathsf{Proc}^{1}$ is disabled and the play continues in
$\mathsf{Proc}^{2}$. Eventually, it will go through all states
$\mathsf{q}_{6},\dots,\mathsf{q}_{14}$. Note that player B has to update the
messages $\langle\mathsf{x}_{\mathtt{wr}},\bot\rangle$,
$\langle\mathsf{y},1\rangle$, $\langle\mathsf{y},0\rangle$ and
$\langle\mathsf{x}_{\mathtt{rd}},\bot\rangle$ along the way, and has enough
opportunities to do so. Finally, player B takes the transition
$\mathsf{q}_{14}\mathop{\xrightarrow{~{}\mathtt{mf}~{}}}\mathsf{q}_{1}$ in
$\mathsf{Proc}^{2}$ and player A is forced to respond with
$\mathsf{h}\mathop{\xrightarrow{~{}\mathtt{rd}(\mathsf{x}_{\mathtt{rd}},\bot)~{}}}\mathsf{s}_{k+1}$
in $\mathsf{Proc}^{1}$. Note that the last transition is enabled since the
$\langle\mathsf{x}_{\mathtt{rd}},\bot\rangle$-message has certainly reached
the memory.

To summarise the changes: $\mathsf{Proc}^{1}$ transitioned from
$\mathsf{s}_{k}$ to $\mathsf{s}_{k+1}$, while $\mathsf{Proc}^{2}$ is back in
state $\mathsf{q}_{1}$. The buffer of $\mathsf{Proc}^{1}$ has updated its two
oldest messages, which correspond to the last letter in $\mathsf{w}_{k}$, and
the buffer of $\mathsf{Proc}^{2}$ has been emptied. All variables have their
default values.

We conclude that the game is in configuration $\mathsf{c}_{k+1}$, which
completes the proof by induction. In summary, starting from $\mathsf{c}_{0}$,
the game either reaches the configuration $\mathsf{c}_{n}\in\mathsf{C}_{F}$,
or another configuration in $\mathsf{C}_{F}$. In the latter case, player B
already won, but in the former case, she takes the transition
$\mathsf{s}_{n}\mathop{\xrightarrow{~{}\mathtt{wr}(\mathsf{x}_{\mathtt{wr}},\top)~{}}}\mathsf{h}_{F}$,
updates this message, and finally reaches
$\mathsf{q}_{1}\mathop{\xrightarrow{~{}\mathtt{rd}(\mathsf{x}_{\mathtt{wr}},\top)~{}}}\mathsf{q}_{F}\in\mathsf{Q}_{F}^{\mathcal{P}}$
in her next turn.

###  C.2 From a Winning Strategy in B-TSO to $\mathcal{L}$-Reachability

For the other direction, suppose that player B has a winning strategy.
Consider a strategy of player A that avoids reaching
$\mathsf{q}_{F}\in\mathsf{Q}^{2}\cap\mathsf{Q}_{F}^{\mathcal{P}}$ whenever
possible. Furthermore, to support our argumentation we can assume arbitrary
behaviour of player A, since the strategy of player B must be winning in any
case.

Let $\mathsf{s}_{0},\dots,\mathsf{s}_{n}$ be the sequence of channel states
that are visited by $\mathsf{Proc}^{1}$ during the run induced by these two
strategies. Since player B uses a winning strategy, this sequence is finite.
We will show by induction that for each $k=0,\dots,n$, the run contains the
game configuration
$\mathsf{c}_{k}=\langle\mathcal{S}_{k},\mathcal{B}_{k},\mathcal{M}_{k}\rangle_{B}\in\mathsf{C}_{B}$,
where:

  1. 1.

$\mathcal{S}_{k}=\langle\mathsf{s}_{k},\mathsf{q}_{1}\rangle$

  2. 2.

$\mathcal{B}_{k}=\langle\langle\langle\mathsf{y},1\rangle,\langle\mathsf{x}_{\mathtt{wr}},\mathsf{w}_{k}[1]\rangle,\dots,\langle\mathsf{y},1\rangle,\langle\mathsf{x}_{\mathtt{wr}},\mathsf{w}_{k}[|\mathsf{w}_{k}|]\rangle\rangle,\varepsilon\rangle$,
where $\mathsf{w}_{k}\in\mathsf{M}^{*}$

  3. 3.

$\mathcal{M}_{k}=\\{\mathsf{x}_{\mathtt{wr}}\mapsto\bot,\mathsf{x}_{\mathtt{rd}}\mapsto\bot,\mathsf{y}\mapsto
0\\}$

  4. 4.

If $k>0$, there is a label $\mathsf{op}_{k}$ such that
$\langle\mathsf{s}_{k-1},\mathsf{w}_{k-1}\rangle\mathop{\xrightarrow{~{}\mathsf{op}_{k}~{}}}_{\mathcal{L}}\
\langle\mathsf{s}_{k},\mathsf{w}_{k}\rangle$.

The induction base case clearly holds true, since $\mathsf{c}_{0}$ is the
initial configuration of the game. So, suppose that the claim holds for some
arbitrary but fixed $0\leq k<n$. By the induction hypothesis, we can assume
that the game is in configuration $\mathsf{c}_{k}$. Consider the different
moves player B can make.

First, she may take a transition
$\mathsf{s}_{k}\mathop{\xrightarrow{~{}\mathtt{skip}~{}}}\mathsf{h}$. She
surely does not update any buffer messages during that move, since this would
enable player A to take
$\mathsf{q}_{1}\mathop{\xrightarrow{~{}\mathtt{rd}(\mathsf{x}_{\mathtt{wr}},\mathsf{m})~{}}}\mathsf{q}_{L}$
and win. So, we assume that player A moves along
$\mathsf{h}\mathop{\xrightarrow{~{}\mathtt{skip}~{}}}\mathsf{s}^{\prime}$. By
the construction of $\mathsf{Proc}^{1}$, the path
$\mathsf{s}_{k}\mathop{\xrightarrow{~{}\mathtt{skip}~{}}}\mathsf{h}\mathop{\xrightarrow{~{}\mathtt{skip}~{}}}\mathsf{s}^{\prime}$
implies the existence of a transition
$\mathsf{s}_{k}\mathop{\xrightarrow{~{}\mathtt{skip}~{}}}_{\mathcal{L}}\mathsf{s}^{\prime}$.
We define $\mathsf{s}_{k+1}:=\mathsf{s}^{\prime}$ and
$\mathsf{w}_{k+1}:=\mathsf{w}_{k}$ and conclude that the game is now in
configuration $\mathsf{c}_{k+1}$.

Another option for player A is to take the transition
$\mathsf{s}_{k}\mathop{\xrightarrow{~{}\mathtt{wr}(\mathsf{x}_{\mathtt{wr}},\mathsf{m})~{}}}\mathsf{h}$.
The argumentation continues exactly as in the previous paragraph, the only
difference is that
$\mathsf{s}_{k}\mathop{\xrightarrow{~{}!\mathsf{m}~{}}}_{\mathcal{L}}\mathsf{s}^{\prime}$
and $\mathsf{w}_{k+1}:=\mathsf{m}\bullet\mathsf{w}_{k}$.

Since all other transitions in $\mathsf{Proc}^{1}$ are disabled, the last
possibility for player B to move is in $\mathsf{Proc}^{2}$. She first has to
update a $\langle\mathsf{x}_{\mathtt{wr}},\mathsf{m}\rangle$-message to the
memory (potentially using the loop through $\mathsf{h}_{1}$), and then she is
able to perform
$\mathsf{q}_{1}\mathop{\xrightarrow{~{}\mathtt{rd}(\mathsf{x}_{\mathtt{wr}},\mathsf{m})~{}}}\mathsf{q}_{\mathsf{m}}$.
Assume that player A responds with
$\mathsf{q}_{\mathsf{m}}\mathop{\xrightarrow{~{}\mathtt{wr}(\mathsf{x}_{\mathtt{rd}},\mathsf{m})~{}}}\mathsf{q}_{3}$.
Since staying in $\mathsf{q}_{3}$ is losing for player B, she needs to update
the $\langle\mathsf{x}_{\mathtt{rd}},\mathsf{m}\rangle$-message to the memory,
which enables
$\mathsf{q}_{3}\mathop{\xrightarrow{~{}\mathtt{skip}~{}}}\mathsf{q}_{4}$ in
$\mathsf{Proc}^{2}$. Player A is now forced to proceed from there and takes
$\mathsf{q}_{4}\mathop{\xrightarrow{~{}\mathtt{wr}(\mathsf{x}_{\mathtt{wr}},\bot)~{}}}\mathsf{q}_{5}$.

At this point, player B cannot continue in $\mathsf{Proc}^{2}$, since moving
to $\mathsf{q}_{6}$ opens up the opportunity for player A to immediately force
her win. However, also in $\mathsf{Proc}^{1}$ she has limited possibilities.
In case she starts to simulate a skip or send operation, player A can react
with
$\mathsf{h}\mathop{\xrightarrow{~{}\mathtt{rd}(\mathsf{x}_{\mathtt{rd}},\mathsf{m})~{}}}\mathsf{q}_{L}$
and win. Since player B employs a winning strategy, we conclude that at least
one transition
$\mathsf{s}_{k}\mathop{\xrightarrow{~{}\mathtt{rd}(\mathsf{x}_{\mathtt{rd}},\mathsf{m})~{}}}\mathsf{h}$
is enabled, which player B takes. Player A then has to proceed in
$\mathsf{Proc}^{2}$ and the play continues there until reaching
$\mathsf{q}_{14}$.

We note the following observations, based on the fact that player A cannot
force a win. First, in $\mathsf{q}_{7}$, the variable $\mathsf{y}$ apparently
has value $0$. This means that up to this point, no message from the buffer of
$\mathsf{Proc}^{1}$ has been updated (other than the single
$\langle\mathsf{x}_{\mathtt{wr}},\mathsf{m}\rangle$ from before). Second,
between $\mathsf{q}_{8}$ and $\mathsf{q}_{9}$, the value of $\mathsf{y}$ is
$1$. We conclude that at least one $\langle\mathsf{y},1\rangle$-message has
been updated. Third, in $\mathsf{q}_{11}$, player A reads $\bot$ from
$\mathsf{x}_{\mathtt{wr}}$. This shows that since the transition
$\mathsf{q}_{6}\mathop{\xrightarrow{~{}\mathtt{mf}~{}}}\mathsf{q}_{7}$, no
further $\langle\mathsf{x}_{\mathtt{wr}},\mathsf{m}^{\prime}\rangle$-message
has been updated. In summary, we conclude that during the whole process,
exactly the two messages $\langle\mathsf{x}_{\mathtt{wr}},\mathsf{m}\rangle$
and $\langle\mathsf{y},1\rangle$ have been updated to the memory.

We continue with the execution from $\mathsf{q}_{14}$. Player B empties the
buffer of $\mathsf{Proc}^{2}$ and takes either
$\mathsf{h}\mathop{\xrightarrow{~{}\mathtt{rd}(\mathsf{x}_{\mathtt{rd}},\bot)~{}}}\mathsf{s}^{\prime}$
in $\mathsf{Proc}^{1}$ or
$\mathsf{q}_{14}\mathop{\xrightarrow{~{}\mathtt{mf}~{}}}\mathsf{q}_{1}$ in
$\mathsf{Proc}^{2}$. We assume that player A takes the other one,
respectively.

We define $\mathsf{s}_{k+1}:=\mathsf{s}^{\prime}$ and $\mathsf{w}_{k+1}$ by
$\mathsf{w}_{k+1}\bullet\mathsf{m}:=\mathsf{w}_{k}$. The path
$\mathsf{s}_{k}\mathop{\xrightarrow{~{}\mathtt{rd}(\mathsf{x}_{\mathtt{rd}},\mathsf{m})~{}}}\mathsf{h}\mathop{\xrightarrow{~{}\mathtt{rd}(\mathsf{x}_{\mathtt{rd}},\bot)~{}}}\mathsf{s}_{k+1}$
implies that
$\langle\mathsf{s}_{k},\mathsf{w}_{k}\rangle\mathop{\xrightarrow{~{}?\mathsf{m}~{}}}_{\mathcal{L}}\langle\mathsf{s}_{k+1},\mathsf{w}_{k+1}\rangle$.
Furthermore, the observations above imply that the game is in configuration
$\mathsf{c}_{k+1}$ as defined in the beginning. This concludes the proof by
induction.

Now, we investigate how the run can continue after $\mathsf{c}_{n}$. Player B
cannot start to simulate a skip or send operation, since we can assume that
player A will move to $\mathsf{s}^{\prime}$, which contradicts the initial
assumption that $\mathsf{s}_{n}$ is the last channel state visited in this
run. The same holds true for a receive operation: Following the argumentation
from above, we have already seen that player A can either force a win, or lead
the game into completing the simulation of the receive operation. The only
possibility left is that $\mathsf{s}_{n}$ is a final channel state and player
B takes the transition
$\mathsf{s}_{n}\mathop{\xrightarrow{~{}\mathtt{wr}(\mathsf{x}_{\mathtt{wr}},\top)~{}}}\mathsf{h}_{F}$.

In summary, we constructed a path through $\mathcal{L}$ from
$\langle\mathsf{s}_{0},\varepsilon\rangle$ to
$\langle\mathsf{s}_{n},\mathsf{w}_{n}\rangle$, where
$\mathsf{s}_{n}\in\mathsf{S}_{F}$. This shows that the set of final states of
$\mathcal{L}$ is reachable.

###  C.3 Undecidability

######  Theorem 9.

The safety problem for the B-TSO game is undecidable.

###### Proof.

This follows directly from Theorem 8 and the undecidability of the state
reachability problem for perfect channel systems [17]. ∎

##  Appendix D Undecidability of the AB-TSO game

In this final section we prove undecidability of the AB-TSO game, which is the
TSO game where the players share control over buffer updates in the way that
both of them are allowed to update exactly after their own move. The
construction will be very similar to the one for the B-TSO game. In
particular, $\mathsf{Proc}^{1}$ is exactly the same and is sketched in Figure
9. The construction for $\mathsf{Proc}^{2}$ on the other hand is different and
shown in Figure 11. Note that this process is deadlock-free by design. As
previously, the set of final states is defined as
$\mathsf{Q}_{F}^{\mathcal{P}}:=\\{\mathsf{q}_{F}\\}$. Note that
$\mathsf{q}_{L}$ in $\mathsf{Proc}^{2}$ is immediately losing for player B,
since the final state $\mathsf{q}_{F}$ is not reachable from there.

$\mathsf{q}_{1}$$\mathsf{q}_{2}$$\mathsf{q}_{\mathsf{m}}$$\mathsf{q}_{4}$$\mathsf{q}_{5}$$\mathsf{q}_{6}$$\mathsf{q}_{7}$$\mathsf{q}_{8}$$\mathsf{q}_{9}$$\mathsf{q}_{10}$$\mathsf{q}_{11}$$\mathsf{q}_{12}$$\mathsf{q}_{1}$$\mathtt{skip}$$\mathtt{rd}(\mathsf{x}_{\mathtt{wr}},\mathsf{m})$$\mathtt{wr}(\mathsf{x}_{\mathtt{rd}},\mathsf{m})$$\mathtt{wr}(\mathsf{x}_{\mathtt{wr}},\bot)$$\mathtt{skip}$$\mathtt{mf}$$\mathtt{skip}$$\mathtt{wr}(\mathsf{y},0)$$\mathtt{skip}$$\mathtt{mf}$$\mathtt{wr}(\mathsf{x}_{\mathtt{rd}},\bot)$$\mathtt{skip}$$\mathsf{q}_{F}$$\mathtt{skip}$$\mathtt{skip}$$\mathsf{q}_{L}$$\mathtt{skip}$$\mathtt{skip}$$\mathsf{q}_{F}$$\mathtt{skip}$$\mathtt{skip}$$\mathsf{q}_{L}$$\mathtt{skip}$$\mathtt{skip}$$\mathsf{q}_{L}$$\mathtt{skip}$$\mathtt{skip}$$\mathsf{q}_{F}$$\mathtt{rd}(\mathsf{x}_{\mathtt{wr}},\mathsf{m})$$\mathtt{skip}$$\mathsf{q}_{L}$$\mathtt{rd}(\mathsf{x}_{\mathtt{wr}},\mathsf{m})$$\mathtt{skip}$$\mathsf{q}_{L}$$\mathtt{rd}(\mathsf{x}_{\mathtt{wr}},\bot)$$\mathtt{rd}(\mathsf{y},1)$$\mathtt{skip}$$\mathsf{q}_{F}$$\mathtt{rd}(\mathsf{y},1)$$\mathtt{skip}$$\mathsf{q}_{L}$$\mathtt{rd}(\mathsf{y},1)$$\mathtt{skip}$$\mathsf{q}_{F}$$\mathtt{rd}(\mathsf{y},1)$$\mathtt{skip}$$\mathsf{q}_{L}$$\mathtt{rd}(\mathsf{y},1)$$\mathtt{skip}$$\mathsf{q}_{F}$$\mathtt{rd}(\mathsf{y},1)$$\mathtt{skip}$$\mathsf{q}_{L}$$\mathtt{rd}(\mathsf{y},1)$$\mathtt{skip}$$\mathsf{q}_{F}$$\mathtt{rd}(\mathsf{y},0)$$\mathtt{rd}(\mathsf{x}_{\mathtt{wr}},\mathsf{m})$$\mathtt{skip}$$\mathsf{q}_{L}$$\mathtt{rd}(\mathsf{x}_{\mathtt{wr}},\mathsf{m})$$\mathtt{skip}$$\mathsf{q}_{F}$$\mathtt{rd}(\mathsf{x}_{\mathtt{wr}},\mathsf{m})$$\mathtt{skip}$$\mathsf{q}_{L}$$\mathtt{rd}(\mathsf{x}_{\mathtt{wr}},\mathsf{m})$$\mathtt{skip}$$\mathsf{q}_{F}$$\mathtt{rd}(\mathsf{x}_{\mathtt{wr}},\mathsf{m})$$\mathtt{skip}$$\mathsf{q}_{F}$$\mathtt{rd}(\mathsf{x}_{\mathtt{wr}},\top)$$\mathtt{skip}$
Figure 11: $\mathsf{Proc}^{2}$ of the AB-TSO reduction from PCS

######  Theorem 10.

Consider the AB-TSO game. The set of final states $\mathsf{S}_{F}$ of
$\mathcal{L}$ is reachable from $\mathsf{s}_{0}\in\mathsf{S}$ if and only if
player B wins the game $\mathcal{G}(\mathcal{P},\mathsf{Q}_{F}^{\mathcal{P}})$
starting from the configuration
$\mathsf{c}_{0}=\langle\langle\mathsf{s}_{0},\mathsf{q}_{1}\rangle,\langle\varepsilon,\varepsilon\rangle,\\{\mathsf{x}_{\mathtt{wr}}\mapsto\bot,\mathsf{x}_{\mathtt{rd}}\mapsto\bot,\mathsf{y}\mapsto
0\\}\rangle_{B}\in\mathsf{C}_{B}$.

###  D.1 From $\mathcal{L}$-Reachability to a Winning Strategy in AB-TSO

Proceeding as in the case of the B-TSO games, suppose $\mathsf{S}_{F}$ is
reachable from $\mathsf{s}_{0}$. Given a run
$\mathsf{c}_{0}^{\mathcal{L}},\dots,\mathsf{c}_{n}^{\mathcal{L}}$ in the PCS,
recall the definitions of $\mathsf{c}_{k}^{\mathcal{L}}$ in Appendix B and of
$\mathsf{c}_{k}$ in Appendix C.

We describe a strategy for player B that forces the play into visiting all
configurations $\mathsf{c}_{1},\dots,\mathsf{c}_{n}$. Since
$\mathsf{c}_{n}\in\mathsf{C}_{F}$, this means that the strategy is winning. To
achieve this, we show by induction over k that starting from $\mathsf{c}_{0}$,
Player B can force a play that visits either $\mathsf{c}_{k}$ or
$\mathsf{C}_{F}$. For $k=0$, this is true since $\mathsf{c}_{0}$ is the
initial configuration. Let the induction hypothesis be that the claim holds
true for some arbitrary but fixed $0\leq k<n$. For the induction step, we can
assume that the game is in configuration $\mathsf{c}_{k}$.

In the following, we assume that player A avoids immediate defeats. This does
not lose generality, since otherwise the game would be in $\mathsf{C}_{F}$ and
the induction would still hold.

If $\mathsf{op}_{k+1}=\mathtt{skip}$, then player B first takes the transition
$\mathsf{s}_{k}\mathop{\xrightarrow{~{}\mathtt{skip}~{}}}\mathsf{h}$ in
$\mathsf{Proc}^{1}$. For player A, there are only two enabled transitions.
After
$\mathsf{q}_{1}\mathop{\xrightarrow{~{}\mathtt{skip}~{}}}\mathsf{q}_{2}$,
player B could move to $\mathsf{q}_{F}$ and win. Thus, player A has to follow
up with the transition
$\mathsf{h}\mathop{\xrightarrow{~{}\mathtt{skip}~{}}}\mathsf{s}_{k+1}$
instead. Suppose she also updates one or more messages after her move. Then,
player B could take
$\mathsf{q}_{1}\mathop{\xrightarrow{~{}\mathtt{rd}(\mathsf{x}_{\mathtt{wr}},\mathsf{m}^{\prime})~{}}}\mathsf{q}_{F}$
for some message $\mathsf{m}^{\prime}$ and win. So, we continue assuming that
player A does not update anything to the memory. As there is no change in the
states of $\mathsf{Proc}^{2}$, the buffers or the memory, we can conclude that
the current configuration of the game is $\mathsf{c}_{k+1}$.

Next, consider the case where $\mathsf{op}_{k+1}=!\mathsf{m}$, which is
similar to the previous one. Player B takes
$\mathsf{s}_{k}\mathop{\xrightarrow{~{}\mathtt{wr}(\mathsf{x}_{\mathtt{wr}},\mathsf{m})~{}}}\mathsf{h}$
and the only option for player A is
$\mathsf{h}\mathop{\xrightarrow{~{}\mathtt{wr}(\mathsf{y},1)~{}}}\mathsf{s}_{k+1}$.
As above, we argue that she does not perform any buffer updates. The buffer of
$\mathsf{Proc}^{1}$ has now two additional pending write operations, which
correspond to the channel message $\mathsf{m}$, i.e. the last letter of
$\mathsf{w}_{k+1}$. Thus, the game is in configuration $\mathsf{c}_{k+1}$.

The last case is where $\mathsf{op}_{k+1}=?\mathsf{m}$, which is more
complicated. Player B starts by taking the transition
$\mathsf{q}_{1}\mathop{\xrightarrow{~{}\mathtt{skip}~{}}}\mathsf{q}_{2}$ in
$\mathsf{Proc}^{2}$ and then updates the message
$\langle\mathsf{x}_{\mathtt{wr}},\mathsf{m}\rangle$ to the memory. Now, player
A is forced to leave $\mathsf{q}_{2}$, since otherwise player B could move to
$\mathsf{q}_{F}$ in her next turn. The only enabled transition from there is
$\mathsf{q}_{2}\mathop{\xrightarrow{~{}\mathtt{rd}(\mathsf{x}_{\mathtt{wr}},\mathsf{m})~{}}}\mathsf{q}_{3}$.
Again, we see that she cannot update any messages without losing in the very
next turn. Player B responds with
$\mathsf{q}_{3}\mathop{\xrightarrow{~{}\mathtt{wr}(\mathsf{x}_{\mathtt{rd}},\mathsf{m})~{}}}\mathsf{q}_{4}$,
which she immediately updates to the memory. As before, player A must leave
this state, the only option for this is to follow
$\mathsf{q}_{4}\mathop{\xrightarrow{~{}\mathtt{wr}(\mathsf{x}_{\mathtt{wr}},\bot)~{}}}\mathsf{q}_{5}$.
She does so without buffer updates. Now, player B takes the transition
$\mathsf{s}_{k}\mathop{\xrightarrow{~{}\mathtt{rd}(\mathsf{x}_{\mathtt{rd}},\mathsf{m})~{}}}\mathsf{h}$
in $\mathsf{Proc}^{1}$. She also empties the buffer of $\mathsf{Proc}^{2}$.
Player A has to continue in $\mathsf{Proc}^{2}$, since all outgoing
transitions in $\mathsf{Proc}^{1}$ are disabled. The only option is to go to
$\mathsf{q}_{6}$, as usual without performing any updates. Next, player B can
perform
$\mathsf{q}_{6}\mathop{\xrightarrow{~{}\mathtt{mf}~{}}}\mathsf{q}_{7}$, since
she emptied the buffer one turn earlier. Player A continues to
$\mathsf{q}_{8}$. If she does not perform any updates, or updates more than
one message, i.e. at least one $\langle\mathsf{y},1\rangle$ and one
$\langle\mathsf{x}_{\mathtt{wr}},\mathsf{m}\rangle$ buffer message (for some
channel message $\mathsf{m}$), then player B can immediately win in her next
turn. So, we proceed assuming that player A updates exactly one message
$\langle\mathsf{y},1\rangle$. Then, player B takes the transition
$\mathsf{q}_{8}\mathop{\xrightarrow{~{}\mathtt{wr}(\mathsf{y},0)~{}}}\mathsf{q}_{9}$
and immediately updates this message to the memory. This leaves player A with
the only possibility of moving to $\mathsf{q}_{10}$. As usual, she cannot
update any buffer message without losing. Player B continues with
$\mathsf{q}_{10}\mathop{\xrightarrow{~{}\mathtt{mf}~{}}}\mathsf{q}_{11}$.
Player A has to perform
$\mathsf{q}_{11}\mathop{\xrightarrow{~{}\mathtt{wr}(\mathsf{x}_{\mathtt{rd}},\bot)~{}}}\mathsf{q}_{12}$
and may update this message, but nothing else. Next, player B moves to
$\mathsf{q}_{1}$ and empties the buffer of $\mathsf{Proc}^{2}$. Since player A
cannot move to $\mathsf{q}_{2}$ without losing, she takes the transition
$\mathsf{h}\mathop{\xrightarrow{~{}\mathtt{rd}(\mathsf{x}_{\mathtt{rd}},\bot)~{}}}\mathsf{s}_{k+1}$.
This is enabled since the buffer of $\mathsf{Proc}^{2}$ was last emptied.

To summarise the changes: $\mathsf{Proc}^{1}$ transitioned from
$\mathsf{s}_{k}$ to $\mathsf{s}_{k+1}$, while $\mathsf{Proc}^{2}$ is back in
state $\mathsf{q}_{1}$. The buffer of $\mathsf{Proc}^{1}$ has updated its two
oldest messages, which correspond to the last letter in $\mathsf{w}_{k}$, and
the buffer of $\mathsf{Proc}^{2}$ has been emptied. All variables have their
default values.

We conclude that the game is in configuration $\mathsf{c}_{k+1}$, which
completes the proof by induction. In summary, starting from $\mathsf{c}_{0}$,
the game either reaches the configuration $\mathsf{c}_{n}\in\mathsf{C}_{F}$,
or another configuration in $\mathsf{C}_{F}$. In the latter case, player B
already won, but in the former case, she takes the transition
$\mathsf{s}_{n}\mathop{\xrightarrow{~{}\mathtt{wr}(\mathsf{x}_{\mathtt{wr}},\top)~{}}}\mathsf{h}_{F}$,
updates this message, and finally reaches
$\mathsf{q}_{1}\mathop{\xrightarrow{~{}\mathtt{rd}(\mathsf{x}_{\mathtt{wr}},\top)~{}}}\mathsf{q}_{F}\in\mathsf{Q}_{F}^{\mathcal{P}}$
in her next turn.

###  D.2 From a Winning Strategy in AB-TSO to $\mathcal{L}$-Reachability

For the other direction, suppose that player B has a winning strategy.
Consider a strategy of player A that avoids reaching
$\mathsf{q}_{F}\in\mathsf{Q}^{2}\cap\mathsf{Q}_{F}^{\mathcal{P}}$ whenever
possible. Furthermore, to support our argumentation we can assume arbitrary
behaviour of player A, since the strategy of player B must be winning in any
case.

Let $\mathsf{s}_{0},\dots,\mathsf{s}_{n}$ be the sequence of channel states
that are visited by $\mathsf{Proc}^{1}$ during the run induced by these two
strategies. Since player B uses a winning strategy, this sequence is finite.
We will show by induction that for each $k=0,\dots,n$, the run contains the
game configuration
$\mathsf{c}_{k}=\langle\mathcal{S}_{k},\mathcal{B}_{k},\mathcal{M}_{k}\rangle_{B}\in\mathsf{C}_{B}$,
where:

  1. 1.

$\mathcal{S}_{k}=\langle\mathsf{s}_{k},\mathsf{q}_{1}\rangle$

  2. 2.

$\mathcal{B}_{k}=\langle\langle\langle\mathsf{y},1\rangle,\langle\mathsf{x}_{\mathtt{wr}},\mathsf{w}_{k}[1]\rangle,\dots,\langle\mathsf{y},1\rangle,\langle\mathsf{x}_{\mathtt{wr}},\mathsf{w}_{k}[|\mathsf{w}_{k}|]\rangle\rangle,\varepsilon\rangle$,
where $\mathsf{w}_{k}\in\mathsf{M}^{*}$

  3. 3.

$\mathcal{M}_{k}=\\{\mathsf{x}_{\mathtt{wr}}\mapsto\bot,\mathsf{x}_{\mathtt{rd}}\mapsto\bot,\mathsf{y}\mapsto
0\\}$

  4. 4.

If $k>0$, there is a label $\mathsf{op}_{k}$ such that
$\langle\mathsf{s}_{k-1},\mathsf{w}_{k-1}\rangle\mathop{\xrightarrow{~{}\mathsf{op}_{k}~{}}}_{\mathcal{L}}\
\langle\mathsf{s}_{k},\mathsf{w}_{k}\rangle$.

The induction base case clearly holds true, since $\mathsf{c}_{0}$ is the
initial configuration of the game. So, suppose that the claim holds for some
arbitrary but fixed $0\leq k<n$. By the induction hypothesis, we can assume
that the game is in configuration $\mathsf{c}_{k}$. Consider the different
moves player B can make.

First, she may take a transition
$\mathsf{s}_{k}\mathop{\xrightarrow{~{}\mathtt{skip}~{}}}\mathsf{h}$. She
surely does not update any buffer messages during that move, since this would
enable player A to take
$\mathsf{q}_{1}\mathop{\xrightarrow{~{}\mathtt{rd}(\mathsf{x}_{\mathtt{wr}},\mathsf{m})~{}}}\mathsf{q}_{L}$
and win. So, we assume that player A moves along
$\mathsf{h}\mathop{\xrightarrow{~{}\mathtt{skip}~{}}}\mathsf{s}^{\prime}$. By
the construction of $\mathsf{Proc}^{1}$, the path
$\mathsf{s}_{k}\mathop{\xrightarrow{~{}\mathtt{skip}~{}}}\mathsf{h}\mathop{\xrightarrow{~{}\mathtt{skip}~{}}}\mathsf{s}^{\prime}$
implies the existence of a transition
$\mathsf{s}_{k}\mathop{\xrightarrow{~{}\mathtt{skip}~{}}}_{\mathcal{L}}\mathsf{s}^{\prime}$.
We define $\mathsf{s}_{k+1}:=\mathsf{s}^{\prime}$ and
$\mathsf{w}_{k+1}:=\mathsf{w}_{k}$ and conclude that the game is now in
configuration $\mathsf{c}_{k+1}$.

Another option for player A is to take the transition
$\mathsf{s}_{k}\mathop{\xrightarrow{~{}\mathtt{wr}(\mathsf{x}_{\mathtt{wr}},\mathsf{m})~{}}}\mathsf{h}$.
The argumentation continues exactly as in the previous paragraph, the only
difference is that
$\mathsf{s}_{k}\mathop{\xrightarrow{~{}!\mathsf{m}~{}}}_{\mathcal{L}}\mathsf{s}^{\prime}$
and $\mathsf{w}_{k+1}:=\mathsf{m}\bullet\mathsf{w}_{k}$.

Since all other transitions in $\mathsf{Proc}^{1}$ are disabled, the last
possibility for player B to move is in $\mathsf{Proc}^{2}$. She moves from
$\mathsf{q}_{1}$ to $\mathsf{q}_{2}$. We can assume that she updates exactly
one message from the buffer of $\mathsf{Proc}^{1}$, since otherwise player A
could win in her next turn. Instead, player A has to follow
$\mathsf{q}_{2}\mathop{\xrightarrow{~{}\mathtt{rd}(\mathsf{x}_{\mathtt{wr}},\mathsf{m})~{}}}\mathsf{q}_{\mathsf{m}}$.
In the following, we assume that player A performs no buffer updates unless
stated otherwise. Player B takes the transition
$\mathsf{q}_{\mathsf{m}}\mathop{\xrightarrow{~{}\mathtt{wr}(\mathsf{x}_{\mathtt{rd}},\mathsf{m})~{}}}\mathsf{q}_{4}$.
She might immediately update this message, but nothing else, following the
same argumentation as previously. Player A continues with
$\mathsf{q}_{4}\mathop{\xrightarrow{~{}\mathtt{wr}(\mathsf{x}_{\mathtt{wr}},\bot)~{}}}\mathsf{q}_{5}$,
we can assume that she also empties the buffer of $\mathsf{Proc}^{2}$. Moving
to $\mathsf{q}_{6}$ is losing for player B, thus we can safely say that she
performs
$\mathsf{s}_{k}\mathop{\xrightarrow{~{}\mathtt{rd}(\mathsf{x}_{\mathtt{rd}},\mathsf{m})~{}}}\mathsf{h}$
instead, which is the only enabled transition in $\mathsf{Proc}^{1}$. Player A
then has to proceed in $\mathsf{Proc}^{2}$ and the play continues there until
reaching $\mathsf{q}_{11}$.

We note the following observations, based on the fact that player A cannot
force a win. First, in $\mathsf{q}_{7}$, the variable $\mathsf{y}$ apparently
has value $0$, otherwise player A would win. This means that up to this point,
no message from the buffer of $\mathsf{Proc}^{1}$ has been updated (other than
the single $\langle\mathsf{x}_{\mathtt{wr}},\mathsf{m}\rangle$ from before).
Second, after moving to $\mathsf{q}_{8}$, player A performs such a buffer
update to prevent player B from immediately winning. Third, in
$\mathsf{q}_{11}$, the value of $\mathsf{x}_{\mathtt{wr}}$ in the memory must
be $\bot$, since otherwise player A could win with
$\mathsf{q}_{11}\mathop{\xrightarrow{~{}\mathtt{rd}(\mathsf{x}_{\mathtt{wr}},\mathsf{m})~{}}}\mathsf{q}_{L}$
for some channel message $\mathsf{m}$. This shows that since the transition
$\mathsf{q}_{6}\mathop{\xrightarrow{~{}\mathtt{mf}~{}}}\mathsf{q}_{7}$, no
further $\langle\mathsf{x}_{\mathtt{wr}},\mathsf{m}^{\prime}\rangle$-message
has been updated. In summary, we conclude that during the whole process,
exactly the two messages $\langle\mathsf{x}_{\mathtt{wr}},\mathsf{m}\rangle$
and $\langle\mathsf{y},1\rangle$ have been updated to the memory.

We continue with the execution from $\mathsf{q}_{11}$. Player A performs
$\mathsf{q}_{11}\mathop{\xrightarrow{~{}\mathtt{wr}(\mathsf{x}_{\mathtt{rd}},\bot)~{}}}\mathsf{q}_{12}$
and immediately updates this message to the memory. Player B either takes
either
$\mathsf{h}\mathop{\xrightarrow{~{}\mathtt{rd}(\mathsf{x}_{\mathtt{rd}},\bot)~{}}}\mathsf{s}^{\prime}$
in $\mathsf{Proc}^{1}$ or
$\mathsf{q}_{11}\mathop{\xrightarrow{~{}\mathtt{skip}~{}}}\mathsf{q}_{1}$ in
$\mathsf{Proc}^{2}$. We assume that player A takes the other one,
respectively.

We define $\mathsf{s}_{k+1}:=\mathsf{s}^{\prime}$ and $\mathsf{w}_{k+1}$ by
$\mathsf{w}_{k+1}\bullet\mathsf{m}:=\mathsf{w}_{k}$. The path
$\mathsf{s}_{k}\mathop{\xrightarrow{~{}\mathtt{rd}(\mathsf{x}_{\mathtt{rd}},\mathsf{m})~{}}}\mathsf{h}\mathop{\xrightarrow{~{}\mathtt{rd}(\mathsf{x}_{\mathtt{rd}},\bot)~{}}}\mathsf{s}_{k+1}$
implies that
$\langle\mathsf{s}_{k},\mathsf{w}_{k}\rangle\mathop{\xrightarrow{~{}?\mathsf{m}~{}}}_{\mathcal{L}}\langle\mathsf{s}_{k+1},\mathsf{w}_{k+1}\rangle$.
Furthermore, the observations above imply that the game is in configuration
$\mathsf{c}_{k+1}$ as defined in the beginning.

Now, we investigate how the run can continue after $\mathsf{c}_{n}$. Player B
cannot start to simulate a skip or send operation, since we can assume that
player A will move to $\mathsf{s}^{\prime}$, which contradicts the initial
assumption that $\mathsf{s}_{n}$ is the last channel state visited in this
run. The same holds true for a receive operation: Following the argumentation
from above, we have already seen that player A can either force a win, or lead
the game into completing the simulation of the receive operation. The only
possibility left is that $\mathsf{s}_{n}$ is a final channel state and player
B takes the transition
$\mathsf{s}_{n}\mathop{\xrightarrow{~{}\mathtt{wr}(\mathsf{x}_{\mathtt{wr}},\top)~{}}}\mathsf{h}_{F}$.

In summary, we constructed a path through $\mathcal{L}$ from
$\langle\mathsf{s}_{0},\varepsilon\rangle$ to
$\langle\mathsf{s}_{n},\mathsf{w}_{n}\rangle$, where
$\mathsf{s}_{n}\in\mathsf{S}_{F}$. This shows that the set of final states of
$\mathcal{L}$ is reachable.

###  D.3 Undecidability

######  Theorem 11.

The safety problem for the AB-TSO game is undecidable.

###### Proof.

This follows directly from Theorem 10 and the undecidability of the state
reachability problem for perfect channel systems [17]. ∎