# Four-wave mixing Floquet topological soliton

Sergey K. Ivanov  Moscow Institute of Physics and Technology, Institutsky lane
9, Dolgoprudny, Moscow region, 141700, Russia  Institute of Spectroscopy,
Russian Academy of Sciences, Troitsk, Moscow, 108840, Russia  Yaroslav V.
Kartashov  Institute of Spectroscopy, Russian Academy of Sciences, Troitsk,
Moscow, 108840, Russia  ICFO-Institut de Ciencies Fotoniques, The Barcelona
Institute of Science and Technology, 08860 Castelldefels (Barcelona), Spain
Vladimir V. Konotop  Departamento de Física, Faculdade de Ciências,
Universidade de Lisboa, Campo Grande, Ed. C8, Lisboa 1749-016, Portugal
Centro de Física Teórica e Computacional, Universidade de Lisboa, Campo
Grande, Ed. C8, Lisboa 1749-016, Portugal

###### Abstract

We consider a topological Floquet insulator realized as a honeycomb array of
helical waveguides imprinted in weakly birefringent medium. The systems
accounts for four-wave mixing occurring at a series of resonances arising due
to Floquet phase matching. Under these resonant conditions the system sustains
stable linearly polarized and metastable elliptically polarized two-component
edge solitons. Coupled nonlinear equations describing evolution of the
envelopes of such solitons are derived.

Transverse periodic modulation of a nonlinear medium represents one of the
most common tools for modification of the properties of a propagating beam. In
particular, one can create artificial dispersion supporting diverse types of
solitons and enhancing their stability, or create effective phase matching
conditions for resonant wave interactions. Rich possibilities for light
propagation control are offered by longitudinal periodic modulations of the
medium Rechtsman-13  allowing realization of Floquet topological insulators -
one of the most interesting and important applications of such artificially
created media linreview01 ; linreview02 .

A characteristic feature of topological insulators is the existence of states
localized near their edges and propagating along them HasanKane-10 . In
nonlinear optical systems localized solitons can bifurcate from the linear
topological edge states SmirnovaLeykamChongKivshar-20 . A variety of solitons
sustained by Floquet topological insulators was already obtained. These are
discrete Lumer-13 ; Ablowitz-14 ; AblowitzCole-17  and continuous
LeykamChong-16 ; Ivanov-20  scalar edge solitons, two-component vector
IvanovACS-20 ; IvanovDipol-21  and Bragg IvanovBragg-20  edge solitons.
Topological Floquet solitons were recently observed MukherjeeRechtsman-20
along with nonlinearity-induced edge states NonlinearTI .

All multicomponent solitons mentioned above were obtained for non-resonant
case, when components are coupled via cross-phase modulation only
ChenSegevCoskunChristodoulides-96 . At the same time, diverse optical systems
with Kerr nonlinearity sustain vector solitons in the presence of resonances,
involving the process of four-wave mixing (FWM) Menyuk-fiber ; Menyik-spatial
; Sterke-91 ; Winful ; ChenAtai-94 , see also Akhmediev1 ; Akhmediev2 . While
FWM in 2D periodic media is well studied Bartal-06 , its effect on solitons in
Floquet topological insulators has not been addressed, so far.

The goal of the present Letter is to report a new type of topological solitons
– FWM Floquet solitons. Such elliptically polarized vector states are composed
of two orthogonally polarized components and propagate along the edge of
photonic insulator, traversing hundreds of array periods with negligible
radiative losses. In sharp contrast to non-Floquet media, the resonant
conditions for the efficient FWM can be satisfied in our system for formally
infinite number of propagation constants determined by the novel Floquet
matching conditions. In contrast to previously studied scalar topological
solitons, the FWM Floquet solitons are essentially vector objects described by
two coupled equations for slowly varying amplitudes averaged over the Floquet
period. Their stability properties strongly depend on effective phase mismatch
controlled by waveguide twisting. Propagation of such solitons is
characterized by fast small-amplitude oscillations superimposed over the
average amplitudes.

We consider a two-component field ${\bm{E}}=(E_{x},E_{y})$ of the frequency
$\omega_{0}$ propagating along the $z$-axis of helical honeycomb array
imprinted in a weakly birefringent medium [Fig. 1(a)]. Let
$\psi_{x,y}=(L_{d}/L_{s}I_{0})^{1/2}e^{\pm i\beta z/4}E_{x,y}$, where
$L_{d}=k_{x}a^{2}\approx k_{y}a^{2}$ is the diffraction length for close
wavenumbers of two components $k_{x},k_{y}$, $\beta=2|k_{x}-k_{y}|L_{d}$ is
the normalized phase mismatch, $L_{s}=2c/(\omega_{0}n_{2}I_{0})$ is the self-
action length for nonlinear coefficient $n_{2}$, $a$ and $I_{0}$ are the
characteristic transverse scale and intensity, respectively. Then,
$\psi_{x,y}$ are governed by the system Yaroslav :

$\displaystyle\begin{split}i\frac{\partial\psi_{x}}{\partial
z}=&\left(-\frac{1}{2}\Delta_{\perp}-\frac{\beta}{4}-R\right)\psi_{x}-\\\
&\left(|\psi_{x}|^{2}+\frac{2}{3}|\psi_{y}|^{2}\right)\psi_{x}-\frac{1}{3}\psi_{x}^{*}\psi_{y}^{2},\end{split}$
(1) $\displaystyle\begin{split}i\frac{\partial\psi_{y}}{\partial
z}=&\left(-\frac{1}{2}\Delta_{\perp}+\frac{\beta}{4}-R\right)\psi_{y}-\\\
&\left(|\psi_{y}|^{2}+\frac{2}{3}|\psi_{x}|^{2}\right)\psi_{y}-\frac{1}{3}\psi_{y}^{*}\psi_{x}^{2}.\end{split}$
(2)

Here $\Delta_{\perp}=\partial_{x}^{2}+\partial_{y}^{2}$,
${{\bm{r}}}=\textbf{i}x+\textbf{j}y$ and $z$ are normalized to the
characteristic transverse scale $a$ and diffraction length $L_{d}$,
respectively. For simplicity, we assume identical refractive index landscapes
described by $R({\bm{r}},z)$ for both components. The nonlinear terms, in
order of their appearance in Eqs. (1), (2), describe self-phase-modulation
(SPM), cross-phase modulation (XPM), and four-wave mixing (FWM).

Honeycomb array [Fig. 1(a)] is periodic along the $y$ and $z$ axes and is
truncated along the $x$-axis:
$R({\bm{r}}+L\textbf{j},z)=R({\bm{r}},z+Z)=R({\bm{r}},z)$, where $L$ and $Z$
are the respective periods. It is described by the function
$R({\bm{r}},z)=p\sum_{mn}\exp{\left(-[{\bm{r}}-{\bm{r}}_{nm}-{\bm{s}}(z)]^{2}/\sigma^{2}\right)}$,
where ${\bm{s}}(z)=r_{0}(\sin(\omega z),\;\cos(\omega z))$ describes helicity
of the waveguides, ${\bm{r}}_{mn}$ are the coordinates of the knots of the
honeycomb lattice identified by the integers $m$ and $n$, $d$ is the distance
between neighbouring waveguides (respectively $L=3^{1/2}d$), $\sigma$ is the
waveguide width, $r_{0}$ is the helix radius, and $\omega=2\pi/Z$. We consider
truncation creating zigzag-zigzag interface [Fig. 1(b)]. Such arrays can be
fabricated using fs-laser writing Rechtsman-13 .

Figure 1: (a) Schematics of a 3D helical honeycomb array with clockwise
waveguide rotation direction. (b) Five periods of the truncated array with
zigzag-zigzag edges (top) and a linear Floquet edge state at $k=0.45K$ shown
for $z=0$ (bottom). Here and below $p=11$, $d=1.7$, $\sigma=0.4$, $r_{0}=0.5$,
and $Z=8$.

To describe physics of the phenomenon, we start with two linear eigenvalue
problems $\left(i\partial_{z}\pm\beta/4-H\right)\phi_{\nu k}^{\alpha}=b_{\nu
k}^{\alpha}\phi_{\nu k}^{\alpha}$, where
$H:=-(1/2)\Delta_{\perp}-R({\bm{r}},z)$ and $\alpha$ stands either for $x$
(”$+$”) or $y$ (”$-$”). The eigenvalues (pseudo-propagation constants) $b_{\nu
k}^{\alpha}\in[-\omega/2,+\omega/2)$ are marked by the index $\nu$ denoting a
band or an edge state, and by the Bloch momentum $k\in[0,\textrm{K})$ with
$\textrm{K}=2\pi/L$. At $\beta=0$, the linear spectra $b_{\nu k}^{x}$ and
$b_{\nu k}^{y}$ of two components coincide. We illustrate them in Fig. 2(a),
where we omitted indices for brevity. Waveguide helicity leads to opening of a
gap with two edge branches between the Dirac points (branches marked by blue
and red are localized at the left and right edges, respectively). An example
of the edge state from the red branch at $k=0.45K$ is shown in the lower panel
of Fig. 1(b).

Figure 2: (a) Pseudo-propagation constants vs Bloch wavenumber at $\beta=0$.
Green and magenta arrows indicate shifts of the band structures for $\psi_{x}$
and $\psi_{y}$ components, respectively, occurring due to $\beta>0$ (see the
text). (b) Superimposed band structures for $\psi_{x}$ (green dots) and
$\psi_{y}$ (magenta dots) components at $\beta=1.6$. (c) The first- (solid
lines) and second- (dashed lines) order derivatives for the edge state
branches in (a).

Our goal are Floquet solitons bifurcating from the edge states for $x$ and $y$
components in the presence of FWM. To ensure quasi-momentum conservation both
components must bifurcate form the linear states with the same Bloch momentum
$k_{0}$. Since, for a given edge there is only one branch of edge modes, we
conclude that both linear modes are represented by the same Floquet state with
the same indices $(\nu,k_{0})$. Below we denote such state by
$\phi_{0}=\phi_{\nu k_{0}}^{x}e^{-i(\beta/4)z}=\phi_{\nu
k_{0}}^{y}e^{i(\beta/4)z}$. At $\beta=0$ the eigenvalue corresponding to
$\phi_{0}$ is $b_{0}$. Now, to take into account weak nonlinearity and
describe the bifurcation of the FWM solitons we look for a solution of (1),
(2) in the form $\psi_{\alpha}=\mu
e^{i\left(b_{0}\pm\beta/4\right)z}[a_{\alpha}(Y,z)\phi_{0}+\mu\Phi_{\alpha}^{(1)}+...]$,
where $\mu\ll 1$ is a formal small parameter, $a_{\alpha}$ are the slowly
varying amplitudes and $Y=y-vz$ is the coordinate in the frame moving with
velocity $v=-b_{0}^{\prime}$ (here $b_{0}^{\prime}=\partial b_{0}/\partial
k$).

Now we recall that the efficiency of the FWM interactions is determined by the
phase matching conditions between two components, which would be trivial in
$z$-independent media, but acquire the following form in Floquet insulator:

$\displaystyle b_{x}=b_{y}+\frac{\delta}{2},\qquad(\text{mod}\;\omega),$ (3)

where $b_{x}=b_{0}+{\beta}/{4}$, $b_{y}=b_{0}-{\beta}/4$, and
$|\delta|\ll\omega$ is a small detuning. This condition stems from the fact
that the pseudo-propagation constant $b_{0}$ is determined in the Floquet
eigenvalue problem $\left(i\partial_{z}-H\right)\phi_{0}=b_{0}\phi_{0}$ modulo
$\omega$. Therefore (3) is referred below as Floquet phase matching. Thus, in
our Floquet system the exact resonance corresponds to the choice
$\beta=2n\omega$, $n=0,\,1,\,2,\,...$, while possible detuning from exact
phase matching is given by $\delta=\beta-2n\omega$, where $n$ is chosen to
minimize $|\beta-2n\omega|$. To illustrate the essence of the Floquet phase
matching, in Fig. 2(b) we show the shift of band structures of two components
from Fig. 2(a) arising due to non-zero $\beta$. Since $b_{x}$ and $b_{y}$
coincide at $\beta=0$, by adding and subtracting $\beta/4$ one cyclically
shifts two band structures upwards [green arrow in Fig. 2(a)] and downwards
[magenta arrow in 2(a)]. If mutual shift equals to $2n\omega$ the displaced
spectra exactly coincide with each other [although generally they will not
coincide with the original spectrum at $\beta=0$: cf. Fig. 2(a) and Fig.
2(b)). In the presence of small detuning $\delta$, shifted Floquet spectra
also appear slightly displaced, as shown in Fig. 2(b). Thus, Floquet phase
matching allows to compensate even considerable material phase mismatch
$\beta$ leading to efficient FWM interactions.

If condition (3) is satisfied, one can apply the multiscale expansion and
$z$-averaging defined by $\langle f\rangle_{Z}=(1/Z)\int_{0}^{Z}f(z)dz$, as
described in details in IvanovACS-20 ; IvanovDipol-21 , to derive the
equations for the slowly varying envelopes of two components:

$\displaystyle i\frac{\partial a_{x}}{\partial z}$
$\displaystyle=\frac{b_{0}^{\prime\prime}}{2}\frac{\partial^{2}a_{x}}{\partial
Y^{2}}-\chi\left(|a_{x}|^{2}a_{x}+\frac{2}{3}|a_{y}|^{2}a_{x}+\frac{1}{3}a_{x}^{*}a_{y}^{2}e^{-i\delta
z}\right),$ (4) $\displaystyle i\frac{\partial a_{y}}{\partial z}$
$\displaystyle=\frac{b_{0}^{\prime\prime}}{2}\frac{\partial^{2}a_{y}}{\partial
Y^{2}}-\chi\left(|a_{y}|^{2}a_{y}+\frac{2}{3}|a_{x}|^{2}a_{y}+\frac{1}{3}a_{y}^{*}a_{x}^{2}e^{+i\delta
z}\right).$ (5)

Here $b_{0}^{\prime\prime}=\partial^{2}b_{0}/\partial k^{2}$ and
$\chi=\langle\int|\phi_{0}|^{4}d{\bm{r}}\rangle_{Z}$ is the effective
nonlinearity coefficient. The derivatives $b_{0}^{\prime}=\partial
b_{0}/\partial k$ and $b_{0}^{\prime\prime}=\partial^{2}b_{0}/\partial k^{2}$
versus $k$ for selected states are shown in Fig. 2(c).

Figure 3: Profiles of the $w_{x}$ (solid lines) and $w_{y}$ (dashed lines)
soliton components at $\delta=0$ (a) and $\delta=0.005$ (b). In (a)
$b_{x}^{nl}=0.002$ (curve 1), $b_{x}^{nl}=0.005$ (curve 2), and
$b_{x}^{nl}=0.01$ (curve 3). In (b) $b_{x}^{nl}=0.002$, $b_{y}^{nl}=0.0045$
(curves 1) and $b_{x}^{nl}=0.01$, $b_{y}^{nl}=0.0125$ (curves 2). (c) Powers
of components $U_{x,y}$ (black and red curves) and perturbation growth rate
$\lambda$ (blue curve) vs $b_{x}^{nl}$ at $\delta=0.2$. Vertical dashed line
shows the border of existence for vector solitons. (d) Critical propagation
constant shift $b_{x}^{cr}$ vs detuning $\delta$. All solitons bifurcate from
edge state with $k_{0}=0.45K$, yielding $b_{0}^{\prime\prime}=-0.0963$,
$\chi=0.703$.

We are interested in bright vector solitons of Eqs. (4), (5) that exist at
$b_{0}^{\prime\prime}<0$. Such solitons can be found either linearly polarized
$a_{x,y}=w_{x,y}\exp{(ib_{x,y}^{nl}z)}$ or elliptically polarized
$a_{x}=w_{x}\exp{(ib_{x}^{nl}z)}$, $a_{y}=iw_{y}\exp{(ib_{y}^{nl}z)}$. To
ensure that the profiles $w_{x,y}$ are broad and cover many $y$-periods of the
structure, the nonlinearity-induced shifts of propagation constants
$b^{nl}_{x,y}$ must be much smaller than the pseudo-propagation constants and
the width of the gap in the Floquet spectrum. Since Eqs. (4), (5) allow
linearly polarized FWM solutions only for exact Floquet phase matching,
$\delta=0$, we consider only elliptically polarized states. Some properties of
the FWM Floquet solitons with elliptical polarization are illustrated in Fig.
3. Representative envelopes of such solitons for exact resonance ($\delta=0$)
are shown in Fig. 3(a). In this case both components coincide and feature
equal nonlinear propagation constant shifts $b_{x}^{nl}=b_{y}^{nl}$. Examples
of profiles at small detuning $\delta\neq 0$ are shown in Fig. 3(b). Now
soliton components have different shapes, since
$b_{y}^{nl}=b_{x}^{nl}+\delta/2$ is different from $b_{x}^{nl}$. Such FWM
vector solitons bifurcate from the family of scalar solitons with
$U_{x}=0,U_{y}\neq 0$ at critical propagation constant value
$b_{x}^{nl}=b_{x}^{cr}$ indicated by the dashed vertical line in Fig. 3(c),
the powers $U_{x,y}={\int|\psi_{x,y}|^{2}d{\bm{r}}}$ of its components
monotonically increase with $b_{x}^{nl}$. Critical propagation constant
$b_{x}^{cr}$ grows with increase of $|\delta|$, so that such vector solitons
exist within filled area in Fig. 3(d) with straight lower borders. We
performed linear stability analysis for perturbed solitons
$a_{x,y}=(w_{x,y}+u_{x,y}e^{\lambda z}+v_{x,y}e^{-\lambda
z})e^{ib_{x,y}^{nl}z}$ of Eqs. (4), (5), where
$|u_{\alpha}|,\,|v_{\alpha}|\ll|w_{\alpha}|$, and determined growth rate of
the most unstable perturbation. While for exact resonance $\delta=0$ all
states are stable ($\textrm{Re}\lambda=0$), for $\delta\neq 0$ we encountered
weak oscillatory instabilities with $\textrm{Re}\lambda\neq 0$, see Fig. 3(c)
for dependence of growth rate on $b^{nl}_{x}$ (blue curve). The characteristic
development length for such instabilities is $1/(\text{Re}\lambda)\gg Z$.
Similar results were obtained for other values of $\delta\neq 0$.

Figure 4: Propagation dynamics of the edge soliton corresponding to
$b_{x}^{nl}=b_{y}^{nl}=0.002$, $k=0.45K$, $b^{\prime\prime}=-0.0963$,
$\chi=0.703$ under conditions of exact Floquet phase matching ($\delta=0$) for
$\beta=0$ (left column) and $\beta=2\omega$ (right column). Last panel in the
left column shows output wavepacket in the linear regime. Two last panels in
the right column compare output $|\psi_{x}|$ and $|\psi_{y}|$ distributions.

In Fig. 4 we illustrate the evolution of the FWM edge solitons bifurcating
from the red branch in Floquet spectrum at $k_{0}=0.45K$ [see Fig. 2(a)] under
conditions of exact Floquet phase matching ($\delta=0$) for $\beta=0$ (left
column) and $\beta=2\omega\approx 1.57$ (right column). The initial conditions
in Eqs. (1), (2) for these soliton solutions are taken as
$a_{\alpha}(y,0)\phi_{0}({\bm{r}},0)$ with $a_{x}$ and $a_{y}$ found from Eqs.
(4), (5), respectively. We show dynamics for only one component; the dynamics
of the second one is identical. Both components are locked and move together
along the edge (see two last rows in the right column) without considerable
modifications (notice that we work with huge, but finite $y$-window, so due to
transverse displacement and periodic boundary conditions in $y$, after
sufficiently long propagation distance the soliton reappears from the other
side of the window). Weak reshaping, due to the fact that our theory provides
$z$-averaged approximation to the exact $z$-oscillating solution, takes place
only at the initial stage of propagation. There is almost no radiation into
the bulk of the array for selected $r_{0}$ and $Z$ values. To prove that these
states are indeed supported by the combined effect of SPM, XPM, and FWM in the
bottom panel of left column of Fig. 4 we show the output distribution
propagated through a linear medium. In this case we observe strong asymmetric
expansion of the wavepacket. Comparing two columns in Fig. 4 we observe that
FWM solitons at two different resonances are very similar [notice that their
envelopes obtained from Eqs. (4), (5) are identical, but they were propagated
using different resonant values of $\beta$ in full 2D Eqs. (1), (2)].

Figure 5: Propagation dynamics of the edge soliton corresponding to
$\delta=0.005$, $b_{x}^{nl}=0.002,b_{y}^{nl}=0.0045$,
$b_{0}^{\prime\prime}=-0.0963$, and $\chi=0.703$ at $k=0.45K$ (top and
middle). $|\psi_{x}|$ and $|\psi_{y}|$ distributions at different distances
are superimposed on the same plot. Peak amplitudes of components versus $z$
(bottom).

Propagation in the frames of Eqs. (1), (2) also confirms metastability of the
vector solitons at $\delta=0.005$, which survive over hundreds of helix
periods. The evolution of $\psi_{x}$ and $\psi_{y}$ components of such soliton
is illustrated in top and middle panels of Fig. 5, where distributions at
different distances $z$ are superimposed on the same plot. Metastability leads
to small-amplitude oscillations (bottom row) that do not cause destruction of
this state at the considered distances up to $z\sim 10^{4}$, even though
linear stability analysis predicts formal instability of the envelope and
small growth rate $\lambda=4.3\cdot 10^{-4}$.

In conclusion, we have shown that in a Floquet topological system it is
possible to realise a new type of resonant phase matching that enables the
existence of a new type of FWM edge solitons that are stable at exact
resonance and become metastable at small detuning from resonance.

The authors acknowledge funding from the RSF (grant 21-12-00096), and
Portuguese Foundation for Science and Technology (FCT) under Contract no.
UIDB/00618/2020.

Disclosures. The authors declare no conflicts of interest.

## References

  * (1) M. C. Rechtsman, J. M. Zeuner, Y. Plotnik, Y. Lumer, D. Podolsky, F. Dreisow, S. Nolte, M. Segev, and A. Szameit, “Photonic Floquet topological insulators,” Nature 496, 196 (2013).
  * (2) L. Lu, J. D. Joannopoulos and M. Soljačić, “Topological photonics,” Nature Photonics 8, 821 (2014).
  * (3) T. Ozawa, H. M. Price, A. Amo, N. Goldman, M. Hafezi, L. Lu, M. C. Rechtsman, D. Schuster, J. Simon, O. Zilberberg and I. Carusotto, “Topological photonics,” Rev. Mod. Phys. 91, 015006 (2019)
  * (4) M. Z. Hasan and C. L. Kane, “Topological insulators,” Rev. Mod. Phys. 82, 3045 (2010).
  * (5) D. Smirnova, D. Leykam, Y. D. Chong, and Y. Kivshar, “Nonlinear topological photonics,” Appl. Phys. Rev. 7, 021306 (2020).
  * (6) Y. Lumer, Y. Plotnik, M. C. Rechtsman, and M. Segev, “Self-Localized States in Photonic Topological Insulators,” Phys. Rev. Lett. 111, 243905 (2013).
  * (7) M. J. Ablowitz, C. W. Curtis, and Y.-P. Ma, “Linear and nonlinear traveling edge waves in optical honeycomb lattices,” Phys. Rev. A 90, 023813 (2014).
  * (8) M. J. Ablowitz and J. T. Cole, “Tight-binding methods for general longitudinally driven photonic lattices: Edge states and solitons,” Phys. Rev. A 96, 043868 (2017).
  * (9) D. Leykam and Y.-D. Chong, “Edge Solitons in Nonlinear-Photonic Topological Insulators,” Phys. Rev. Lett., 117, 143901 (2016).
  * (10) S. K. Ivanov, Y. V. Kartashov, A. Szameit, L. J. Maczewsky, and V. V. Konotop, “Edge Solitons in Lieb Topological Floquet Insulators,” Opt. Lett. 45, 1459 (2020).
  * (11) S. K. Ivanov, Y. V. Kartashov, A. Szameit, L. Torner, V. V. Konotop, “Vector topological edge solitons in Floquet insulators,” ACS Photonics 7, 735 (2020).
  * (12) S. K. Ivanov, Y. V. Kartashov, M. Heinrich, A. Szameit, L. Torner, and V. V. Konotop, “Topological dipole Floquet solitons,” Phys. Rev. A 103, 053507 (2021).
  * (13) S. K. Ivanov, Y. V. Kartashov, L. J. Maczewsky, A. Szameit, V. V. Konotop, “Bragg solitons in topological Floquet insulators,” Opt. Lett. 45, 2271 (2020).
  * (14) S. Mukherjee, M. C. Rechtsman, “Observation of Floquet solitons in a topological bandgap,” Science 368, 856 (2020).
  * (15) L. J. Maczewsky, M. Heinrich, M. Kremer, S. K. Ivanov, M. Ehrhardt, F. Martinez, Y. V. Kartashov, V. V. Konotop, L. Torner, D. Bauer, and A. Szameit, “Nonlinearity-induced photonic topological insulator,” Science 370, 701 (2020).
  * (16) Z. Chen, M. Segev, T. H. Coskun, and D. N. Christodoulides, “Observation of incoherently coupled photorefractive spatial soliton pairs,” Optics Letters 21, 18, 1436–1438 (1996).
  * (17) C. R. Menyuk, “Nonlinear Pulse Propagation in Birefringent Optical Fibers,” IEEE. J. Quant. Electr. 23, 174 (1987).
  * (18) C. R. Menyuk, IEEE. J. Quant. Electr. 25, 2674 (1989).
  * (19) C. M. de Sterke and J. E. Sipe, “Polarization instability in a waveguide geometry,” Opt. Lett. 16, 202 (1991).
  * (20) D. Liu and H. G. Winful, “Parametric solitons: nonlinear propagation of coherently coupled pulses generated through four-photon mixing processes,” Opt. Lett. 16, 67 (1991).
  * (21) Y. Chen and J. Atai, “Parametric spatial solitary waves,” Opt. Lett. 19, 1287 (1994).
  * (22) J. M. Soto-Crespo, N. Akhmediev, and A. Ankiewicz, “Stationary solitonlike pulses in birefringent optical fibers,” Phys. Rev. E 51, 3547 (1995).
  * (23) J. U. Kang, G. I. Stegeman, J. S. Aitchison, and N. Akhmediev, “Observation of Manakov spatial solitons in AlGaAs planar waveguides,” Phys. Rev. Lett. 76, 3699 (1996).
  * (24) G. Bartal, O. Manela, and M. Segev, “Spatial Four Wave Mixing in Nonlinear Periodic Structures,” Phys. Rev. Lett. 97, 073906 (2006).
  * (25) M. Heinrich, Y. V. Kartashov, A. Szameit, F. Dreisow, R. Keil, S. Nolte, A. Tünnermann, V. A. Vysloukh, and L. Torner, “Observation of two-dimensional coherent surface vector lattice solitons,” Opt. Lett. 34, 1624 (2009).


# Proving Unsolvability of Set Agreement Task with
Epistemic $\mu$-Calculus

Susumu Nishimura
<EMAIL_ADDRESS>
Dept. Math, Kyoto University, Japan The author is supported by JSPS KAKENHI
Grant Number 20K11678.

###### Abstract

This paper shows, in the framework of the _logical method_ [8, 21], the
unsolvability of $k$-set agreement task by devising a suitable formula of
epistemic logic. The unsolvability of $k$-set agreement task is a well-known
fact, which is a direct consequence of Sperner’s lemma, a classic result from
combinatorial topology. However, Sperner’s lemma does not provide a good
intuition for the unsolvability, hiding it behind the elegance of its
combinatorial statement. The logical method has a merit that it can account
for the reason of unsolvability by a concrete formula, but no epistemic
formula for the general unsolvability result for $k$-set agreement task has
been presented so far.

We employ a variant of _epistemic $\mu$-calculus_, which extends the standard
epistemic logic with distributed knowledge operators and propositional
fixpoints, as the formal language of logic. With these extensions, we can
provide an epistemic $\mu$-calculus formula that mentions higher-dimensional
connectivity, which is essential in the original proof of Sperner’s lemma, and
thereby show that $k$-set agreement tasks are not solvable even by multi-round
protocols. Furthermore, we also show that the same formula applies to
establish the unsolvability for $k$-concurrency, a submodel of the 2-round
protocol.

##  1 Introduction

A distributed _task_ is a computational problem to be solved by a distributed
system, which consists of $n+1$ mutually communicating processes. A task
specifies, for a given set of initial inputs to the processes, what final
output values are expected to be produced by the processes. For instance, _$k$
-set agreement_, which is a fundamental distributed computing problem, is
specified as a task that produces a set of final outputs satisfying the
following properties.

Agreement

At most $k$ different output values are decided by the $n+1$ processes;

Validity

The output decided by each process must be one of the $n+1$ input values given
to the processes.

We say a task is solvable, if there exists a distributed algorithm, called a
_protocol_ , that conforms to the task specification. Throughout the paper, we
argue distributed task solvability by wait-free protocols, assuming
asynchronous distributed systems with crash-failure.

Research development in the last decades has found the so called _topological
method_ [11] as a means for discussing properties of distributed systems,
especially unsolvability of distributed tasks, on the firm theoretical ground
of combinatorial topology. In the topological method, a state of a distributed
system of $n+1$ processes is modeled by an $n$-dimensional _simplex_ , whose
$n+1$ vertexes represent the local states of the $n+1$ processes. A task or a
protocol is defined as a function, called a _carrier map_ , that relates each
input simplex with a _(simplicial) complex_ , i.e., a collection of output
simplexes, which is intended to model the combination of nondeterministic
outputs by the $n+1$ processes. The topological method argues the
unsolvability of a task by showing that existence of a carrier map breaches
certain topological invariant, where tools from combinatorial topology come
into play.

The topological method has been successful because of its cleanness, but it
sometimes hides the reason of unsolvability behind the elegance of topological
tools. For instance, one can cleanly prove the unsolvability of the $k$-set
agreement task [13, 11], admitting the following classic result from
combinatorial topology.

######  Sperner’s Lemma  ([20, 5]).

Suppose we are given a simplex $X$ whose vertexes are distinctly colored by a
color set $S$. We say a coloring on vertexes of a subdivision of $X$ a
_Sperner coloring_ , if each vertex $v$ in the subdivision has the same color
as a vertex of $Y$, where $Y$ is the minimal face of $X$ that contains $v$.
Then, any subdivision of the simplex $X$ with Sperner coloring contains an odd
number of simplexes that are fully-colored by $S$.

The unsolvability of $k$-set agreement task is a direct consequence of
Sperner’s lemma, but the statement of the lemma does not provide a good
topological intuition for the reason of unsolvability.

Goubault, Ledent, and Rajsbaum [8] proposed _logical method_ as an alternative
to the topological method. They observed that a topological model of
simplicial complex has an equivalent counterpart of Kripke model, where the
adjacency of simplexes in a complex is interpreted as the relation over Kripke
states that is suitable for epistemic reasoning. This allows us to establish
the unsolvability of a task just by finding a formula of epistemic logic [22]
that is valid in the Kripke model of the task but not valid in the model of
the protocol. Their method has a strong merit that such a formula can
explicitly account for the unsolvability.

In its earliest development, the logical method has come with few concrete
formulas, however. Goubault et al. [8] provided such an epistemic formula for
consensus task (i.e., 1-set agreement) and $N$-approximate agreement task but
they left general $k$-set agreement as an open problem. Soon later, Nishida
[17] devised a concrete epistemic logic formula to show the unsolvability of
$k$-set agreement and this formula is further refined in [24] to show the
unsolvability under superset-closed adversary, which generalizes wait-freedom.
However, both studies solely concern single-round protocols, where each
process in the system is allowed to communicate with the others by accessing
the communication device only once. In contrast, the topological method works
for multi-round protocols, where processes are allowed to communicate
arbitrarily many times, as so usual in most of the distributed environments.

The aim of this paper is to provide a concrete formula that proves the
unsolvability of $k$-set agreement task by multi-round protocols in the
framework of the logical method and thereby to express the reason for the
unsolvability in the formal language of epistemic logic. The statement of
Sperner’s lemma is, however, not directly expressible by epistemic logic,
because there is no effective means to enumerate all relevant epistemic states
in a Kripke model. So we instead elaborate on the combinatorial structure that
is exploited in the proof of Sperner’s lemma [5]. For this, we need to extend
the formal language of epistemic logic with the following three aspects:

Epistemic $\mu$-calculus for connectivity.

We extend the language of the epistemic logic with propositional greatest
fixpoint $\nu Z.\varphi$, which gives rise to the _epistemic $\mu$-calculus_
[6, 19], an epistemic variant of modal $\mu$-calculi [15, 4]. While epistemic
modalities, such as the knowledge modality $\mathop{\mathrm{K}_{a}}$, in the
standard epistemic logic can only mentions adjacent epistemic states of finite
proximity in a Kripke model, the epistemic $\mu$-calculus can express indirect
adjacency of unbounded diameter, e.g., transitive closure of adjacency
relations, by means of greatest fixpoints.

Distributed knowledge for higher-dimensional connectivity.

We further extend the epistemic $\mu$-calculus by introducing distributed
knowledge modality $\mathop{\mathrm{D}_{A}}$, where $A$ is a subset of the
$n+1$ processes. Topologically, while the knowledge modality
$\mathop{\mathrm{K}_{a}}$ concerns simplexes that are connected via a single
common vertex, the distributed knowledge modality $\mathop{\mathrm{D}_{A}}$
[6, 10] concerns simplexes connected via a common simplex of an arbitrary
dimension, e.g., a vertex (dimension 0 for ${\lvert}A{\rvert}=1$), an edge
(dimension 1 for ${\lvert}A{\rvert}=2$), a surface (dimension 2 for
${\lvert}A{\rvert}=3$), etc.

Factual change of atomic propositions mentioning output decision.

We carry out our development in a logical model that extends the original one
with factual change of atomic propositions [21]. The extended model provides
an extra set of atomic formulas that can mention the final output decision
values made by processes.

Sperner’s lemma has been proven by examining the combinatorial structure that
is specific to a certain graph induced from Sperner coloring, where the graph
nodes are the simplexes and the edges are connecting those adjacent simplexes,
which share a common face. We paraphrase this argument on the graph structure
into that on higher-dimensional connectivity of simplicial complex and
construct a relevant logic formula, combining the greatest fixpoint and
distributed knowledge modality, where the formula also needs to mention output
decision values in order to describe the constrains on coloring. Specifically,
assuming the solvability of $k$-set agreement, we show that a certain
epistemic $\mu$-calculus formula entails the existence of a cycle-free, ever-
lasting connectivity path, which leads to a contradiction.

###  1.1 Related work

To the best of author’s knowledge, there has been no proposal of a concrete
epistemic logic formula that gives an account for the reason that multi-round
protocols cannot solve $k$-set agreement task. Recent developments on the
logical method have shown that the standard epistemic logic, which employs
solely knowledge modality, is rather weak for establishing unsolvability. In
[21], a bisimulation technique is applied to show that no formula of the
standard epistemic logic can establish the unsolvability of a certain task,
which can be proven unsolvable by the topological method. Very recently,
Hoshino [14] observed that, applying a simulation technique, the unsolvability
of set agreement tasks by multi-round protocols cannot be established, even if
the language of the logic is extended with distributed knowledge modality.
This indicates that the formula proposed in [17, 24], which makes use of
distributed knowledge modality, is a peculiar instance that works solely for
single-round protocols.

In [21], Ditmarsch et al. proposed to extend the logical model with factual
change of atomic propositions [8] and provided a generic formula of the
extended logic that works for virtually every task whose unsolvability can be
established by a topological argument. However, this generic formula contains
no epistemic modality within and therefore provides no hints for the reason of
unsolvability. In the present study, we also assume the logical model extended
with factual change but present a formula that contains explicit epistemic
contents expressing higher-dimensional connectivity.

From the perspective of topological method, it has been observed that higher-
dimensional connectivity, a.k.a., $k$-connectivity [11, 12], is essential for
the unsolvability of $(k+1)$-set agreement task. The present work expresses a
similar (but topologically less general) notion of higher-dimensional
connectivity in the language of epistemic $\mu$-calculus.

###  1.2 Organization

The rest of this paper is organized as follows. Section 2 reviews the
topological model of distributed computing and introduces the epistemic
$\mu$-calculus for reasoning about distributed systems. Section 3 gives the
formal definition of product update models, on which the unsolvability of
$k$-set agreement task is argued. In Section 4, we prove the unsolvability
with a concrete formula that encodes the essence of Sperner’s lemma in the
language of epistemic $\mu$-calculus. We further discuss that the same method
applies to a submodel of $k$-concurrency in Section 5.

##  2 Logical Approach to Distributed Computing

In what follows, $[\ell,m]$ denotes a range of nonnegative integers, namely,
the set $\\{\ell,\ell+1,\ldots,m\\}$. We consider a distributed system of
$n+1$ processes, where each individual process is distinguished by a unique
process id, taken from the set $\Pi=[0,n]$. We say ‘process $a$’ to refer to
the process identified by the unique id $a\in\Pi$. We also write
$\mathit{Value}$ to denote the set of possible initial input values given to
each process. In the sequel, we assume $\mathit{Value}=\Pi$, renaming the
input values as necessary.

###  2.1 Simplicial topology for distributed computing

In the topological theory of distributed computing [11], a particular state of
an individual process is represented by a pair
$(a,v)\in\Pi\times\mathit{Value}$ to mean that a process $a$ has a private
value $v$. The pair $(a,v)$ is regarded as a vertex of color $a$ and we define
the _coloring function_ $\chi$ on colored vertexes by $\chi((a,v))=a$. A
_simplex_ is a collection of vertexes of pairwisely distinct colors and a
simplex consisting of $d+1$ vertexes is called a $d$-dimensional simplex. A
simplex $Y$ is called a _face_ of a simplex $X$, if $Y\subseteq X$. For a
simplex $X$ and a color $a\in\chi(X)$, we define $\mathit{view}_{a}(X)=v$ iff
$(a,v)\in X$.

A _simplicial complex_ (or _complex_ for short) $\mathcal{C}$ is a finite
collection of simplexes closed under set inclusion: $X\in\mathcal{C}$ and
$Y\subseteq X$ implies $Y\in\mathcal{C}$. A maximal simplex in $\mathcal{C}$
is called a _facet_. Particularly, a distributed system of $n+1$ processes is
modeled by a complex whose every facet is a simplex
$\\{(0,v_{0}),(1,v_{1}),\ldots,(n,v_{n})\\}$ of dimension $n$, where the $n+1$
vertexes are distintively colored through $0$ to $n$. We write
$\mathsf{F}(\mathcal{C})$ (resp., $V(\mathcal{C})$) to denote the set of
facets (resp., vertexes) contained in $\mathcal{C}$.

Suppose we are given complexes $\mathcal{C}$ and $\mathcal{D}$ colored by
$\Pi$. A _simplicial_ map $\delta:V(\mathcal{C})\to V(\mathcal{D})$ is a
color-preserving function on vertexes such that $\chi(\delta(v))=\chi(v)$ for
every $v\in V(\mathcal{C})$ and also $\delta(X)\in\mathcal{D}$ for every
$X\in\mathcal{C}$. We also define the cartesian product
$\mathcal{C}\times\mathcal{D}$ as follows. For each pair of facets
$X\in\mathsf{F}(\mathcal{C})$ and $Y\in\mathsf{F}(\mathcal{D})$, we define
$X\times Y$ as a simplex $X\times Y=\\{(a,(u,v))\mid(a,u)\in X,(a,v)\in
Y,a\in\Pi\\}$ so that each vertex in $X\times Y$ is given a pair of private
values taken from the vertexes of matching color in $X$ and $Y$. The cartesian
product $\mathcal{C}\times\mathcal{D}$ is a complex determined by the set of
facets $\mathsf{F}(\mathcal{C}\times\mathcal{D})=\\{X\times Y\mid
X\in\mathsf{F}(\mathcal{C}),Y\in\mathsf{F}(\mathcal{D})\\}$.

###  2.2 Epistemic logic for distributed computing

####  2.2.1 The epistemic $\mu$-calculus

The syntax of the epistemic $\mu$-calculus formulas considered in this paper
is given by:

$\varphi::=p\mid\neg p\mid
Z\mid\varphi\vee\varphi\mid\varphi\wedge\varphi\mid\mathop{\mathrm{D}_{A}}\varphi\mid\nu
Z.\varphi,$

where $p$ ranges over the set $\mathrm{AP}$ of atomic propositions, $Z$ ranges
over the set $\mathrm{PV}$ of propositional variables, and $A$ ranges over
$2^{\Pi}$.

Notice that the formulas are restricted to _positive_ ones: Only atomic
formulas are allowed to be negated by $\neg$. In what follows, we say
$\varphi$ is a propositional formula, if it does not contain any propositional
variables, epistemic modalities, or greatest fixpoints. As usual convention,
we write $\varphi\Rightarrow\psi$ for $\neg\varphi\vee\psi$, where $\varphi$
is a propositional formula and $\psi$ is a positive formula.

$\displaystyle\lVert{}p\rVert^{M}_{\rho}={}$ $\displaystyle\\{X\in S\mid p\in
L(X)\\}\qquad\quad\lVert{}Z\rVert^{M}_{\rho}={}\rho(Z)\qquad\quad\lVert{}\neg
p\rVert^{M}_{\rho}={}S\setminus\lVert{}p\rVert^{M}_{\rho}$
$\displaystyle\lVert{}\varphi_{1}\vee\varphi_{2}\rVert^{M}_{\rho}={}$
$\displaystyle\lVert{}\varphi_{1}\rVert^{M}_{\rho}\cup\lVert{}\varphi_{2}\rVert^{M}_{\rho}\qquad\qquad\lVert{}\varphi_{1}\wedge\varphi_{2}\rVert^{M}_{\rho}={}\lVert{}\varphi_{1}\rVert^{M}_{\rho}\cap\lVert{}\varphi_{2}\rVert^{M}_{\rho}$
$\displaystyle\lVert{}\mathop{\mathrm{D}_{A}}\varphi\rVert^{M}_{\rho}={}$
$\displaystyle\\{X\in S\mid Y\in\lVert{}\varphi\rVert^{M}_{\rho}\text{ for
every $Y$ such that $Y\sim_{A}X$}\\}$ $\displaystyle\lVert{}\nu
Z.\varphi\rVert^{M}_{\rho}={}$ $\displaystyle\bigcup\\{S^{\prime}\in 2^{S}\mid
S^{\prime}\subseteq\lVert{}\varphi\rVert^{M}_{\rho[S^{\prime}/Z]}\\}$ Figure
1: Kripke semantics of the epistemic $\mu$-calculus

A _Kripke frame_ is a pair $\langle{S,\sim}\rangle$, where $S$ is the set of
(epistemic) _states_ and $\sim$ is a family $\\{\sim_{a}\subseteq S\times
S\mid a\in\Pi\\}$ of _indistinguishability relations_ , with each $\sim_{a}$
being an equivalence relation over $S$. The Kripke model
$M=\langle{S,\sim,L}\rangle$ augments the Kripke frame with a function $L:S\to
2^{\mathrm{AP}}$, which assigns, for each $X\in S$, a set $L(X)$ of atomic
propositions that are true at the state $X$. For a subset $A$ of $\Pi$, we
write $\sim_{A}$ for a derived equivalence relation defined by $X\sim_{A}Y$
iff $X\sim_{a}Y$ for all $a\in A$.

The formal semantics of a formula $\varphi$ is given by the set
$\lVert{}\varphi\rVert^{M}_{\rho}$ of states at which $\varphi$ is satisfied,
where $\rho:\mathrm{PV}\to 2^{S}$ gives an _interpretation_ of propositional
variables that occur free in $\varphi$. Figure 1 gives the definition of the
semantics by induction on the structure of formula $\varphi$. In addition to
propositional formulas, the epistemic $\mu$-calculus provides an epistemic
modality $\mathop{\mathrm{D}_{A}}\varphi$, which is intended to express the
distributed knowledge asserting “the group $A$ of processes know $\varphi$.”
It further provides greatest fixpoint $\nu Z.\varphi$, which denotes the
greatest solution satisfying the equation $Z=\varphi$ on the propositional
variable $Z$ [6, 19].111The least fixpoint $\mu Z.\varphi$, which is logically
equivalent to $\neg\nu Z.\neg\varphi$, is missing from the present logic,
because it is not a positive formula.

In what follows, we write $M,X\models_{\rho}\varphi$ iff
$X\in\lVert{}\varphi\rVert^{M}_{\rho}$, to mean that, $\varphi$ is _satisfied_
at a particular state $X$ of Kripke model $M$, under an interpretation $\rho$.
In particular, we write $M,X\models\varphi$, when $\varphi$ is a _closed_
formula, i.e., $\varphi$ contains no free occurrences of propositional
variables. We also write $M\models\varphi$ to mean a closed formula $\varphi$
is _valid_ , that is, $M,X\models\varphi$ holds at every state $X\in S$ of the
Kripke model $M$.

####  2.2.2 Simplicial model: a Kripke model induced from simplicial complex

The topological structure of a complex can be turned into a Kripke model,
called a _simplicial model_ [8].

######  Definition 2.1.

A complex $\mathcal{C}$ induces a Kripke model
$M=\langle{\mathsf{F}(\mathcal{C}),\sim,L}\rangle$, called a _simplicial
model_ , where

  * •

the set of (epistemic) states is the set of facets $\mathsf{F}(\mathcal{C})$
of $\mathcal{C}$,

  * •

$\sim$ is a family of relations $\\{\sim_{a}\mid a\in\Pi\\}$ over
$\mathsf{F}(\mathcal{C})$, where each $\sim_{a}$, called an
_indistinguishability relation_ , is an equivalence relation defined by
$X\sim_{a}Y\text{ iff }a\in\chi(X\cap Y)$, and

  * •

$L:\mathsf{F}(\mathcal{C})\to 2^{\mathrm{AP}}$, where
$\mathrm{AP}=\\{\mathsf{input}_{a}^{v}\mid a\in\Pi,v\in\mathit{Value}\\}$, is
a function defined by $L(X)=\\{\mathsf{input}_{a}^{v}\mid(a,v)\in X\\}$.

By abuse of notation, we write $\mathcal{C}$ to refer to both the complex
$\mathcal{C}$ itself and the simplicial model
$M=\langle{\mathcal{C},\sim,L}\rangle$ induced from it. Simplicial models
indeed have the identical structure with local proper Kripke models [8], up to
categorical equivalence under a suitable categorical setting.

(a) A simplical complex $\mathcal{C}$

(b) The corresonding Kripke model
$\langle{\mathsf{F}(\mathcal{C}),\sim,L}\rangle$

Figure 2: A topological model and its corresponding Kripe model for a 3
process system

Fig. 2 illustrates how a complex is interpreted as a Kripke model. Fig. 2
gives a 2-dimensional complex consisting of three different facets, which
models a 3 process system of process ids $\Pi=\\{0,1,2\\}$. Each vertex
receives its own private input as indicated in the figure and each facet has 3
vertexes, as designated by vertexes of different colors ${\circ}$,
${\color[rgb]{0,0,204}\bullet}$, and ${\color[rgb]{255,204,204}\bullet}$,
corresponding to processes $0$, $1$, and $2$, respectively. (Throughout the
rest of the paper, we will follow this coloring convention.) Fig. 2 shows the
corresponding simplicial Kripke model. The Kripke frame is depicted by an
undirected graph, where each graph node stands for a state, corresponding to a
facet in $\mathcal{C}$, and each graph edge labeled by $a\in\Pi$ stands for a
pair of nodes related by $\sim_{a}$. (As such, a simplicial model can be
pictorized by an undirected graph with self-cycles, because epistemic
knowledge is modeled by an S5 Kripke model, in which $\sim_{a}$ is an
equivalence relation for each $a\in\Pi$.) The function $L$ determines the
input value given to each vertex in each facet by the set of atomic formulas
of the form $\mathsf{input}_{a}^{v}$, as in the figure.

Though the epistemic logic primarily concerns epistemic information in Kripke
models, geometric interpretation on the original complexes, from which the
simplicial models are induced, is insightful for the later development in this
paper. A pair of facets are related by $\sim_{a}$ in an induced simplicial
model $\langle{\mathsf{F}(\mathcal{C}),\sim,L}\rangle$, as it immediately
follows from the definition, if they share a common vertex of color $a$ in the
complex $\mathcal{C}$. Similarly, the derived relation $\sim_{A}$ relates a
pair of facets if they share a common face $U$ such that $\chi(U)=A$. For
example, in the complex of Fig. 2, $X\sim_{\\{1,2\\}}Y$ holds, because they
share a 1-dimensional simplex (i.e., an edge that connects
${\color[rgb]{0,0,204}\bullet}$ and ${\color[rgb]{255,204,204}\bullet}$). In
contrast, $X$ and $W$ are not related by $\sim_{\\{1,2\\}}$ but by
$\sim_{\\{1\\}}$ via the common 0-dimensional simplex (i.e., vertex
${\color[rgb]{0,0,204}\bullet}$).222The distributed knowledge operator
$\mathop{\mathrm{D}_{\\{a\\}}}\varphi$ for a singleton set of processes is
known as the knowledge operator $\mathop{\mathrm{K}_{a}}\varphi$. The
knowledge operator is more popular in the literature of epistemic logic but is
omitted in the present logic, as it is a special form of the distributed
knowledge. Therefore
$\mathcal{C},X\models\mathop{\mathrm{D}_{\\{1,2\\}}}\mathsf{input}_{2}^{2}$ is
satisfied because $\sim_{\\{1,2\\}}$ relates $X$ with itself and $Y$, while
$\mathcal{C},X\not\models\mathop{\mathrm{D}_{\\{1\\}}}\mathsf{input}_{2}^{2}$
because $X\sim_{\\{1\\}}W$ but
$\mathcal{C},W\not\models\mathsf{input}_{2}^{2}$.

The greatest fixpoint provides extra power in expressing epistemic property
such as the common knowledge and the common distributed knowledge [6, 2]. The
common knowledge, written $\mathop{\mathrm{C}_{A}}\psi$ for a subset $A$ of
$\Pi$, can be defined as the greatest fixpoint $\nu
Z.(\psi\wedge\bigwedge_{a\in A}\mathop{\mathrm{D}_{\\{a\\}}}Z)$, which can be
understood as an infinite conjuction in repeated unfolding
$\psi\wedge\bigwedge_{a\in
A}\mathop{\mathrm{D}_{\\{a\\}}}\Bigl{(}\psi\wedge\bigwedge_{a\in
A}\mathop{\mathrm{D}_{\\{a\\}}}\bigl{(}\psi\wedge\bigwedge_{a\in
A}\mathop{\mathrm{D}_{\\{a\\}}}(\ldots)\bigr{)}\Bigr{)}$. This defines the
common knowledge $\mathop{\mathrm{C}_{A}}\psi$ as a property that $\psi$ is
satisfied at every state in the reach of the trasitive closure of the union
relation $\bigcup_{a\in A}\sim_{a}$. For example, in the complex $\mathcal{C}$
of Fig. 2,
$\mathcal{C},X\not\models\mathop{\mathrm{C}_{\\{0,2\\}}}\mathsf{input}_{2}^{2}$
but $\mathcal{C},X\models\mathop{\mathrm{C}_{\\{2\\}}}\mathsf{input}_{2}^{2}$,
because $X\sim_{2}Y\sim_{0}W$ and hence $W$ is in the reach of the former but
not the latter.

In the subsequent sections, task solvability will be defined with the notion
of morphisms. Let $\langle{\mathsf{F}(\mathcal{C}),\sim,L}\rangle$ and
$\langle{\mathsf{F}(\mathcal{D}),\sim^{\prime},L^{\prime}}\rangle$ be
simplicial models induced from complexes $\mathcal{C}$ and $\mathcal{D}$,
respectively. We say a function $\delta:V(\mathcal{C})\to V(\mathcal{D})$ is a
_morphism_ , if $\delta$ is a color-preserving simplicial map and furthermore
$L(X)=L^{\prime}(\delta(X))$ holds for every $X\in\mathsf{F}(\mathcal{C})$.

The knowledge gain theorem, which is essential for showing task unsolvability
in the logical method, is conservatively extended to allow the additional
logical connectives, i.e., greatest fixpoints and distributed knowledge
modalities, in the epistemic $\mu$-calculus.

######  Theorem 2.1 (knowledge gain).

Suppose $\mathcal{C}=\langle{\mathsf{F}(\mathcal{C}),\sim,L}\rangle$ and
$\mathcal{D}=\langle{\mathsf{F}(\mathcal{D}),\sim^{\prime},L^{\prime}}\rangle$
are simplicial models and $\delta$ is a morphism from $\mathcal{C}$ to
$\mathcal{D}$. Then, for any state $X\in\mathsf{F}(\mathcal{C})$ and closed
positive formula $\varphi$, $\mathcal{D},\delta(X)\models\varphi$ implies
$\mathcal{C},X\models\varphi$.

##  3 Product Update Models for $k$-Set Agreement

In the logical method, distributed computation is modeled by _product updates_
, which have been used for defining update on the knowledge model in dynamic
epistemic logic (DEL) [1, 22]. This section presents concrete instances of
product updates that are relevant for discussing $k$-set agreement.

###  3.1 Product updates and task solvability

Suppose $\mathcal{C}$ and $\mathcal{D}$ are complexes. A product update model
is derived from a complex $\mathcal{C}[\mathcal{D}]$, which is a subcomplex of
the the cartesian product $\mathcal{C}\times\mathcal{D}$ (i.e.,
$\mathsf{F}(\mathcal{C}[\mathcal{D}])\subseteq\mathsf{F}(\mathcal{C}\times\mathcal{D})$).
The subcomplex $\mathcal{C}[\mathcal{D}]$ can be regarded as a specification
of distributed computation: $X\times Y\in\mathsf{F}(\mathcal{C}[\mathcal{D}])$
implies that $Y\in\mathsf{F}(\mathcal{D})$ is one of possible outputs for an
input $X\in\mathsf{F}(\mathcal{C})$. In other words,
$\mathcal{C}[\mathcal{D}]$ is a binary relation over
$\mathsf{F}(\mathcal{C})\times\mathsf{F}(\mathcal{D})$, which encodes a one-
to-many mapping from input facets to output facets. (Formally, such a
subcomplex $\mathcal{C}[\mathcal{D}]$ is determined by an epistemic formula,
called a _precondition_ , defined for each $Y\in\mathsf{F}(\mathcal{D})$. See
[8, 21] for the formal definition.)

Let $\mathcal{C}[\mathcal{D}]$ be a subcomplex of
$\mathcal{C}\times\mathcal{D}$ and
$\langle{\mathsf{F}(\mathcal{C}),\sim^{\mathcal{C}},L}\rangle$ be the
simplicial model induced from $\mathcal{C}$. A _product update model_ is a
simplicial model
$\langle{\mathsf{F}(\mathcal{C}[\mathcal{D}]),\sim^{\mathcal{C}[\mathcal{D}]},L^{\prime}}\rangle$,
where
$\langle{\mathsf{F}(\mathcal{C}[\mathcal{D}]),\sim^{\mathcal{C}[\mathcal{D}]}}\rangle$
is the Kripke frame induced from $\mathcal{C}[\mathcal{D}]$ and $L^{\prime}$
is defined by $L^{\prime}(X\times Y)=L(X)$ for every $X\times
Y\in\mathsf{F}(\mathcal{C}[\mathcal{D}])$.

In what follows, we write $\mathcal{I}$ to denote the input complex, i.e., a
complex whose set of facets is
$\mathsf{F}(\mathcal{I})=\bigl{\\{}\\{(0,v_{0}),\ldots,(n,v_{n})\\}\mid
v_{0},\ldots,v_{n}\in\Pi\bigr{\\}}$. To argue if a task is solvable by a
protocol in the logical method, we model the task and the protocol by product
update models $\mathcal{I}[\mathcal{T}]$ and by $\mathcal{I}[\mathcal{P}]$,
respectively, where $\mathcal{T}$ is the output complex for the task and
$\mathcal{P}$ is that for the protocol. The task solvability is defined as
below, via the notion of morphism, as follows.

######  Definition 3.1 (task solvability[8]).

A task $\mathcal{I}[\mathcal{T}]$ is solvable by a protocol
$\mathcal{I}[\mathcal{P}]$ iff there exists a morphism
$\delta:\mathcal{I}[\mathcal{P}]\to\mathcal{I}[\mathcal{T}]$ such that
$\pi_{\mathcal{I}}\circ\delta=\pi_{\mathcal{I}}$, where $\pi_{\mathcal{I}}$ is
the first projection, i.e., $\pi_{\mathcal{I}}((X\times Y))=X$.

The product update model presented above, however, does not suffice for
showing the unsolvability of $k$-set agreement, as we have mentioned in
Section 1. We need to extend it with factual change [21] so that the output
decision values can be mentioned by atomic propositions.

Let $\mathcal{I}[\mathcal{T}]$ denote the product update model
$\langle{\mathsf{F}(\mathcal{I}[\mathcal{T}]),\sim^{\mathcal{I}[\mathcal{T}]},L}\rangle$
for the task and $\mathcal{I}[\mathcal{P}]$ denote the product update model
$\langle{\mathsf{F}(\mathcal{I}[\mathcal{P}]),\sim^{\mathcal{I}[\mathcal{P}]},L^{\prime}}\rangle$
for the protocol. Let us assume an augmented set of atomic propositions
$\widehat{\mathrm{AP}}=\mathrm{AP}\cup\\{\mathsf{decide}_{a}^{v}\mid
a\in\Pi,v\in\mathit{Value}\\}$, where $\mathsf{decide}_{a}^{v}$ is an atomic
proposition asserting that process $a$ decides $v$ as its output value. Then
the product update model with factual change for the task, written
$\widehat{\mathcal{I}[\mathcal{T}]}$, is a modified product update model
$\langle{\mathsf{F}(\mathcal{I}[\mathcal{T}]),\sim^{\mathcal{I}[\mathcal{T}]},\widehat{L}}\rangle$,
where $\widehat{L}$ augments the assignment of true atomic propositions by
$\widehat{L}(X\times Y)=\\{\mathsf{input}_{a}^{v}\mid(a,v)\in
X\\}\cup\\{\mathsf{decide}_{a}^{d}\mid(a,d)\in Y\\}$. Moreover, for each given
morphism $\delta:\mathcal{I}[\mathcal{P}]\to\mathcal{I}[\mathcal{T}]$, the
product update model with factual change for the protocol, written
${\mathcal{I}[\mathcal{P}]}_{\delta}$, is a modified product update model
$\langle{\mathsf{F}(\mathcal{I}[\mathcal{P}]),\sim^{\mathcal{I}[\mathcal{P}]},\widehat{L}^{\prime}}\rangle$,
where $\widehat{L}^{\prime}(X\times Y)=\widehat{L}(\delta(X\times Y))$ for
every $X\times Y\in\mathsf{F}(\mathcal{I}[\mathcal{P}])$.

To show the unsolvability of $k$-set agreement, we will resort to the
following property of product update with factual change. (This claim follows
from Theorem 2.1 and certain properties of product updates with factual
change. For the details, see the discussion in the proof of Theorem 19 in
[21].)

######  Theorem 3.1.

Let $\mathcal{I}[\mathcal{T}]$ and $\mathcal{I}[\mathcal{P}]$ be the product
update models of a task and a protocol, respectively. Suppose there exists a
morphism $\delta:\mathcal{I}[\mathcal{P}]\to\mathcal{I}[\mathcal{T}]$. Then,
$\widehat{\mathcal{I}[\mathcal{T}]},\delta(X)\models\varphi$ implies
${\mathcal{I}[\mathcal{P}]}_{\delta},X\models\varphi$, for any
$X\in\mathsf{F}({\mathcal{I}[\mathcal{P}]}_{\delta})$ and positive formula
$\varphi$.

###  3.2 Product update model $\mathcal{I}[\mathcal{SA}_{k}]$ for $k$-set
agreement task

The output complex of $k$-set agreement task is specified by the set of facets
$\mathsf{F}(\mathcal{O}_{k})=\bigl{\\{}\\{(0,d_{0}),\ldots,(n,d_{n})\\}\bigm{|}{\lvert}\\{d_{0},\ldots,d_{n}\\}{\rvert}\leq
k,d_{0},\ldots,d_{n}\in\Pi\bigr{\\}}$. Hence the product update model
$\mathcal{I}[\mathcal{SA}_{k}]$ is given by
$\langle\mathsf{F}(\mathcal{I}[\mathcal{SA}_{k}]),$
$\sim^{\mathcal{I}[\mathcal{SA}_{k}]},L\rangle$, where
$\mathsf{F}(\mathcal{I}[\mathcal{SA}_{k}])=\\{I\times O\mid
I\in\mathsf{F}(\mathcal{I}),O\in\mathsf{F}(\mathcal{O}_{k}),\\{v\mid(a,v)\in
I\\}\supseteq\\{d\mid(a,d)\in O\\}\\}$ is the set of facets respecting the
validity condition.

This product update model can be extended to the one with factual change
$\widehat{\mathcal{I}[\mathcal{SA}_{k}]}=\langle\mathsf{F}(\mathcal{I}[\mathcal{SA}_{k}]),\sim^{\mathcal{I}[\mathcal{SA}_{k}]}$,
$\widehat{L}\rangle$, where $\widehat{L}(I\times
O)=\\{\mathsf{input}_{a}^{v}\mid(a,v)\in
I\\}\cup\\{\mathsf{decide}_{a}^{d}\mid(a,d)\in O\\}$ for each $I\times
O\in\mathsf{F}(\mathcal{I}[\mathcal{SA}_{k}])$.

Figure 3: Standard chromatic subdivision of a 2-dimensional simplex with
facets being labeled with ordered set partitions.

###  3.3 Product update model $\mathcal{I}[\mathcal{IS}^{m}]$ for multi-round
$m$-iterated immediate snapshot protocol

In this paper, we assume the read-write shared memory model as a device for
inter-process communication. The topological properties of the read-write
shared memory distributed systems are well understood. As for wait-free
solvability, the read-write shared memory model is equivalent to the iterated
immediate snapshot protocol [3, 9, 18], a multi-round protocol in which
processes communicate via immediate snapshot objects.

In each single round execution of the immediate snapshot protocol, the $n+1$
processes are arranged into an arbitrary sequence of concurrency classes
$A_{1},\ldots,A_{r}$ ($r\geq 1$), a disjoint partition of $\Pi$ by nonempty
sets. According to the arranged order, processes take snapshot: Each process
writes its own input value in a shared memory and collects the values that
have been written so far by other processes and itself. The set of values
collected by a snapshot operation is called a _view_. Processes belonging to
the same concurrency class $A_{q}$ witness the same view, i.e., the set of
values written by the processes of ids $\bigcup_{i=1}^{q}A_{i}$. In the
$m$-iterated multi-round immediate snapshot protocol, each process repeatedly
takes snapshots, using the view of $i$-th round as the input to the subsequent
$(i+1)$-th round.

The virtue of the immediate snapshot model is that each snapshot operation
amounts to a topological operation of subdivision, called the _(iterated)
standard chromatic subdivision_ [13, 11]. Figure 3 illustrates the standard
chromatic subdivision of a 2-dimensional simplex, where each facet of the
subdivision is distinctly labeled by a sequence of concurrency classes, or an
_ordered set partition_. We write $\langle
A_{1}{\mid}A_{2}{\mid}\cdots{\mid}A_{r}\rangle$ to denote an ordered set
partition, where $A_{1},A_{2},\ldots,A_{r}$ ($r>0$) is a sequence of nonempty
subsets such that $\Pi=\bigcup_{i=1}^{r}A_{i}$ [16]. (In what follows, we omit
curly braces in an ordered set partition, say, $\langle
0,1{\mid}2{\mid}3\rangle$ instead of
$\langle\\{0,1\\}{\mid}\\{2\\}{\mid}\\{3\\}\rangle$.)

Let $\gamma,\gamma^{\prime}$, etc. range over ordered set partitions. For a
facet $X\in\mathsf{F}(\mathcal{I})$, we write $X\mathop{\rtimes}\gamma$ to
denote a facet of the standard chromatic subdivision of $X$ that is uniquely
identified by an ordered set partition $\gamma$. The snapshot view of a
process $a$ in a facet $X\mathop{\rtimes}\langle
A_{1}{\mid}A_{2}{\mid}\cdots{\mid}A_{r}\rangle$ of the subdivision is defined
by:

$\displaystyle\mathit{view}_{a}(X\mathop{\rtimes}\langle
A_{1}{\mid}A_{2}{\mid}\cdots{\mid}A_{r}\rangle)={}$ $\displaystyle\\{(b,v)\in
X\mid b\in\textstyle\bigcup_{i=1}^{q}A_{i}\\},\text{ where $a\in A_{q}$.}$

In other words, a facet $X\mathop{\rtimes}\langle
A_{1}{\mid}A_{2}{\mid}\cdots{\mid}A_{r}\rangle$ denotes a set of vertexes
$\bigl{\\{}\bigl{(}a,\mathit{view}_{a}(X\mathop{\rtimes}\langle
A_{1}{\mid}A_{2}{\mid}\cdots$ ${\mid}A_{r}\rangle)\bigr{)}\mid
a\in\Pi\bigr{\\}}$. We also write
$X\mathop{\rtimes}\gamma_{1}\mathop{\rtimes}\cdots\mathop{\rtimes}\gamma_{m}$
($m\geq 1$) to denote a facet of subdivision by an $m$-iterated immediate
snapshot, where each ordered set partition $\gamma_{i}$ corresponds to the
$i$-th snapshot, with $\mathop{\rtimes}$ associating to left. The snapshot
view is defined by induction on $m$.

The product update model of the $m$-iterated immediate snapshot protocol is
given by
$\mathcal{I}[\mathcal{IS}^{m}]=\langle\mathsf{F}(\mathcal{I}[\mathcal{IS}^{m}]),$
$\sim^{\mathcal{I}[\mathcal{IS}^{m}]},L^{\prime}\rangle$, where the set of
facets is
$\mathsf{F}(\mathcal{I}[\mathcal{IS}^{m}])=\\{X\mathop{\rtimes}\gamma_{1}\mathop{\rtimes}\cdots\mathop{\rtimes}\gamma_{m}\mid
X\in\mathsf{F}(\mathcal{I}),\gamma_{1},\ldots,\gamma_{m}$ are ordered set
partitions of $\Pi\\}$333Formally, a facet in $\mathcal{I}[\mathcal{IS}^{m}]$
must be written in the form
$X\times(X\mathop{\rtimes}\gamma_{1}\mathop{\rtimes}\cdots\mathop{\rtimes}\gamma_{m})$,
with duplicates of $X$, but for brevity we write it in the abridged notation
$X\mathop{\rtimes}\gamma_{1}\mathop{\rtimes}\cdots\mathop{\rtimes}\gamma_{m}$.
An alternative definition of product update proposed in [23] can circumvent
this kind of duplication, but we stick to the original definition. and
$L^{\prime}(X\times\gamma_{1}\mathop{\rtimes}\cdots\mathop{\rtimes}\gamma_{m})=\\{\mathsf{input}_{a}^{v}\mid(a,v)\in
X\\}$ for each
$X\times\gamma_{1}\mathop{\rtimes}\cdots\mathop{\rtimes}\gamma_{m}\in\mathsf{F}(\mathcal{I}[\mathcal{IS}^{m}])$.

In [16], using ordered set partition, Kozlov gave the combinatorial
description of incidence of facets contained in the standard chromatic
subdivision of a simplex. This entails that the facets in
$\mathcal{I}[\mathcal{IS}]$ admit the following incidence relation, which is
suitable for the subsequent discussion.

Suppose $0\leq d\leq n$ and $b\in[0,d]$. Let $A=[0,d]\setminus\\{b\\}$ and
$X\mathop{\rtimes}\gamma\in\mathsf{F}(\mathcal{I}[\mathcal{IS}])$ be a facet,
where $X\in\mathsf{F}(\mathcal{I})$ and $\gamma=\langle
A_{1}{\mid}A_{2}{\mid}\cdots{\mid}A_{r}{\mid}d+1{\mid}d+2{\mid}\cdots{\mid}n\rangle$
($r>0$) is an ordered partition of $[0,n]$. Then,
$X\mathop{\rtimes}\gamma\sim_{A}Y\mathop{\rtimes}\langle
A_{1}^{\prime}{\mid}A_{2}^{\prime}{\mid}\cdots{\mid}A_{r^{\prime}}^{\prime}{\mid}d+1{\mid}\cdots{\mid}n\rangle$
holds if and only if either of the following holds.

  * •

$A_{r}=\\{b\\}$, $\langle
A_{1}^{\prime}{\mid}A_{2}^{\prime}{\mid}\cdots{\mid}A_{r^{\prime}}^{\prime}{\mid}d+1{\mid}\cdots{\mid}n\rangle=\gamma$,
and $X\sim_{A}Y$.

  * •

$A_{r}\neq\\{b\\}$, $X=Y$, and $\langle
A_{1}^{\prime}{\mid}A_{2}^{\prime}{\mid}\cdots{\mid}A_{r^{\prime}}^{\prime}{\mid}d+1{\mid}\cdots{\mid}n\rangle$
is either $\gamma$ or $\underline{\gamma}_{A}$, where

$\displaystyle\underline{\gamma}_{A}={}$ $\displaystyle\begin{cases}\langle
A_{1}{\mid}\cdots{\mid}A_{r-1}{\mid}A_{r}{\setminus}\\{b\\}{\mid}\,b\,{\mid}d+1{\mid}\cdots{\mid}n\rangle&\text{if
$b\in A_{r}$, ${\lvert}A_{r}{\rvert}>1$,}\\\ \langle
A_{1}{\mid}\cdots{\mid}A_{s-1}{\mid}A_{s}{\setminus}\\{b\\}{\mid}\,b\,{\mid}A_{s+1}{\mid}\cdots{\mid}A_{r}{\mid}d+1{\mid}\cdots{\mid}n\rangle&\text{if
$b\in A_{s}$, ${\lvert}A_{s}{\rvert}>1$ ($s<r$),}\\\ \langle
A_{1}{\mid}\cdots{\mid}A_{s-1}{\mid}A_{s+1}{\cup}\\{b\\}{\mid}\cdots{\mid}A_{r}{\mid}d+1{\mid}\cdots{\mid}n\rangle&\text{if
$A_{s}=\\{b\\}$ ($s<r$).}\end{cases}$

This extends to the multi-round model $\mathcal{I}[\mathcal{IS}^{m}]$ as
follows.

######  Proposition 3.2.

Suppose $0\leq d\leq n$ and $b\in[0,d]$. Let $A=[0,d]\setminus\\{b\\}$ and
$X\mathop{\rtimes}\gamma_{1}\mathop{\rtimes}\cdots\mathop{\rtimes}\gamma_{m}\in\mathsf{F}(\mathcal{I}[\mathcal{IS}^{m}])$,
where each $\gamma_{i}$ is an ordered set partition of the restricted form
$\langle
A_{1}{\mid}A_{2}{\mid}\cdots{\mid}A_{r_{i}}{\mid}d+1{\mid}\cdots{\mid}n\rangle$.
Then,
$X\mathop{\rtimes}\gamma_{1}\mathop{\rtimes}\cdots\mathop{\rtimes}\gamma_{m}\sim_{A}Y\mathop{\rtimes}\gamma_{1}^{\prime}\mathop{\rtimes}\cdots\mathop{\rtimes}\gamma_{m}^{\prime}$,
where each $\gamma_{i}^{\prime}$ is an ordered set partition of the same
restricted form, holds if and only if either of the following hold.

  * •

$A_{r_{i}}=\\{b\\}$ and $\gamma_{i}^{\prime}=\gamma_{i}$ holds for every $i$
and also $X\sim_{A}Y$.

  * •

$A_{r_{i}}\neq\\{b\\}$ for some $i$, $X=Y$, and
$\gamma_{i}^{\prime}=\gamma_{i}$ holds for every $i$ except for the minimum
index $j$ such that $A_{r_{j}}\neq\\{b\\}$ and $\gamma_{j}^{\prime}$ is either
$\gamma_{j}$ or $\underline{\gamma_{j}}_{A}$.

###  3.4 Logical properties of product update models
$\widehat{\mathcal{I}[\mathcal{SA}_{k}]}$ and $\mathcal{I}[\mathcal{IS}^{m}]$

In the sequel, let $\sigma,\tau$, etc. range over facets of a product update
model.

In both $\widehat{\mathcal{I}[\mathcal{SA}_{k}]}$ and
$\mathcal{I}[\mathcal{IS}^{m}]$, the following formula $\mathrm{IFUN}$ is
valid.

$\displaystyle\mathrm{IFUN}={}$
$\displaystyle\textstyle\bigwedge_{a\in\Pi}\bigl{(}\bigwedge_{i,j\in\Pi,i\neq
j}\neg(\mathsf{input}_{a}^{i}\wedge\mathsf{input}_{a}^{j})\wedge\bigvee_{i\in\Pi}\mathsf{input}_{a}^{i}\bigr{)}$
(1)

This formula is intended to mean that each process $a$ is given a unique input
value.

In $\widehat{\mathcal{I}[\mathcal{SA}_{k}]}$, the following formulas
concerning output values are also valid.

$\displaystyle\mathrm{OFUN}={}$
$\displaystyle\textstyle\bigwedge_{a\in\Pi}\bigl{(}\bigwedge_{d,e\in\Pi,d\neq
e}\neg(\mathsf{decide}_{a}^{d}\wedge\mathsf{decide}_{a}^{e})\wedge\bigvee_{d\in\Pi}\mathsf{decide}_{a}^{d}\bigr{)}$
(2) $\displaystyle\mathrm{VALID}={}$
$\displaystyle\textstyle\bigwedge_{a\in\Pi}\bigwedge_{d\in\Pi}\bigl{(}\mathsf{decide}_{a}^{d}\Rightarrow\bigvee_{b\in\Pi}\mathsf{input}_{b}^{d}\bigr{)}$
(3) $\displaystyle\mathrm{AGREE}_{k}={}$
$\displaystyle\textstyle\bigvee_{A\subseteq\Pi,0<{\lvert}A{\rvert}\leq
k}\bigwedge_{a\in\Pi}\bigvee_{d\in A}\mathsf{decide}_{a}^{d}$ (4)
$\displaystyle\mathrm{KNOW}={}$
$\displaystyle\textstyle\bigwedge_{A\subseteq\Pi}\bigwedge_{a\in
A}\bigwedge_{d\in\Pi}\bigl{(}\mathsf{decide}_{a}^{d}\Rightarrow\mathop{\mathrm{D}_{A}}\mathsf{decide}_{a}^{d}\bigr{)}$
(5)

The formula $\mathrm{OFUN}$ means that each process $a$ decides a unique
output value. The formula $\mathrm{VALID}$ expresses the validity condition:
Any output value $d$ must have been input to some of the processes. The
formula $\mathrm{AGREE}_{k}$ specifies that output values must be decided
among at most $k$ different values. Finally, the formula $\mathrm{KNOW}$
indicates that, given two facets $\sigma$ and $\sigma^{\prime}$ such that
$\sigma\sim_{A}\sigma^{\prime}$, any process $a\in A$ decides the same output
value $d$ at both $\sigma$ and $\sigma^{\prime}$.

##  4 Proving Unsolvability of $k$-Set Agreement by Logical Method

Let us revisit the the original proof of Sperner’s lemma [5], which has been
applied to show the unsolvability of $k$-set agreement task. Suppose we have a
fully-colored $d+1$-dimensional simplex $X$ such that $\chi(X)=[0,d]$ and also
a subdivision of $X$ with Sperner coloring. The proof proceeds by induction on
dimension. Assume that, for the fully-colored $d$-dimensional face $Y$ of $X$
such that $\chi(Y)=[0,d-1]$, the subdivision of $Y$ contains an odd number of
fully-colored $d$-dimensional simplexes. The subdivision of $X$ is modeled by
a graph, where the set of graph nodes comprises of the $d+1$-dimensional
simplexes of the subdivision of $X$ and a special extra node. The extra node
is connected by a graph edge to each $d+1$-dimensional simplex of the
subdivision of $X$ that has an $d$-dimensional simplex of the subdivision of
$Y$ as a face. Further, a pair of $d+1$-dimensional simplexes are connected by
an edge if and only if they share a common $d$-dimensional face whose vertexes
are distinctly colored by $[0,d-1]$. In this graph, a graph node has an odd
degree, if and only if either it is the special extra node or a fully-colored
$d+1$-dimensional simplex. Therefore, by a simple fact from graph theory that
every graph has an even number of nodes of odd degree, we conclude that the
subdivision of $X$ contains an odd number of fully-colored $d+1$-dimensional
simplexes.

In the proceeding proof, instead of counting the number of relevant simplexes
in a graph, we exploit graph connectivity by using fixpoints and distributed
knowledge modality of epistemic $\mu$-calculus. Specifically, assuming the
solvability of $k$-set agreement, we provide a concrete epistemic
$\mu$-calculus formula that entails the existence of a cycle-free, ever-
lasting path, which contradicts to the finiteness of the graph.

###  4.1 Proving unsolvability with an epistemic $\mu$-calculus formula

To show the unsolvability of the $k$-set agreement task, let us assume, by
contradiction, that there exists a morphism
$\delta:\mathcal{I}[\mathcal{IS}^{m}]\to\mathcal{I}[\mathcal{SA}_{k}]$.

For any nonempty subset $A$ of $\Pi$, let us define
$\mathrm{DEC}_{A}=\bigwedge_{d=0}^{{\lvert}A{\rvert}-1}\bigvee_{a\in
A}\mathsf{decide}_{a}^{d}$. It is easy to see that the following epistemic
$\mu$-calculus formula

$\displaystyle\Phi_{k}={}$ $\displaystyle\nu
Z.\Bigl{[}\mathrm{OFUN}\wedge\mathrm{VALID}\wedge\bigwedge_{\emptyset\subsetneq
A\subseteq\Pi}\bigl{(}\mathrm{DEC}_{A}\Rightarrow\mathop{\mathrm{D}_{A}}(\mathrm{KNOW}\wedge\mathrm{AGREE}_{k}\wedge
Z)\bigr{)}\Bigr{]}$ (6)

is valid in the product update model with factual change
$\widehat{\mathcal{I}[\mathcal{SA}_{k}]}$, because $\mathrm{OFUN}$,
$\mathrm{VALID}$, $\mathrm{KNOW}$, $\mathrm{AGREE}_{k}$ are all valid formulas
in $\widehat{\mathcal{I}[\mathcal{SA}_{k}]}$. Then Theorem 3.1 implies that
$\Phi_{k}$ is also valid in ${\mathcal{I}[\mathcal{IS}^{m}]}_{\delta}$. In
what follows, we will show that this cannot happen, that is,
${\mathcal{I}[\mathcal{IS}^{m}]}_{\delta},\sigma\not\models\Phi_{k}$ for some
$\sigma\in\mathsf{F}(\mathcal{I}[\mathcal{IS}^{m}])$.

Figure 4: The collections of facets $F_{0}$, $F_{1}$, $F_{2}$ in the product
update model ${\mathcal{I}[\mathcal{IS}^{2}]}_{\delta}$. The dotted orange
lines and solid blue lines indicate the (incomplete) path of facets connected
by the relation $\mathrel{\frown_{\\{0\\}}}$ and
$\mathrel{\frown_{\\{0,1\\}}}$, respectively. The number put on top of each
vertex is the output value.

Let $I_{0},\ldots,I_{n}\in\mathsf{F}(\mathcal{I})$ be facets of the input
complex $\mathcal{I}$ defined by

$\displaystyle I_{d}={}$ $\displaystyle\\{(i,i)\mid
i\in[0,d]\\}\cup\\{(i,d)\mid i\in[d+1,n]\\}$

and also
$F_{0},\ldots,F_{n}\subseteq\mathsf{F}({\mathcal{I}[\mathcal{IS}^{m}]}_{\delta})$
be collections of the facets in ${\mathcal{I}[\mathcal{IS}^{m}]}_{\delta}$
defined by

$\displaystyle\quad F_{d}={}$
$\displaystyle\\{I_{d}\mathop{\rtimes}\gamma_{1}\mathop{\rtimes}\cdots\mathop{\rtimes}\gamma_{m}\mid\parbox[t]{325.215pt}{$\gamma_{i}=\langle
A_{i,1}{\mid}\cdots{\mid}A_{i,r_{i}}{\mid}d+1{\mid}\cdots{\mid}n\rangle$
($r_{i}\geq 1$) is an ordered set partition of $[0,n]\\}$.}$

Each collection $F_{d}$ is intended to represent the graph nodes in the proof
of Sperner’s lemma. Each facet in $F_{d}$ has a $d$-dimensional face that is a
simplex of the subdivision of the $d$-dimensional face
$I_{d}^{\prime}=\\{(i,i)\mid i\in[0,d]\\}$ of $I_{d}$. Conversely, each
$d$-dimensional simplex of the subdivision of $I_{d}^{\prime}$ is a face of a
unique facet
$I_{d}\mathop{\rtimes}\gamma_{1}\mathop{\rtimes}\cdots\mathop{\rtimes}\gamma_{m}\in
F_{d}$, where the uniqueness is due to the complementary vertexes
$\\{(i,d)\mid i\in[d+1,n]\\}$ in $I_{d}$ and the trailing sequence
${\mid}d+1{\mid}\cdots{\mid}n\rangle$ in each ordered set partition
$\gamma_{j}$.

We define an irreflexive symmetric relation $\mathrel{\frown_{A}}$ over
$\bigcup_{d=0}^{k}F_{d}$, which corresponds to the graph edges defined in the
proof of Sperner’s lemma: For every
$\sigma,\sigma^{\prime}\in\bigcup_{d=0}^{k}F_{d}$,
$\sigma\mathrel{\frown_{A}}\sigma^{\prime}$ holds iff

  * •

$\sigma\sim_{A}\sigma^{\prime}$ and $\sigma\neq\sigma^{\prime}$,

  * •

$A\subseteq[\,0,{\lvert}A{\rvert}\,]$,

  * •

$\sigma\in F_{d}$, $\sigma^{\prime}\in F_{e}$ for some $d,e$ such that
$\max(d,e)={\lvert}A{\rvert}$ and ${\lvert}d-e{\rvert}\leq 1$, and

  * •

${\mathcal{I}[\mathcal{IS}^{m}]}_{\delta},\sigma\models\mathrm{DEC}_{A}$ and
${\mathcal{I}[\mathcal{IS}^{m}]}_{\delta},\sigma^{\prime}\models\mathrm{DEC}_{A}$.

Figure 4 depicts, for the case of three processes, the collections of facets
$F_{0}$, $F_{1}$, $F_{2}$ in $\mathcal{I}[\mathcal{IS}^{2}]$ and how the
facets are related by $\mathrel{\frown_{A}}$. Note that, unlike the proof of
Sperner’s lemma where a graph is constructed for each different dimension, we
define the relation $\mathrel{\frown_{A}}$ for all dimensions at once. Instead
of putting a special graph node for each dimension, we allow a pair of facets
$\sigma\in F_{d}$ and $\sigma\in F_{d+1}^{\prime}$ to be related, if they
share a $d$-dimensional common face whose vertexes are colored by $[0,d-1]$.

Particularly when $d=1$, we see that $F_{0}$ consists of a single facet
$\sigma_{0}$ that is related solely with a single facet in $F_{1}$.

######  Lemma 4.1.

Let $\gamma_{1}=\cdots=\gamma_{m}=\langle 0{\mid}1{\mid}\cdots{\mid}n\rangle$.
We have $F_{0}=\\{\sigma_{0}\\}$, where
$\sigma_{0}=I_{0}\mathop{\rtimes}\gamma_{1}\mathop{\rtimes}\cdots\mathop{\rtimes}\gamma_{m}$.
Also, $\sigma_{0}\mathrel{\frown_{A}}\sigma^{\prime}$ iff $A=\\{0\\}$ and
$\sigma^{\prime}=I_{1}\mathop{\rtimes}\gamma_{1}\mathop{\rtimes}\cdots\mathop{\rtimes}\gamma_{m}$.

More generally, up to certain condition that is compelled by the formula
$\Phi_{k}$, each facet in $F_{0},F_{1},\ldots,F_{k}$ other than $\sigma_{0}$
is related with zero or two facets by $\mathrel{\frown_{A}}$.

######  Proposition 4.2.

Suppose ${\mathcal{I}[\mathcal{IS}^{m}]}_{\delta}\models\mathrm{VALID}$. For
any $\sigma\in F_{d}$ ($1\leq d\leq k$) such that
${\mathcal{I}[\mathcal{IS}^{m}]}_{\delta},\sigma\models\mathrm{OFUN}\wedge\mathrm{VALID}\wedge\mathrm{AGREE}_{k}\wedge\mathrm{KNOW}$,
the number of facets $\sigma^{\prime}\in\bigcup_{d=0}^{k}F_{d}$ satisfying
$\sigma\mathrel{\frown_{A}}\sigma^{\prime}$ for some $A$ is either 0 or 2.

###### Proof.

Given $\sigma\in F_{d}$ ($0<d\leq k$) such that
${\mathcal{I}[\mathcal{IS}^{m}]}_{\delta},\sigma\models\mathrm{OFUN}\wedge\mathrm{VALID}\wedge\mathrm{AGREE}_{k}\wedge\mathrm{KNOW}$,
let us define $f_{\sigma}(a)=b$ iff
${\mathcal{I}[\mathcal{IS}^{m}]}_{\delta},\sigma\models\mathsf{decide}_{a}^{b}$.
Then $f_{\sigma}$ is a well-defined total function from $[0,n]$ to $[0,d]$,
because
${\mathcal{I}[\mathcal{IS}^{m}]}_{\delta},\sigma\models\mathrm{OFUN}\wedge\mathrm{VALID}$.

Consider the case $[0,d-1]\not\subseteq f_{\sigma}([0,d])$. Assume, by
contradiction, $\sigma\mathrel{\frown_{A}}\tau$ holds for some $A$ and
$\tau\in F_{e}$ ($0<e\leq k$). Then $[0,d-1]\subseteq f_{\sigma}(A)$ holds
from ${\mathcal{I}[\mathcal{IS}^{m}]}_{\delta},\sigma\models\mathrm{DEC}_{A}$.
If either $e=d-1$ or $e=d$, $\sigma\mathrel{\frown_{A}}\tau$ implies
$A\subseteq[0,d]$; If $e=d+1$, $\sigma\sim_{A}\tau$ implies $A\subseteq[0,d]$,
because $\sigma$ and $\tau$ are a subdivision of $I_{d}$ and $I_{d+1}$,
respectively, and $\chi(I_{d}\cap I_{d+1})=[0,d]$. In either case, we have
$[0,d-1]\subseteq f_{\sigma}(A)\subseteq f_{\sigma}([0,d])$, a contradiction.
Therefore $\sigma\mathrel{\frown_{A}}\tau$ does not hold for any $\tau$ and
$A$.

Consider the other case $[0,d-1]\subseteq f_{\sigma}([0,d])$. Then, either of
the following hold:

  1. (a)

$d\in f_{\sigma}([0,d])$. In this case, $f_{\sigma}$ is a bijection on
$[0,d]$. In order for $\tau\mathrel{\frown_{A}}\sigma$ to hold for some
$\sigma$, $A$ must be either $B_{0}=[0,d]$ or $B_{1}$ such that such that
$B_{1}\subseteq[0,d]$, ${\lvert}B_{1}{\rvert}=d$, and
$f_{\sigma}(B_{1})=[0,d-1]$. (This implies $d<k$, because
${\mathcal{I}[\mathcal{IS}^{m}]}_{\delta},\sigma\models\mathrm{AGREE}_{k}$.)

  2. (b)

$d\not\in f_{\sigma}([0,d])$. In this case, $f_{\sigma}$ is a surjection from
$[0,d]$ to $[0,d-1]$. In order for $\tau\mathrel{\frown_{A}}\sigma$ to hold
for some $\sigma$, $A$ must be either of $B_{2},B_{3}\subseteq[0,d]$ such that
${\lvert}B_{2}{\rvert}={\lvert}B_{3}{\rvert}=d$, ${\lvert}B_{2}\cap
B_{3}{\rvert}=d-1$, and $f_{\sigma}(B_{2})=f_{\sigma}(B_{3})=[0,d-1]$.

Suppose
$\sigma=I_{d}\mathop{\rtimes}\gamma_{1}\mathop{\rtimes}\cdots\mathop{\rtimes}$
$\gamma_{m}$ is a facet in $F_{d}$, where $\gamma_{j}=\langle
A_{j,1}{\mid}\cdots{\mid}A_{j,r_{j}}{\mid}d{+}1{\mid}\cdots{\mid}n\rangle$ for
each $j$. Let us show that $\sigma$ has a unique facet related by
$\mathrel{\frown_{B_{i}}}$, for each $i\in\\{0,1\\}$ in the case of (a) and
also for each $i\in\\{2,3\\}$ in the case of (b). For the case of $B_{0}$,
$\tau=I_{e}\mathop{\rtimes}\gamma_{1}\mathop{\rtimes}\cdots\mathop{\rtimes}\gamma_{m}\in
F_{e}$ is the sole facet satisfying $\sigma\sim_{B_{0}}\tau$, because
$\sigma\sim_{B_{0}}\tau^{\prime}$ does not hold for any facet
$\tau^{\prime}\in F_{d}$ by Proposition 3.2. For the remining cases, we show
$B\subseteq[0,d]$, ${\lvert}B{\rvert}=d$, and $f_{\sigma}(B)=[0,d-1]$ holds,
where $B$ is either $B_{1},B_{2}$, or $B_{3}$. By Proposition 3.2, we have
three cases to consider.

  * •

$B=[0,d-1]$ and $A_{j,r_{j}}=\\{d\\}$ for each $j$.
There is no facet $\tau\in F_{d}$ satisfying $\sigma\sim_{B}\tau$ by
Proposition 3.2. Hence the sole facet satisfying $\sigma\sim_{B}\tau$ is
$\tau=I_{e}\mathop{\rtimes}\gamma_{1}\mathop{\rtimes}\cdots\mathop{\rtimes}\gamma_{m}\in
F_{e}$.

  * •

$B=[0,d]\setminus\\{c\\}$ for some $c\in[0,d-1]$ and $A_{j,r_{j}}=\\{c\\}$ for
each $j$.
This case cannot happen. Suppose there exists such $c$. Define
$J=\\{(i,v)\mid(i,v)\in I_{d},i\neq c\\}\cup\\{(c,d)\\}$. Then
$I_{d}\sim_{B}J$ and hence $\sigma\sim_{B}\tau$, where
$\tau=J\mathop{\rtimes}\gamma_{1}\mathop{\rtimes}\cdots\mathop{\rtimes}\gamma_{m}$.
Since $f_{\sigma}(B)=[0,d-1]$, it holds that
${\mathcal{I}[\mathcal{IS}^{m}]}_{\delta},\sigma\models\mathsf{decide}_{a}^{c}$
for some $a\in B$. Then,
${\mathcal{I}[\mathcal{IS}^{m}]}_{\delta},\sigma\models\mathrm{KNOW}$ implies
${\mathcal{I}[\mathcal{IS}^{m}]}_{\delta},\tau\models\mathsf{decide}_{a}^{c}$.
However, since
${\mathcal{I}[\mathcal{IS}^{m}]}_{\delta},\tau\models\mathrm{VALID}$, we have
${\mathcal{I}[\mathcal{IS}^{m}]}_{\delta},\tau\models\mathsf{input}_{b}^{c}$
for some $b$, which contradicts to the definition of $J$.

  * •

There exists $j$ such that either ${\lvert}A_{j,r_{j}}{\rvert}>1$ or
$B=[0,d]\setminus A_{j,t}$ where $A_{j,t}=\\{c\\}$ for some $t$ ($1\leq
t<r_{j}$) and $c\in[0,d]$.
Let $\ell$ be the minimum of such $j$. Then, by Proposition 3.2, the sole
facet satisfying $\sigma\sim_{B}\tau$ is
$\tau=I_{d}\mathop{\rtimes}\gamma_{1}^{\prime}\mathop{\rtimes}\cdots\mathop{\rtimes}\gamma_{m}^{\prime}\in
F_{d}$, where $\gamma_{\ell}^{\prime}=\underline{\gamma_{\ell}}_{B}$ and
$\gamma_{i}^{\prime}=\gamma_{i}$ for every $i$ ($i\neq\ell$).

To see $\sigma\mathrel{\frown_{B_{i}}}\tau$ holds for each
$i\in\\{0,1,2,3\\}$, it remains to show
${\mathcal{I}[\mathcal{IS}^{m}]}_{\delta},\sigma\models\mathrm{DEC}_{B_{i}}$
and
${\mathcal{I}[\mathcal{IS}^{m}]}_{\delta},\tau\models\mathrm{DEC}_{B_{i}}$.
The former immediately follows from the definition of $f_{\sigma}$; The latter
follows from the former and
${\mathcal{I}[\mathcal{IS}^{m}]}_{\delta},\sigma\models\mathrm{KNOW}$. ∎

######  Theorem 4.3.

Let $\mathcal{I}[\mathcal{SA}_{k}]$ and $\mathcal{I}[\mathcal{IS}^{m}]$ be the
product update models for $k$-set agreement task and $m$-iterated immediate
snapshot protocol, respectively. If $k\leq n$, there exists no morphism
$\delta$ from $\mathcal{I}[\mathcal{IS}^{m}]$ to
$\mathcal{I}[\mathcal{SA}_{k}]$, meaning that $k$-set agreement task is not
solvable by the iterated immediate snapshot protocol.

###### Proof.

Suppose, by contradiction, there exists such a morphism $\delta$. By Theorem
3.1, we have $\widehat{\mathcal{I}[\mathcal{SA}_{k}]}\models\Phi_{k}$, and
hence ${\mathcal{I}[\mathcal{IS}^{m}]}_{\delta}\models\Phi_{k}$. In
particular, ${\mathcal{I}[\mathcal{IS}^{m}]}_{\delta}\models\mathrm{VALID}$.

Hence it must hold that
${\mathcal{I}[\mathcal{IS}^{m}]}_{\delta},\sigma_{0}\models\Phi_{k}$, where
$\sigma_{0}$ is the sole facet of $F_{0}$. Unfolding $\nu Z$ once, we have
${\mathcal{I}[\mathcal{IS}^{m}]}_{\delta},\sigma_{0}\models\mathrm{OFUN}\wedge\mathrm{VALID}$,
which implies
${\mathcal{I}[\mathcal{IS}^{m}]}_{\delta},\sigma_{0}\models\mathsf{decide}_{0}^{0}$
and hence
${\mathcal{I}[\mathcal{IS}^{m}]}_{\delta},\sigma_{0}\models\mathrm{DEC}_{\\{0\\}}$.
Then, by Lemma 4.1, we can see there exists $\sigma_{1}\in F_{1}$ such that
$\sigma_{0}\mathrel{\frown_{\\{0\\}}}\sigma_{1}$ and hence
${\mathcal{I}[\mathcal{IS}^{m}]}_{\delta},\sigma_{1}\models\mathrm{OFUN}\wedge\mathrm{VALID}\wedge\mathrm{KNOW}\wedge\mathrm{AGREE}_{k}\wedge\Phi_{k}$.

Let us show that, for every $\ell\geq 1$, there exists a path of facets
$\sigma_{0}\mathrel{\frown_{A_{0}}}\sigma_{1}\mathrel{\frown_{A_{1}}}\cdots\mathrel{\frown_{A_{\ell-1}}}\sigma_{\ell}$
such that $\sigma_{0}$, $\sigma_{1},\ldots,\sigma_{\ell}$ are pairwisely
distinct facets in $\bigcup_{i=0}^{k}F_{k}$ and also
${\mathcal{I}[\mathcal{IS}^{m}]}_{\delta},\sigma_{i}\models\mathrm{OFUN}\wedge\mathrm{VALID}\wedge\mathrm{KNOW}\wedge\mathrm{AGREE}_{k}\wedge\Phi_{k}$
holds for every $\sigma_{i}$. We show this by induction on $\ell$. We have
already examined the case $l=1$. Suppose the claim holds up to $\ell$, that
is, $\sigma_{\ell-1}\mathrel{\frown_{A_{\ell-1}}}\sigma_{l}$ and
${\mathcal{I}[\mathcal{IS}^{m}]}_{\delta},\sigma_{\ell}\models\mathrm{OFUN}\wedge\mathrm{VALID}\wedge\mathrm{KNOW}\wedge\mathrm{AGREE}_{k}\wedge\Phi_{k}$.
By Proposition 4.2, $\sigma_{\ell}$ must have a facet $\sigma_{\ell+1}$, other
than $\sigma_{\ell-1}$, such that
$\sigma_{\ell}\mathrel{\frown_{A_{\ell}}}\sigma_{\ell+1}$ for an appropriate
$A_{\ell}$. The relation
$\sigma_{\ell}\mathrel{\frown_{A_{\ell}}}\sigma_{\ell+1}$ implies
${\mathcal{I}[\mathcal{IS}^{m}]}_{\delta},\sigma_{\ell}\models\mathrm{DEC}_{A_{\ell}}$
and hence we have
${\mathcal{I}[\mathcal{IS}^{m}]}_{\delta},\sigma_{\ell+1}\models\mathrm{OFUN}\wedge\mathrm{VALID}\wedge\mathrm{KNOW}\wedge\mathrm{AGREE}_{k}\wedge\Phi_{k}$
again for $\sigma_{\ell+1}$, by unfolding $\nu Z$.

Finally, let us show that $\sigma_{\ell+1}$ is distinct from any other
preceding facets. If $\ell=1$, this immediately follows from Proposition 4.2.
Suppose $\ell>1$ and $\sigma_{\ell+1}=\sigma_{j}$ for some $j$ ($1\leq
j<\ell-1$). Then, by
$\sigma_{j-1}\mathrel{\frown_{A_{j}}}\sigma_{j}\mathrel{\frown_{A_{j+1}}}\sigma_{j+1}$
and Proposition 4.2, either $\sigma_{j-1}$ or $\sigma_{j+1}$ must have been
$\sigma_{\ell}$, which contradicts the induction hypothesis.

The existence of path of distinct facets of arbitrary length contradicts to
the fact that $\bigcup_{i=0}^{k}F_{k}$ is a finite set. Therefore there exists
no morphism $\delta$. ∎

##  5 Set Agreement in Submodel: $k$-Concurrency

Figure 5: The 2-concurrency model $\mathcal{R}_{2}$ for a 3-process system, a
submodel of $\mathcal{I}[\mathcal{IS}^{2}]$ restricted to the shaded facets

The unsolvability argument carried out in Section 4 can be applied to a
submodel of $\mathcal{I}[\mathcal{IS}^{m}]$, if the submodel keeps a relevant
set of facets in $\mathcal{I}[\mathcal{IS}^{m}]$. In this section, let us
examine $k$-concurrency model [7], as an instance of such a submodel.

The _$k$ -concurrency model_, denoted by $\mathcal{R}_{k}$, is a submodel of
$\mathcal{I}[\mathcal{IS}^{2}]$, where the facets in
$\mathcal{I}[\mathcal{IS}^{2}]$ are confined to those corresponding to an
execution in which at most $k$ out of $n+1$ concurrent processes are allowed
to execute the two consecutive iterations of immediate snapshot protocol
simultaneously.

Following [7], we formally define the $k$-concurrency submodel
$\mathcal{R}_{k}$ as follows. For an ordered set partition $\gamma=\langle
A_{1}{\mid}A_{2}{\mid}\cdots{\mid}A_{r}\rangle$ of $\Pi$ and $a\in\Pi$, we
define $\mathit{view}_{a}(\gamma)=\bigcup_{i=1}^{t}A_{i}$, where $a\in A_{t}$.
Also, for a facet
$X\mathop{\rtimes}\gamma_{1}\mathop{\rtimes}\gamma_{2}\in\mathsf{F}(\mathcal{I}[\mathcal{IS}^{2}])$
and a vertex of color $a\in\Pi$, we define the _carrier set_ for $a$ by
$\mathit{carrier}_{a}(X\mathop{\rtimes}\gamma_{1}\mathop{\rtimes}\gamma_{2})=\bigcup_{b\in\mathit{view}_{a}(\gamma_{2})}\mathit{view}_{b}(\gamma_{1})$.
The contention sets [7] for a facet $\sigma\in\mathcal{I}[\mathcal{IS}^{2}]$
are defined by
$\mathit{Cont}(\sigma)=\\{A\subseteq\Pi\mid\mathit{carrier}_{a}(\sigma)=\bigcup_{b\in
A}\mathit{carrier}_{b}(\sigma)$ for every $a\in A\\}$. Then the
$k$-concurrency model $\mathcal{R}_{k}$ is a submodel of
$\mathcal{I}[\mathcal{IS}^{2}]$ with a restricted set of facets
$\mathsf{F}(\mathcal{R}_{k})=\bigl{\\{}\sigma\in\mathcal{I}[\mathcal{IS}^{2}]\bigm{|}{\lvert}A{\rvert}\leq
k\text{ for every $A\in\mathit{Cont}(\sigma)$}\bigr{\\}}$.

Figure 5 illustrates the $2$-concurrency submodel $\mathcal{R}_{2}$ for a
3-process system. The submodel contains all the facets relevant for the
unsolvability argument for $1$-set consensus, namely, $F_{0}$ and $F_{1}$ in
Section 4. We can formally check this containment property as follows.
Remember that all the facets considered in the previous section for $k$-set
agreement (with $m=2$) has the form
$I_{d}\mathop{\rtimes}\gamma_{1}\mathop{\rtimes}\gamma_{2}$ ($d\leq k$) where
both of the ordered set partitions $\gamma_{1},\gamma_{2}$ are of the form
$\langle
A_{1}{\mid}A_{2}{\mid}\cdots{\mid}A_{r}{\mid}\,d+1\,{\mid}\cdots{\mid}n\rangle$.
For such a facet $\sigma$, $\mathit{carrier}_{a}(\sigma)=[0,a]$ if
$a\in[d+1,n]$, while $\mathit{carrier}_{a}(\sigma)\subseteq[0,d]$ if
$a\in[0,d]$. Therefore ${\lvert}A{\rvert}\leq d+1\leq k+1$ for every
$A\in\mathit{Cont}(\sigma)$ and hence
$I_{d}\mathop{\rtimes}\gamma_{1}\mathop{\rtimes}\gamma_{2}\in\mathsf{F}(\mathcal{R}_{k+1})$.

By the same argument in the preceding section, we can show that $k-1$ (or
fewer) set agreement task is not solvable in the $k$-concurrency model.

######  Theorem 5.1.

Let $\mathcal{I}[\mathcal{SA}_{\ell}]$ be the product update model for
$\ell$-set agreement task, $\mathcal{R}_{k}$ be the $k$-concurrency model.
Then there is no morphism $\delta$ from $\mathcal{R}_{k}$ to
$\mathcal{I}[\mathcal{SA}_{\ell}]$, if $\ell<k$.

## References

  * [1] Alexandru Baltag, Lawrence S. Moss, and Sławomir Solecki.  The logic of public announcements, common knowledge, and private suspicions.  In Horacio Arló-Costa, Vincent F. Hendricks, and Johan van Benthem, editors, Readings in Formal Epistemology: Sourcebook, chapter 39, pages 773–812. Springer, 2016.
  * [2] Alexandru Baltag and Sonja Smets.  Learning what others know.  In LPAR-23: 23rd International Conference on Logic for Programming, Artificial Intelligence and Reasoning, volume 73 of EPiC Series in Computing, pages 90–119, 2020.
  * [3] Elizabeth Borowsky and Eli Gafni.  Immediate atomic snapshots and fast renaming (extended abstract).  In Proceedings of the 12th Annual ACM Symposium on Principles of Distributed Computing, pages 41–51. ACM, 1993.
  * [4] Julian C. Bradfield and Colin Stirling.  Modal mu-calculi.  In Patrick Blackburn, J. F. A. K. van Benthem, and Frank Wolter, editors, Handbook of Modal Logic, volume 3 of Studies in logic and practical reasoning, pages 721–756. North-Holland, 2007.
  * [5] Mark de Longueville.  A Course in Topological Combinatorics.  Universitext. Springer, 2013.
  * [6] Ronald Fagin, Joseph Y. Halpern, Yoram Moses, and Moshe Y. Vardi.  Reasoning About Knowledge.  MIT Press, 1995.
  * [7] Eli Gafni, Yuan He, Petr Kuznetsov, and Thibault Rieutord.  Read-write memory and $k$-set consensus as an affine task.  In 20th International Conference on Principles of Distributed Systems (OPODIS 2016), pages 6:1–6:17, 2016.
  * [8] Éric Goubault, Jérémy Ledent, and Sergio Rajsbaum.  A simplicial complex model for dynamic epistemic logic to study distributed task computability.  Information and Computation, 278:104597, 2021.  An earlier version appeared in Proc. of 9th International Symposium on Games, Automata, Logics, and Formal Verification, GandALF 2018.
  * [9] Rachid Guerraoui and Petr Kuznetsov.  Algorithms for Concurrent Systems.  EPFL press, 2018.
  * [10] Joseph Y. Halpern and Yoram Moses.  Knowledge and common knowledge in a distributed environment.  Journal of the ACM, 37(3):549–587, 1990.
  * [11] Maurice Herlihy, Dmitry N. Kozlov, and Sergio Rajsbaum.  Distributed Computing Through Combinatorial Topology.  Morgan Kaufmann, 2013.
  * [12] Maurice Herlihy and Sergio Rajsbaum.  Algebraic spans.  Mathematical Structures in Computer Science, 10(4):549–573, 2000\.
  * [13] Maurice Herlihy and Nir Shavit.  The topological structure of asynchronous computability.  Journal of the ACM, 46(6):858–923, 1999.
  * [14] Sou Hoshino.  Determining existence of logical obstructions to the distributed task solvability, 2022.
  * [15] Dexter Kozen.  Results on the propositional $\mu$-calculus.  Theoretical Computer Science, 27(3):333–354, 1983.
  * [16] Dmitry N. Kozlov.  Chromatic subdivision of a simplicial complex.  Homology, Homotopy and Applications, 14(2):197–209, 2012.
  * [17] Yutaro Nishida.  Impossibility of $k$-set agreement via dynamic epistemic logic (in Japanese).  In Algebraic system, Logic, Language and Related Areas in Computer Sciences II, volume 2188 of RIMS Kôkyûroku, pages 96–105, Feb. 2020.
  * [18] Susumu Nishimura.  Schlegel diagram and optimizable immediate snapshot protocol.  In 21st International Conference on Principles of Distributed Systems, OPODIS 2017, pages 22:1–22:16, 2017.
  * [19] Nikolay V. Shilov and Natalya Olegovna Garanina.  Model checking knowledge and fixpoints.  In Fixed Points in Computer Science, FICS 2002, volume NS-02-2 of BRICS Notes Series, pages 25–39, 2002.
  * [20] Emanuel Sperner.  Neuer beweis für die invarianz der dimensionszahl und des gebietes.  Abhandlungen Hamburg, 6:265–272, 1928.
  * [21] Hans van Ditmarsch, Éric Goubault, Marijana Lazic, Jérémy Ledent, and Sergio Rajsbaum.  A dynamic epistemic logic analysis of equality negation and other epistemic covering tasks.  Journal of Logical and Algebraic Methods in Programming, 121:100662, 2021.
  * [22] Hans van Ditmarsch, Wiebe van der Hoek, and Barteld Kooi.  Dynamic Epistemic Logic, volume 337 of Synthese Library.  Springer, 2008.
  * [23] Diego A. Velázquez, Armando Castañeda, and David A. Rosenblueth.  Communication pattern models: An extension of action models for dynamic-network distributed systems.  In Proceedings Eighteenth Conference on Theoretical Aspects of Rationality and Knowledge, TARK 2021, volume 335 of EPTCS, pages 307–321, 2021.
  * [24] Koki Yagi and Susumu Nishimura.  Logical obstruction to set agreement tasks for superset-closed adversaries, 2020.