Determining Existence of Logical Obstructions to the Distributed Task Solvability ^†^†thanks: This article is a revised version of aurthor’s Master’s thesis [Hoshino:Msc22].

Sou Hoshino Dept. of Mathematics, Kyoto University, Japan; E-mail: [email protected]

Abstract

To study the distributed task solvability, Goubault, Ledent, and Rajsbaum devised a model of dynamic epistemic logic that is equivalent to the topological model for distributed computing. In the logical model, the unsolvability of a particular distributed task can be proven by finding a formula, called logical obstruction. This logical method is very appealing because the concrete formulas that prevent to solve task would have implications of intuitive factors for the unsolvability. However, it has not been well studied when a logical obstruction exists and how to systematically construct a concrete logical obstruction formula, if any. In addition, it is proved that there are some tasks that are solvable but do not admit logical obstructions.

In this paper, we propose a method to prove the non-existence of logical obstructions to the solvability of distributed tasks, based on the technique of simulation. Moreover, we give a method to determine whether a logical obstruction exists or not for a finite protocol and a finite task, and if it exists, construct a concrete obstruction. Using this method, we demonstrate that the language of the standard epistemic logic, without distributed knowledge, does not admit logical obstruction to the solvability of $k$ -set agreement tasks. We also show that there is no logical obstruction for multi-round immediate snapshot even in the language of epistemic logic with distributed knowledge. In addition, for the know-all model, we provide a concrete obstruction formula that shows the unsolvability of the $k$ -set agreement task.

1 Introduction

For decades, topological models have been used to study the solvability of tasks in distributed computing [DBLP:books/mk/Herlihy2013]. In topological models, the possible configurations in distributed computation are represented by a $\Pi$ -colored chromatic simplicial complex, where each vertex is colored by an element taken from $\Pi$ , the set of processes. This allows the unsolvability of the $k$ -set agreement to be proven by examining the connectivity of the simplicial complex that models the protocol [DBLP:books/mk/Herlihy2013, DBLP:conf/podc/HerlihyR94].

Recently, Goubault, Ledent, and Rajsbaum proposed a model of dynamic epistemic logic (DEL), called simplicial model, as a substitute for the conventional topological model [DBLP:journals/iandc/GoubaultLR21]. In the logical model, the unsolvability of a task $T$ by a protocol $P$ is shown as follows: 1. Find a formula $\varphi$ that expresses some property that does not hold in $\mathcal{I}[P]$ , a simplicial model for the protocol, but holds in $\mathcal{I}[T]$ , a simplicial model for the task. 2. Show that $\varphi$ is true in $\mathcal{I}[T]$ but is false in $\mathcal{I}[P]$ . 3. Apply the knowledge gain theorem to conclude that the task cannot be solved by the protocol. Thus, to prove the unsolvability, we only need to find an appropriate formula $\varphi$ . We call such a formula logical obstruction. This logical method is very attractive because it provides a concrete formula that prevents to solve a task, which would contribute to better understanding of unsolvability. In addition, the above procedures 1-3 could be completed without resorting to sophisticated topological tools, such as homotopy group, Nerve lemma, and so on. However, there is no concrete way to obtain logical obstructions, and furthermore, there may be no logical obstruction. Goubault et al. [DBLP:conf/tap/GoubaultLLR19] showed that a certain unsolvable distributed task has no logical obstruction, applying the technique of bisimulation.

So far, concrete instances of logical obstruction have been devised for a limited variations of distributed tasks. Goubault et al. provided instances of logical obstructions for simple tasks such as consensus (or 1-set agreement) and approximate agreement tasks but they left logical obstruction to general $k$ -set agreement task as open problem [DBLP:journals/iandc/GoubaultLR21]. Nishida devised a logical obstruction to general $k$ -set agreement by extending the logic with modality of distributed knowledge [Nishida:Msc20]. Yagi and Nishimura [DBLP:journals/corr/abs-2011-13630] applied Nishida’s obstruction to show the unsolvability of $k$ -set agreement tasks in the superset closed adversary model. However, their logical obstructions to the solvability of $k$ -set agreement tasks work for only single-round protocols but not for multiple-round protocols. This is in contrast to the topological method, which can handle multi-round protocols [DBLP:conf/podc/HerlihyR10, DBLP:journals/jacm/HerlihyS99]. The concrete instances mentioned above seem to indicate that the epistemic logic is so weak that the unsolvability is in general hard to be expressed as an obstruction. Indeed there exists an unsolvable task that has no logical obstruction [DBLP:conf/tap/GoubaultLLR19].

In this study, we are concerned with the ability of epistemic logic in expressing the unsolvability. Particularly, we study two languages of epistemic logic, $\mathcal{L}_{K}$ and $\mathcal{L}_{D}$ , and how the additional expressibility of the latter differentiates the ability. The language $\mathcal{L}_{K}$ is the epistemic logic with the standard epistemic modality $\mathrm{K}_{a}$ , a.k.a. knowledge operator; The language $\mathcal{L}_{D}$ extends $\mathcal{L}_{K}$ with additional modality $\mathrm{D}_{A}$ , called distributed knowledge. The logical obstructions given in [Nishida:Msc20, DBLP:journals/corr/abs-2011-13630] suggest that the distributed knowledge provides more logical obstructions to unsolvable tasks, but it does not preclude that $\mathcal{L}_{K}$ and $\mathcal{L}_{D}$ are equally able to define logical obstructions for unsolvable tasks.

In order to answer this question and find a systematic way for constructing logical obstructions, we apply the technique of simulation over simplicial models to argue the existence of logical obstructions. Simulation is a weaker notion of bisimulation between simplicial models. As we will show in a proceeding section, the knowledge gain theorem can be extended for simulations. Moreover, simulation gives a method to determine whether a logical obstruction exists or not for a finite protocol and a finite task, and if it exists, we provide a procedure for constructing a logical obstruction.

The contributions of this paper are the followings.

•

Simulation between simplicial models is introduced as a means to show that the usual epistemic language $\mathcal{L}_{K}$ admits no logical obstruction.
•

Simulation is extended to incorporate distributed knowledge and provides us a method for proving the non-existence of logical obstruction in the epistemic language $\mathcal{L}_{D}$ with distributed knowledge operator.
•

There exists a procedure that determines the existence of logical obstruction for a given pair of a finite protocol and a finite task. Moreover, in case such a logical obstruction exists, the procedure further constructs a concrete obstruction formula systematically.

We will show the following facts to demonstrate the merit of our approach.

•

The language $\mathcal{L}_{K}$ , without distributed knowledge, admits no logical obstruction for $k$ -set agreement tasks and immediate snapshot protocol, where $k\geq 2$ . Therefore, $\mathcal{L}_{D}$ admits properly larger class of logical obstructions than $\mathcal{L}_{K}$ .
•

The language $\mathcal{L}_{D}$ , with distributed knowledge, admits no logical obstruction for $2$ -set agreement task and multi-round immediate snapshot protocol, where $|\Pi|=3$ . Therefore, although $\mathcal{L}_{D}$ admits more logical obstructions than $\mathcal{L}_{K}$ , it still fails to establish the unsolvability, which can be topologically proven.
•

We generate a concrete logical obstruction for $k$ -set agreement tasks and a protocol in the know-all model [DBLP:journals/tcs/CastanedaFPRRT21].

Table 1: Existence of logical obstructions for varying tasks, protocols and languages of epistemic logic

Task	Protocol	Existence of logical obstruction
Consensus	Immediate snapshot	exist in $\mathcal{L}_{CK}$ [DBLP:journals/iandc/GoubaultLR21]
Approximate agreement	Immediate snapshot	exist in $\mathcal{L}_{K}$ unless solvable [DBLP:journals/iandc/GoubaultLR21]
$k$ -set agreement where $2\leq k<\|\Pi\|$	Single-round immediate snapshot	exist in $\mathcal{L}_{D}$ [Nishida:Msc20], but not exist in $\mathcal{L}_{K}$ [This paper]
	Multi-round immediate snapshot	not exist in $\mathcal{L}_{K}$ and not exist when $\|\Pi\|=3$ in $\mathcal{L}_{D}$ [This paper]
	Instance of know-all model	exist in $\mathcal{L}_{D}$ unless solvable [This paper]
Equality negation with two agents and three input values	Layered message passing	not exist in $\mathcal{L}_{CK}$ [DBLP:conf/tap/GoubaultLLR19]
$\mathcal{L}_{K}$ : the language of epistemic logic with modality of knowledge but without distributed knowledge
$\mathcal{L}_{D}$ : the language of epistemic logic with distributed knowledge
$\mathcal{L}_{CK}$ : the language of epistemic logic with modality of knowledge and common knowledge

The Table 1 summarizes the results of prior works and the present paper.

We notice that the present paper concerns epistemic logic whose atomic propositions can mention solely input values. Epistemic logic with an augmentedset of atomic proposition such as the one proposed in [DBLP:journals/jlap/DitmarschGLLR21] which is more expressive in defining logical obstruction, is out of the scope of the paper.

The rest of the paper is organized as follows. Section 2 defines distributed tasks, protocols, and its solvability with simplicial models of DEL. In Section 3, we introduce the notion of simulation and show that there is no logical obstruction for $k$ -set agreement tasks and immediate snapshot protocol in $\mathcal{L}_{K}$ . In Section 4, we reinforce the simulation with distributed knowledge and show that there is no logical obstruction for $2$ -set agreement task and multi- round immediate snapshot protocol in $\mathcal{L}_{D}$ when $|\Pi|=3$ . In Section LABEL:sec_lo_construction, we give a procedure that determines whether a simulation exists or not and further, in case there is no simulation, produce a logical obstruction. Section LABEL:sec_conclusion concludes the paper.

2 Preliminaries

Throughout the paper, we fix a non empty finite set $\Pi$ for colors, or agents. We write $\mathbb{N}$ to denote the set of non-negative integers.

2.1 Simplicial models

In the topological theory of distributed computing, distributed systems are modeled by simplicial complexes. In [DBLP:journals/iandc/GoubaultLR21], it is shown that simplicial complexes provide Kripke models that is suitable for analysis by epistemic logic.

Definition 2.1 (Chromatic simplicial complex).

A chromatic simplicial complex $\mathcal{C}=(V,S,\chi)$ is a triple consisting of a set $V$ of vertices, a set $S$ of non-empty finite subsets of $V$ and a coloring map $\chi\colon V\to\Pi$ such that $S$ and $\chi$ satisfy the following conditions:

•

$S$ is closed under inclusion, i.e. $X\in S$ and $\emptyset\subsetneq Y\subseteq X\implies Y\in S$ .
•

For any vertex $v\in V$ , $\{v\}\in S$ .
•

For any simplex $X\in S$ , $\chi|_{X}\colon X\to\Pi$ is injective.

Each element of $S$ is called a simplex. We write $X\in\mathcal{C}$ to mean $X$ is a simplex of $C$ , i.e. $X\in S$ . The dimension of a simplex $X\in S$ is defined by $|X|-1$ . A simplex that is maximal with respect to inclusion is called a facet. The set of facets is denoted by $\mathcal{F}({\mathcal{C}})$ . A complex is called pure if all its facets have the same dimension.

In the following, Let $\mathsf{At}=\{\mathtt{input}_{a}^{v}\mid\text{$a\in\Pi$, $v\in V^{in}$}\}$ be a set of atomic propositions, where $V^{in}$ is an arbitrary set of input values. For each $a\in\Pi$ , $\mathsf{At}_{a}=\{\mathtt{input}_{a}^{v}\in\mathsf{At}\mid v\in V^{in}\}$ .

Definition 2.2 (Simplicial model).

A simplicial model $M=(V,S,\chi,l)$ is a pure ( $|\Pi|-1$ )-dimensional chromatic simplicial complex $\mathcal{C}=(V,S,\chi)$ equipped with a labeling map $l\colon V\to\mathcal{P}(\mathsf{At})$ such that $l(v)\subseteq\mathsf{At}_{\chi(v)}$ .

For each $a\in\Pi$ , we define an equivalence relation $\sim_{a}$ over $\mathcal{F}({\mathcal{C}})$ , called an indistinguishability relation, by $X\sim_{a}Y$ if and only if $a\in\chi(X\cap Y)$ . Then $(\mathcal{F}({C}),(\sim_{a})_{a\in\Pi},l)$ gives a multi-agent Kripke model of facets being the set of possible worlds.

In abuse of notation, we may write $\mathcal{F}({M})$ to mean a set of facets $\mathcal{F}({C})$ in its underlying simplicial complex.

Definition 2.3 (Morphism between simplicial models).

Let $M=(V,S,\chi,l)$ , $M^{\prime}=(V^{\prime},S^{\prime},\chi^{\prime},l^{\prime})$ be simplicial models. A morphism $f\colon M\to M^{\prime}$ is a map $f$ from $V$ to $V^{\prime}$ that satisfies the following conditions:

•

For all $X\in S$ , $f(X)\in S^{\prime}$ ,
•

$f$ preserves the coloring, i.e. $\chi^{\prime}(f(v))=\chi(v)$ for any $v\in V$ and
•

$f$ preserves the labeling, i.e. $l^{\prime}(f(v))=l(v)$ for any $v\in V$ .

Definition 2.4 (Input simplicial model).

An input simplicial model is a simplicial model $\mathcal{I}=(V,S,\chi,l)$ where

•

$V\subseteq\Pi\times V^{in}$ ,
•

$X\in S$ if $X$ have at most one $a$ -colored vertex for each color $a\in\Pi$ ,
•

$\chi(a,v)=a$ and
•

$l(a,v)=\{\mathtt{input}_{a}^{v}\}$ .

In the sequel, we assume $V=\Pi\times V^{in}$ . Figure 2 shows an example of an input simplicial model, where each color of vertex is illustrated as a color of node.

Figure 1: Example of an input simplicial model for

\Pi=\{\circ,\bullet\}

V^{in}=\{0,1\}

Figure 2:

\mathcal{I}[\mathcal{SA}_{1}]

for

\Pi=\{\circ,\bullet\}

V^{in}=\{0,1\}

V^{out}=\{0,1\}

2.2 Epistemic logic for simplicial models

Definition 2.5 (Epistemic formula).

We define the language of epistemic formulas $\mathcal{L}_{K}$ as follows:

\varphi::=p\mid\lnot\varphi\mid(\varphi\land\varphi)\mid\mathrm{K}_{a}\varphi

where $p\in\mathsf{At}$ is an atomic proposition and $a\in\Pi$ is an agent.

Definition 2.6.

Given a formula $\varphi\in\mathcal{L}_{K}$ and a facet $X\in\mathcal{F}({M})$ of a simlicial model $M$ , we define the truth of $\varphi$ at $X$ , written $M,X\models\varphi$ , as below by induction on $\varphi$ .

	$\displaystyle M,X\models p$	$\displaystyle\text{if $p\in l(X)$}.$
	$\displaystyle M,X\models\lnot\varphi$	$\displaystyle\text{if $M,X\not\models\varphi$}.$
	$\displaystyle M,X\models\varphi_{1}\land\varphi_{2}$	$\displaystyle\text{if $M,X\models\varphi_{1}$ and $M,X\models\varphi_{2}$}.$
	$\displaystyle M,X\models\mathrm{K}_{a}\varphi$	$\displaystyle\text{if for all Y $\in\mathcal{F}({M})$, $Y\sim_{a}X\implies M,Y\models\varphi$}.$

2.3 Protocols, tasks and solvability with DEL

Protocols and tasks in distributed computing are regarded as transformation of the input configuration to the output. In simplicial models, this can be defined as product update.

Definition 2.7 (Simplicial action model and product update).

A simplicial action model, (or an action model for short) $A=(V,S,\chi,\mathtt{pre})$ is a pure ( $|\Pi|-1$ )-dimensional chromatic simplicial complex $\mathcal{C}=(V,S,\chi)$ equipped with a map $\mathtt{pre}\colon\mathcal{F}({\mathcal{C}})\to\mathcal{L}_{K}$ . Each facet in $\mathcal{F}({\mathcal{C}})$ is called an action and $\mathtt{pre}$ assigns a precondition formula to each action. In abuse of notation, we may write $\mathcal{F}({A})$ to mean a set of facets $\mathcal{F}({C})$ in its underlying simplicial complex.

Let $M=(V_{M},S_{M},\chi_{M},l_{M})$ be a simplicial model and $A=(V_{A},S_{A},\chi_{A},\mathtt{pre})$ be a simplicial action model. A product update model $M[A]=(V,S,\chi,l)$ is a simplicial model defined as follows:

•

$\mathcal{F}({M[A]})=\{X\times_{\Pi}T\mid\text{$X\in\mathcal{F}({M})$, $T\in\mathcal{F}({A})$, $M,X\models\mathtt{pre}(T)$}\}$ ,
•

$\chi(m,a)=\chi_{M}(m)=\chi_{A}(a)$ and
•

$l(m,a)=l_{M}(m)$ ,

where $X\times_{\Pi}T=\{(m,a)\in X\times T\mid\chi_{M}(m)=\chi_{A}(a)\}$ is a subset of the product $X\times T$ whose each element is a tuple of a vertex in $X$ and a vertex in $T$ with the same color.

Definition 2.8 (Task).

A simplicial action model $A=(V,S,\chi,\mathtt{pre})$ is called a task if there exists an injection $\iota\colon\mathcal{F}({A})\to[\Pi,V^{out}]$ such that $T\sim_{a}T^{\prime}$ holds if and only if $\iota(T)(a)=\iota(T^{\prime})(a)$ for any $T,T^{\prime}\in\mathcal{F}({A})$ and $a\in\Pi$ , where $V^{out}$ is an arbitrary set of output values, $[\Pi,V^{out}]$ is the set of functions from $\Pi$ to $V^{out}$ .

Example 2.9 ( $k$ -set agreement task).

We define a task $\mathcal{SA}_{k}$ , where $k=1,\dots,|\Pi|$ , called $k$ -set agreement as follows:

•

$V^{out}=V^{in}$ ,
•

$V=\Pi\times V^{out}$ ,
•

$\mathcal{F}({\mathcal{SA}_{k}})=\{\{(a,decide(a))\mid a\in\Pi\}\mid decide\in[\Pi,V^{out}],|decide(\Pi)|\leq k$ },
•

$\chi(a,d)=a$ and
•

$\mathtt{pre}(\{(a,decide(a))\mid a\in\Pi\})=\bigwedge_{a\in\Pi}\bigvee_{b\in\Pi}\mathtt{input}_{b}^{decide(a)}$ .

This is a well-defined task because there is an injection $\{(a,decide(a))\mid a\in\Pi\}\mapsto decide$ . In what follows, we write $(a,i_{a},d_{a})$ to mean a vertex $((a,i_{a}),(a,d_{a}))$ of $\mathcal{I}[\mathcal{SA}_{k}]$ . we assume the set of input values for the $k$ -set agreement is given by $V^{in}=\Pi$ unless otherwise stated. The product update model $\mathcal{I}[\mathcal{SA}_{1}]$ is as shown in Figure 2, where each color of vertex is illustrated as a color of node and the input $i$ and the decision $d$ is indicated as $i\mapsto d$ .

Using product updates, solvability of distributed tasks is defined as follows.

Definition 2.10 (Solvability).

Let $\mathcal{I}$ be an input simplicial model. A task $T$ is solvable by an action model $P$ , if there exists a morphism $f\colon\mathcal{I}[P]\to\mathcal{I}[T]$ .

3 Non-existence of logical obstructions

In this section, we consider the following language $\mathcal{L}_{K}^{+}$ of positive epistemic formulas:

\varphi::=p\mid\lnot p\mid(\varphi\lor\varphi)\mid(\varphi\land\varphi)\mid\mathrm{K}_{a}\varphi

where $p\in\mathsf{At}$ is an atomic proposition and $a\in\Pi$ is an agent.

3.1 Knowledge gain and logical obstruction

Theorem 3.1 (Knowledge gain [DBLP:journals/iandc/GoubaultLR21]).

Suppose $f\colon M\to M^{\prime}$ be a morphism between simplicial models. Then, for any facet $X\in\mathcal{F}({M})$ and positive formula $\varphi\in\mathcal{L}_{K}^{+}$ , $M^{\prime},f(X)\models\varphi$ implies $M,X\models\varphi$ .

Corollary 3.2.

If there exists a morphism $f\colon M\to M^{\prime}$ , for any positive formula $\varphi\in\mathcal{L}_{K}^{+}$ , $M^{\prime}\models\varphi$ implies $M\models\varphi$ .

Corollary 3.3.

Let $\mathcal{I}$ be an input simplicial model, $T$ be a task and $A$ be an action model. If there exists a positive formula $\varphi\in\mathcal{L}_{K}^{+}$ such that $\mathcal{I}[T]\models\varphi$ and $\mathcal{I}[A]\not\models\varphi$ , the task $T$ is not solvable by $A$ .

A positive formula $\varphi$ such as the one in the above corollary is called a logical obstruction to the solvability of $T$ by $A$ . We simply call $\varphi$ a logical obstruction when $T$ and $A$ are clear from the context.

3.2 Knowledge gain via simulation

Definition 3.4 (Simulation).

Suppose $M$ and $M^{\prime}$ are simplicial models. A simulation of $M$ by $M^{\prime}$ is a binary relation $R\subseteq\mathcal{F}({M})\times\mathcal{F}({M^{\prime}})$ over the facets of simplicial models that satisfies the following properties.

(Atom): For all $X\in\mathcal{F}({M})$ and $X^{\prime}\in\mathcal{F}({M^{\prime}})$ , $X\mathrel{R}X^{\prime}$ implies $l(X)=l^{\prime}(X^{\prime})$ .
(Forth): For all $a\in\Pi$ , $X,Y\in\mathcal{F}({M})$ and $X^{\prime}\in\mathcal{F}({M^{\prime}})$ , if $X\mathrel{R}X^{\prime}$ and $X\sim_{a}Y$ , there exists $Y^{\prime}\in\mathcal{F}({M^{\prime}})$ such that $Y\mathrel{R}Y^{\prime}$ and $X^{\prime}\sim_{a}Y^{\prime}$ .

A simulation $S$ is called total if for all $X\in\mathcal{F}({M})$ , there exists $X^{\prime}\in\mathcal{F}({M^{\prime}})$ such that $X\mathrel{S}X^{\prime}$ . For a facet $X\in\mathcal{F}({M})$ , we say that $S$ is not total at $X$ if there is no $X^{\prime}\in\mathcal{F}({M^{\prime}})$ such that $X\mathrel{S}X^{\prime}$ .

Proposition 3.5.

Suppose $f\colon M\to M^{\prime}$ is a morphism between simplicial models, and define a binary relation $graph(f)\subseteq\mathcal{F}({M})\times\mathcal{F}({M^{\prime}})$ by $graph(f)=\{(X,f(X))\mid X\in\mathcal{F}({M})\}$ . Then, the $graph(f)$ is a total simulation.

Proof.

(Atom): By the definition of morphism, $f$ preserves labeling, i.e. $l(X)=l^{\prime}(f(X))$ .

(Forth): Let $X,Y\in\mathcal{F}({M})$ be facets such that $X\sim_{a}Y$ . Then there exists $a$ -colored vertex $v\in X\cap Y$ . Since $f$ is a color-preserving map, we have $f(v)\in f(X)\cap f(Y)$ and $\chi^{\prime}(f(v))=\chi(v)=a$ . This implies $f(X)\sim_{a}f(Y)$ .

It is clear that $graph(f)$ is total. ∎

Theorem 3.6.

Suppose $S\subseteq\mathcal{F}({M})\times\mathcal{F}({M^{\prime}})$ be a simulation. Then, for any facets $(X,X^{\prime})\in S$ and positive formula $\varphi\in\mathcal{L}_{K}^{+}$ , $M^{\prime},X^{\prime}\models\varphi$ implies $M,X\models\varphi$ .

Proof.

We proceed by induction on $\varphi$ .

For the base case, suppose $\varphi=p$ or $\lnot p$ , where $p$ is an atomic proposition. Since $S$ satisfies the condition (Atom), we have $M,X\models p\iff p\in l(X)\iff p\in l^{\prime}(X^{\prime})\iff M^{\prime},X^{\prime}\models p$ . This implies $M^{\prime},X^{\prime}\models\varphi\implies M,X\models\varphi$ .

The cases of conjunction and disjunction are easily shown by induction hypothesis.

For the case of modal operator, suppose $\varphi=\mathrm{K}_{a}\psi$ . Assuming $M^{\prime},X^{\prime}\models\mathrm{K}_{a}\psi$ , we show that $M,Y\models\psi$ holds for any $Y\in\mathcal{F}({M})$ such that $X\sim_{a}Y$ . By the condition (Forth), there exists $Y^{\prime}\in\mathcal{F}({M^{\prime}})$ such that $Y\mathrel{S}Y^{\prime}$ and $X^{\prime}\sim_{a}Y^{\prime}$ . This implies $M^{\prime},Y^{\prime}\models\psi$ and also $M,Y\models\psi$ by induction hypothesis. Therefore, $M,X\models\mathrm{K}_{a}\psi$ . ∎

Corollary 3.7.

If there exists a total simulation of $M$ by $M^{\prime}$ , for any positive formula $\varphi\in\mathcal{L}_{K}^{+}$ , $M^{\prime}\models\varphi$ implies $M\models\varphi$ .

3.3 Non-existence of logical obstructions to the solvability of $\mathcal{SA}_{k}$ by $\mathcal{IS}^{r}$

The (iterated) immediate snapshot is a protocol that characterizes the wait-free asynchronous distributed computation in the read-write shared memory systems [DBLP:conf/podc/BorowskyG92, DBLP:books/mk/Herlihy2013]. The specification of this protocol is as follows. Let $\Pi$ be a set of processes and suppose that processes in $\Pi$ communicate with each other by iterating the immediate snapshot protocol $r$ times. When a process $a\in\Pi$ finishes immediate snapshot of $i$ -th iteration, it obtains a view $V_{a}\subseteq\{(p,v_{p})\mid p\in\Pi\}$ where $v_{p}$ is the view of $p$ ’s $(i-1)$ -th iteration, assuming the view of $p$ ’s iteration is the initial input value to $p$ . The views $(V_{p})_{p\in\Pi}$ of each round satisfy the following properties.

(Self-inclusion): For all $a\in\Pi$ , $(a,v_{a})\in V_{a}$ .
(Containment): For all $a,b\in\Pi$ , $V_{a}\subseteq V_{b}$ or $V_{b}\subseteq V_{a}$ .
(Immediacy): For all $a,b\in\Pi$ , $(b,v_{b})\in V_{a}$ implies $V_{b}\subseteq V_{a}$ .

The set of views are equally specified by means of ordered partition. The $r$ -iterated immediate snapshot is thus modeled by an action model whose underlying simplicial complex is determined by initial input values and a sequence of $r$ ordered partitions.

Definition 3.8.

An ordered partition of $\Pi$ is a finite sequence $\gamma=(C_{1},\dots,C_{l})$ of subsets of $\Pi$ such that $\emptyset\neq C_{1}\subsetneq C_{2}\subsetneq\dots\subsetneq C_{l}=\Pi$ . We write $\mathrm{OP}_{\Pi}$ for the set of all ordered partitions of $\Pi$ .

Definition 3.9.

Let $\mathcal{I}$ be an input simplicial model. We define a set $\mathsf{Views}^{r}$ of possible views obtained by communicating $r$ -times, by induction on $r$ as

•

$\mathsf{Views}^{0}=V^{in}$ and
•

$\mathsf{Views}^{r+1}=\{\{(p,v_{p})\mid p\in P\}\mid\text{$P\subseteq\Pi$, $v_{p}\in\mathsf{Views}^{r}$}\}$ .

Let $a\in\Pi$ be an agent. We also define a map $view^{r}_{a}\colon\mathcal{F}({\mathcal{I}})\times\mathrm{OP}^{r}_{\Pi}\to\mathsf{Views}^{r}$ , by induction on $r$ as

•

$view^{0}_{a}(\{(b,i_{b})\mid b\in\Pi\})=i_{a}$ and
•

$view^{r+1}_{a}(I,\gamma_{1},\dots,\gamma_{r},(C_{1},\dots,C_{l}))=\{(p,view^{r}_{p}(I,\gamma_{1},\dots,\gamma_{r}))\mid p\in C_{\min\{j\mid a\in C_{j}\}}\}$ .

Definition 3.10.

Let $r\geq 1$ be a natural number. We define an action model $\mathcal{IS}^{r}=(V,S,\chi,\mathtt{pre})$ , for $r$ -iterated immediate snapshot protocol as follows:

•

$V\subseteq\Pi\times V^{in}\times\mathsf{Views}^{r}$ ,
•

$X\in\mathcal{F}({\mathcal{IS}^{r}})$ if there exists a facet $I\in\mathcal{F}({\mathcal{I}})$ and ordered partitions $\gamma_{1},\dots,\gamma_{r}$ such that $X=\{(a,i_{a},view^{r}_{a}(I,\gamma_{1},\dots,\gamma_{r}))\mid(a,i_{a})\in I\}$ ,
•

$\chi(a,i,v)=a$ and
•

$\mathtt{pre}(\{(a,i_{a},v_{a})\mid a\in\Pi\})=\bigwedge_{a\in\Pi}\mathtt{input}_{a}^{i_{a}}$ .

Figure 3: Simplices of

\mathcal{IS}^{1}

, which is isomorphic to

\mathcal{I}[\mathcal{IS}^{1}]

, for the case

\Pi=\{\circ,{\color[rgb]{.75,.75,.75}\definecolor[named]{pgfstrokecolor}{rgb}{.75,.75,.75}\pgfsys@color@gray@stroke{.75}\pgfsys@color@gray@fill{.75}\bullet},\bullet\}

and all process have

0

as input.

The action model $\mathcal{IS}^{1}$ is illustrated in Figure 3, for the case $\Pi=\{\circ,{\color[rgb]{.75,.75,.75}\definecolor[named]{pgfstrokecolor}{rgb}{.75,.75,.75}\pgfsys@color@gray@stroke{.75}\pgfsys@color@gray@fill{.75}\bullet},\bullet\}$ and all process have $0$ as input. For instance, let $X$ be a facet labeled with $\gamma=(\{\bullet\},\{\circ,\bullet\},\{\circ,{\color[rgb]{.75,.75,.75}\definecolor[named]{pgfstrokecolor}{rgb}{.75,.75,.75}\pgfsys@color@gray@stroke{.75}\pgfsys@color@gray@fill{.75}\bullet},\bullet\})$ . Then, the views of each processes are as follows: $view^{1}_{\circ}=\{(\circ,0),(\bullet,0)\}$ and $view^{1}_{{\color[rgb]{.75,.75,.75}\definecolor[named]{pgfstrokecolor}{rgb}{.75,.75,.75}\pgfsys@color@gray@stroke{.75}\pgfsys@color@gray@fill{.75}\bullet}}=\{(\circ,0),({\color[rgb]{.75,.75,.75}\definecolor[named]{pgfstrokecolor}{rgb}{.75,.75,.75}\pgfsys@color@gray@stroke{.75}\pgfsys@color@gray@fill{.75}\bullet},0),(\bullet,0)\}$ , $view^{1}_{\bullet}=\{(\bullet,0)\}$ . This means $X=\{(\circ,0,\{(\circ,0),(\bullet,0)\}),\{({\color[rgb]{.75,.75,.75}\definecolor[named]{pgfstrokecolor}{rgb}{.75,.75,.75}\pgfsys@color@gray@stroke{.75}\pgfsys@color@gray@fill{.75}\bullet},0,\{(\circ,0),({\color[rgb]{.75,.75,.75}\definecolor[named]{pgfstrokecolor}{rgb}{.75,.75,.75}\pgfsys@color@gray@stroke{.75}\pgfsys@color@gray@fill{.75}\bullet},0),(\bullet,0)\}),\{(\bullet,0,\{(\bullet,0)\})\}$ .

Let $\mathcal{I}$ be an input simplicial model. The underlying simplicial complex of the product update model $\mathcal{I}[\mathcal{IS}^{r}]$ is equivalent to the one of the action model $\mathcal{IS}^{r}$ up to a simplicial map $((a,i_{a}),(a,i_{a},v_{a}))\mapsto(a,i_{a},v_{a})$ .

In what follows, we write $(a,i_{a},v_{a})$ , in abuse of notation, to mean a vertex $((a,i_{a}),(a,i_{a},v_{a}))$ of $\mathcal{I}[\mathcal{IS}^{r}]$ . We also write $I[\gamma_{1},\dots,\gamma_{r}]$ for a facet $\{(a,i_{a},view^{r}_{a}(I,\gamma_{1},\dots,\gamma_{r}))\mid(a,i_{a})\in I\}$ .

Definition 3.11.

We define a map $carrier\colon\bigcup_{r\geq 1}\mathsf{Views}^{r}\to\mathsf{Views}^{1}$ as

carrier(w)=\begin{cases}w,&\text{(if $w\in\mathsf{Views}^{1}$)}\\ \bigcup_{p\in P}carrier(v_{p}),&\text{(otherwise)}\end{cases}

where $P\subseteq\Pi$ is a set of agents and $(v_{p})_{p\in P}$ is a family of views such that $w=\{(p,v_{p})\mid p\in P\}$ .

Lemma 3.12.

Let $I\in\mathcal{F}({\mathcal{I}})$ be a facet of an input simplicial model and $\gamma_{1},\gamma_{2},\ldots\in\mathrm{OP}_{\Pi}$ be ordered partitions of $\Pi$ , where $\gamma_{1}=(C_{1},\dots,C_{l})$ . For any $r\geq 1$ and $a\in\Pi$ , the following holds:

\{(p,i_{p})\in I\mid p\in C_{1}\}\subseteq carrier(view^{r}_{a}(I,\gamma_{1},\dots,\gamma_{r}))\subseteq I.

Proof.

We proceed by induction on $r$ . Given an agent $a\in\Pi$ , let us write $j_{a}$ to denote $\min\{j\mid a\in C_{j}\}$ .

For the base case $r=1$ , we have $carrier(view^{1}_{a}(I,\gamma_{1}))=\{(q,i_{q})\in I\mid q\in C_{j_{a}}\}\subseteq I$ and $\{(p,i_{p})\mid p\in C_{1}\}\subseteq\{(q,i_{q})\mid q\in C_{j_{a}}\}$ since $C_{1}\subseteq C_{j}$ for any $1\leq j\leq l$ .

For the case $r+1$ , we have

	$\displaystyle carrier(view^{r+1}_{a}(I,\gamma_{1},\dots,\gamma_{r+1}))$
	$\displaystyle=carrier(\{(q,i_{q},view^{r}_{q}(I,\gamma_{1},\dots,\gamma_{r}))\mid q\in C_{j_{a}}\})$
	$\displaystyle=\bigcup_{q\in C_{j_{a}}}carrier(view^{r}_{q}(I,\gamma_{1},\dots,\gamma_{r})).$

By induction hypothesis, we obtain

	$\displaystyle\{(p,i_{p})\mid p\in C_{1}\}$	$\displaystyle=\bigcup_{q\in C_{j_{a}}}\{(p,i_{p})\mid p\in C_{1}\}$
		$\displaystyle\subseteq\bigcup_{q\in C_{j_{a}}}carrier(view^{r}_{q}(I,\gamma_{1},\dots,\gamma_{r}))$
		$\displaystyle\subseteq\bigcup_{q\in C_{j_{a}}}I=I.$

Thus, $\{(p,i_{p})\mid p\in C_{1}\}\subseteq carrier(view^{r+1}_{a}(I,\gamma_{1},\dots,\gamma_{r}))\subseteq I$ holds. ∎

The topological model of (iterated) immediate snapshot is studied [DBLP:journals/jacm/HerlihyS99] and it has been shown that the $k$ -set agreement task is unsolvable by $r$ -round immediate snapshot for any $r\geq 1$ and $1\leq k<|\Pi|$ . It is desirable to have a logical obstruction, but there is no such a formula.

The following theorem shows that $\mathcal{L}_{K}^{+}$ admits no logical obstruction to $k$ -set agreement for any $k\geq 2$ .

Theorem 3.13.

There is no logical obstruction to the solvability of $\mathcal{SA}_{k}$ by $\mathcal{IS}^{r}$ in $\mathcal{L}_{K}^{+}$ , whenever $k\geq 2$ .

Proof.

Let $S\subseteq\mathcal{F}({\mathcal{I}[\mathcal{IS}^{r}]})\times\mathcal{F}({\mathcal{I}[\mathcal{SA}_{k}]})$ be a binary relation defined as

$\displaystyle\{(a,i_{a},v_{a})\mid a\in\Pi\}\mathrel{S}\{(a,i^{\prime}_{a},d_{a})\mid a\in\Pi\}\iff$	(1)	for all $a\in\Pi$ , $i_{a}=i^{\prime}_{a}$ and
	(2)	for all $a\in\Pi$ , there exists $a^{\prime}\in\Pi$
such that $(a^{\prime},d_{a})\in carrier(v_{a})$ .

By Corollary 3.7, it suffices to show that $S$ is a total simulation.

Let us first show $S$ is a simulation.

(Atom): The labeling of facets is given by $l_{\mathcal{I}[\mathcal{IS}^{r}]}(\{(a,i_{a},v_{a})\mid a\in\Pi\})=\{\mathtt{input}^{i_{a}}_{a}\mid a\in\Pi\}$ and $l_{\mathcal{I}[\mathcal{SA}_{k}]}(\{(a,i^{\prime}_{a},d_{a})\mid a\in\Pi\})=\{\mathtt{input}^{i^{\prime}_{a}}_{a}\mid a\in\Pi\}$ . Thus, (Atom) follows from the definition of $S$ .

(Forth): Suppose $a_{0}\in\Pi$ is an agent, $X,Y$ are facets of $\mathcal{I}[\mathcal{IS}^{r}]$ and $X^{\prime}$ is a facet of $\mathcal{I}[\mathcal{SA}_{k}]$ such that $X\mathrel{S}X^{\prime}$ and $X\sim_{a_{0}}Y$ . Let $I\in\mathcal{F}({\mathcal{I}})$ be a facet of the input simplicial complex and $\gamma_{1},\dots,\gamma_{r}$ be ordered partitions such that $Y=I[\gamma_{1},\dots,\gamma_{r}]$ , where $\gamma_{1}=(C_{1},\dots,C_{j})$ . Fix an agent $a_{1}\in C_{1}$ .

For all $a\in\Pi$ , let us write $input_{X}(a)$ for an input value and $view_{X}(a)$ for a view in $\mathsf{Views}^{r}$ such that $(a,input_{X}(a),view_{X}(a))$ is an $a$ -colored vertex in $X$ . Similarly, let us write $(a,input_{Y}(a),view_{Y}(a))$ for an $a$ -colored vertex in $Y$ , and $(a,input_{X^{\prime}}(a),decide_{X^{\prime}}(a))$ for an $a$ -colored vertex in $X^{\prime}$ .

We define a facet $Y^{\prime}\in\mathcal{I}[\mathcal{SA}_{k}]$ by

Y^{\prime}=\{(a_{0},input_{Y}(a_{0}),decide_{X^{\prime}}(a_{0}))\}\cup\{(a,input_{Y}(a),input_{Y}(a_{1}))\mid a\in\Pi\setminus\{a_{0}\}\}.

Let us write $(a,input_{Y^{\prime}}(a),decide_{Y^{\prime}}(a))$ for an $a$ -colored vertex in $Y^{\prime}$ for all $a\in\Pi$ as above. Then, we have $input_{Y^{\prime}}(a)=input_{Y}(a)$ for all $a\in\Pi$ , $decide_{Y^{\prime}}(a_{0})=decide_{X^{\prime}}(a_{0})$ and $decide_{Y^{\prime}}(a)=input_{Y}(a_{1})$ for all $a\in\Pi\setminus\{a_{0}\}$ .

We prove that $Y^{\prime}\in\mathcal{F}({\mathcal{I}[\mathcal{SA}_{k}]})$ , $X^{\prime}\sim_{a_{0}}Y^{\prime}$ and $Y\mathrel{S}Y^{\prime}$ .

It is clear that $|decide_{Y^{\prime}}(\Pi)|\leq 2\leq k$ by definition. Suppose $Y$ and $Y^{\prime}$ satisfies both (1) and (2). Then for all $a\in\Pi$ , $input_{Y}(a)=input_{Y^{\prime}}(a)$ and there exists $a^{\prime}\in\Pi$ such that $(a^{\prime},decide_{Y^{\prime}}(a))\in carrier(view_{Y}(a))$ . Because $carrier(view_{Y}(a))=carrier(view_{a}^{r}(I,\gamma_{1},\dots,\gamma_{r}))\subseteq I$ by Lemma 3.12, $(a^{\prime},decide_{Y^{\prime}}(a))\in I$ , where $I=\{(a,input_{Y}(a))\mid a\in\Pi\}=\{(a,input_{Y^{\prime}}(a))\mid a\in\Pi\}$ . Hence, we have $I\models\bigwedge_{a\in\Pi}\bigvee_{b\in\Pi}\mathtt{input}_{b}^{decide_{Y^{\prime}}(a)}$ . These imply $Y^{\prime}\in\mathcal{F}({\mathcal{I}[\mathcal{SA}_{k}]})$ if $Y$ and $Y^{\prime}$ satisfies both (1) and (2). Therefore, $Y^{\prime}\in\mathcal{F}({\mathcal{I}[\mathcal{SA}_{2}]})$ holds because $Y$ and $Y^{\prime}$ satisfies the conditions (1) and (2), as shown below.

Since $X\mathrel{S}X^{\prime}$ , $X\sim_{a_{0}}Y$ and $input_{Y^{\prime}}(a)=input_{Y}(a)$ for all $a\in\Pi$ , $input_{X^{\prime}}(a_{0})=input_{X}(a_{0})=input_{Y}(a_{0})=input_{Y^{\prime}}(a_{0})$ . Recall that $decide_{Y^{\prime}}(a_{0})=decide_{X^{\prime}}(a_{0})$ by definition. Thus, we have $(a_{0},input_{X^{\prime}}(a_{0}),decide_{X^{\prime}}(a_{0}))=(a_{0},input_{Y^{\prime}}(a_{0}),decide_{Y^{\prime}}(a_{0}))\in X^{\prime}\cap Y^{\prime}$ . Hence, $X^{\prime}\sim_{a_{0}}Y^{\prime}$ holds.

Since $input_{Y^{\prime}}(a)=input_{Y}(a)$ for all $a\in\Pi$ by definition, $Y$ and $Y^{\prime}$ satisfies (1). We prove $Y$ and $Y^{\prime}$ satisfies (2). For the case $a\neq a_{0}$ , we have $(a_{1},decide_{Y^{\prime}}(a))=(a_{1},input_{Y}(a_{1}))\in carrier(view_{Y}(a))$ by Lemma 3.12. For the other case $a=a_{0}$ , since $decide_{Y^{\prime}}(a_{0})=decide_{X^{\prime}}(a_{0})$ , $X\mathrel{S}X^{\prime}$ and $X\sim_{a_{0}}Y$ , there exists $a^{\prime}_{0}\in\Pi$ such that $(a^{\prime}_{0},decide_{Y^{\prime}}(a_{0}))=(a^{\prime}_{0},decide_{X^{\prime}}(a_{0}))\in carrier(view_{X}(a_{0}))=carrier(view_{Y}(a_{0}))$ . Consequently, we have for all $a\in\Pi$ , there exists $a^{\prime}\in\Pi$ such that $(a^{\prime},decide_{Y^{\prime}}(a))\in carrier(view_{Y}(a))$ , i.e. $Y$ and $Y^{\prime}$ satisfies (2), and $Y\mathrel{S}Y^{\prime}$ . Therefore, (Forth) is satisfied.

To show the totality, suppose $X$ is a facet of $\mathcal{F}({\mathcal{I}[\mathcal{SA}_{k}]})$ . Let $I=\{(a,input(a))\mid a\in\Pi\}$ be a facet of the input model $\mathcal{I}$ and $\gamma_{1},\dots,\gamma_{r}$ be ordered partitions such that $X=I[\gamma_{1},\dots,\gamma_{r}]$ , where $\gamma_{1}=(C_{1},\dots,C_{j})$ . Fix an agent $a_{1}\in C_{1}$ . We define a facet $X^{\prime}\in\mathcal{I}[\mathcal{SA}_{k}]$ as $X^{\prime}=\{(a,input(a),input(a_{1}))\mid a\in\Pi\}$ . By Lemma 3.12, $(a_{1},input(a_{1}))\in\{(p,input(p))\mid p\in C_{1}\}\subseteq carrier(view_{a}^{r}(I,\gamma_{1},\dots,\gamma_{r}))$ for all $a\in\Pi$ . Thus, we have $X\mathrel{S}X^{\prime}$ . This implies that $S$ is a total simulation. ∎

We have shown the non-existence of logical obstruction in $\mathcal{L}_{K}^{+}$ for cases where $k\geq 2$ . For the case $k=1$ , [DBLP:journals/iandc/GoubaultLR21] have shown that there exists a logical obstruction to the solvability in $\mathcal{L}_{CK}^{+}$ , an epistemic logic language of positive formulas that extends $\mathcal{L}_{K}^{+}$ with common knowledge operator. It is not difficult to see that $k$ -set agreement task ( $k\geq 2$ ) admits no logical obstruction in $\mathcal{L}_{CK}^{+}$ because the simulation technique presented in this section is compatible with common knowledge operators.

4 Non-existence of logical obstructions with distributed knowledge operator

In this section, we consider a language of epistemic logic $\mathcal{L}_{D}$ , which is an extension of $\mathcal{L}_{K}$ with distributed operator $\mathrm{D}_{A}\varphi$ , and its sublanguage $\mathcal{L}_{D}^{+}$ of positive formulas:

	$\displaystyle\mathcal{L}_{D}:\quad\varphi$	$\displaystyle::=p\mid\lnot\varphi\mid(\varphi\land\varphi)\mid\mathrm{D}_{A}\varphi$
	$\displaystyle\mathcal{L}_{D}^{+}:\quad\varphi$	$\displaystyle::=p\mid\lnot p\mid(\varphi\lor\varphi)\mid(\varphi\land\varphi)\mid\mathrm{D}_{A}\varphi$

where $p\in\mathsf{At}$ is an atomic proposition and $A\subseteq\Pi$ is a set of agents.

Given a formula $\varphi\in\mathcal{L}_{D}$ and a facet $X\in\mathcal{F}({M})$ of a simplicial model $M$ , we define the truth of $\varphi$ at $X$ , written $M,X\models\varphi$ , as below by induction on $\varphi$ .

	$\displaystyle M,X\models p$	$\displaystyle\text{if $p\in l(X)$}.$
	$\displaystyle M,X\models\lnot\varphi$	$\displaystyle\text{if $M,X\not\models\varphi$}.$
	$\displaystyle M,X\models\varphi_{1}\land\varphi_{2}$	$\displaystyle\text{if $M,X\models\varphi_{1}$ and $M,X\models\varphi_{2}$}.$
	$\displaystyle M,X\models\mathrm{D}_{A}\varphi$	$\displaystyle\text{if for all Y $\in\mathcal{F}({M})$, $A\subseteq\chi(X\cap Y)\implies M,Y\models\varphi$}.$

Notice that $\mathrm{K}_{a}\varphi$ is a special case of $\mathrm{D}_{A}\varphi$ where $A$ is a singleton set $\{a\}$ .

4.1 Knowledge gain and a logical obstruction to the solvability of $\mathcal{SA}_{k}$ by $\mathcal{IS}^{1}$ with distributed knowledge

The knowledge gain theorem holds, even the additional modality of distributed knowledge.

Theorem 4.1 (Knowledge gain with distributed knowledge operator).

Suppose $f\colon M\to M^{\prime}$ be a morphism between simplicial models. Then, for any facet $X\in\mathcal{F}({M})$ and positive formula $\varphi\in\mathcal{L}_{D}^{+}$ , $M^{\prime},f(X)\models\varphi$ implies $M,X\models\varphi$ .

Corollary 4.2.

If there exists a morphism $f\colon M\to M^{\prime}$ , for any positive formula $\varphi\in\mathcal{L}_{D}^{+}$ , $M^{\prime}\models\varphi$ implies $M\models\varphi$ .

Corollary 4.3.

Let $\mathcal{I}$ be an input simplicial model, $T$ be a task and $A$ be an action model. If there exists a positive formula $\varphi\in\mathcal{L}_{D}^{+}$ such that $\mathcal{I}[T]\models\varphi$ and $\mathcal{I}[A]\not\models\varphi$ , the task $T$ is not solvable by $A$ .

Thus, we also call a positive formula $\varphi$ such as the one in the above corollary, a logical obstruction to the solvability of $T$ by $A$ , or a logical obstruction, when $T$ and $A$ are clear from the context.

The following theorem on the unsolvability of the set agreement task by a single round immediate snapshot is due to Nishida [Nishida:Msc20], where he provided a concrete logical obstruction in the language $\mathcal{L}_{D}^{+}$ . It has also been shown that the same formula applies to show the unsolvability of the set agreement task by a single round atomic snapshot protocol [DBLP:journals/corr/abs-2011-13630].

Theorem 4.4.

For any $k<|\Pi|$ , there exists a logical obstruction to the solvability of $\mathcal{SA}_{k}$ by $\mathcal{IS}^{1}$ in $\mathcal{L}_{D}^{+}$ .

4.2 Knowledge gain via D-simulation

In the following, we refine the definition of simulation so that Theorem 3.6 is valid if positive formulas have distributed knowledge operator.

Definition 4.5 (D-simulation).

A binary relation over facets of simplicial models $R\subseteq\mathcal{F}({M})\times\mathcal{F}({M^{\prime}})$ is called a D-simulation of $M$ by $M^{\prime}$ , if the following conditions hold.

(Atom): For all $X\in\mathcal{F}({M})$ and $X^{\prime}\in\mathcal{F}({M^{\prime}})$ , $X\mathrel{R}X^{\prime}$ implies $l(X)=l^{\prime}(X^{\prime})$ .
(D-Forth): For all $X,Y\in\mathcal{F}({M})$ and $X^{\prime}\in\mathcal{F}({M^{\prime}})$ , if $X\mathrel{R}X^{\prime}$ holds, there exists $Y^{\prime}\in\mathcal{F}({M^{\prime}})$ such that $Y\mathrel{R}Y^{\prime}$ and $\chi(X\cap Y)\subseteq\chi^{\prime}(X^{\prime}\cap Y^{\prime})$ .

A D-simulation $S$ is called total if for all $X\in\mathcal{F}({M})$ , there exists $X^{\prime}\in\mathcal{F}({M^{\prime}})$ such that $X\mathrel{S}X^{\prime}$ . For a facet $X\in\mathcal{F}({M})$ , we say that $S$ is not total at $X$ if there is no $X^{\prime}\in\mathcal{F}({M^{\prime}})$ such that $X\mathrel{S}X^{\prime}$ . We occasionally write K-simulation to refer to the simulation defined in Definition 3.4, and as well (K-Forth) to refer to (Forth).

Proposition 4.6.

Suppose $f\colon M\to M^{\prime}$ is a morphism between simplicial models. Then, a binary relation $graph(f)=\{(X,f(X))\mid X\in\mathcal{F}({M})\}\subseteq\mathcal{F}({M})\times\mathcal{F}({M^{\prime}})$ is a total D-simulation.

Proof.

(Atom): By the definition of morphism, $f$ preserves labeling, i.e. $l(X)=l^{\prime}(f(X))$ .

(D-Forth): Let $X,Y\in\mathcal{F}({M})$ be facets. It suffices to show that $\chi(X\cap Y)\subseteq\chi^{\prime}(f(X)\cap f(Y))$ . Suppose $a\in\chi(X\cap Y)$ . Then there exists an $a$ -colored vertex $v\in X\cap Y$ . Since $f$ is a color-preserving map, we have $f(v)\in f(X)\cap f(Y)$ and $\chi^{\prime}(f(v))=\chi(v)=a$ . This implies $a\in\chi^{\prime}(f(X)\cap f(Y))$ .

It is clear that $graph(f)$ is total. ∎

Theorem 4.7.

Suppose $S\subseteq\mathcal{F}({M})\times\mathcal{F}({M^{\prime}})$ is a D-simulation. Then, for any facets $(X,X^{\prime})\in S$ and positive formula $\varphi\in\mathcal{L}_{D}^{+}$ , $M^{\prime},X^{\prime}\models\varphi$ implies $M,X\models\varphi$ .

Proof.

This theorem is similarly proved as in Theorem 3.6 by induction on $\varphi$ . Let us only show the case of distributed knowledge operator.

Supoose $\varphi=\mathrm{D}_{A}\psi$ . Assuming $M^{\prime},X^{\prime}\models\mathrm{D}_{A}\psi$ , we show that $M,Y\models\psi$ holds for any $Y\in\mathcal{F}({M})$ such that $A\subseteq\chi(X\cap Y)$ . By the condition (D-Forth), there exists $Y^{\prime}\in\mathcal{F}({M^{\prime}})$ such that $Y\mathrel{S}Y^{\prime}$ and $A\subseteq\chi(X\cap Y)\subseteq\chi^{\prime}(X^{\prime}\cap Y^{\prime})$ . This implies $M^{\prime},Y^{\prime}\models\psi$ and also $M,Y\models\psi$ by induction hypothesis. Therefore, $M,X\models\mathrm{D}_{A}\psi$ . ∎

Corollary 4.8.

If there exists a total D-simulation of $M$ by $M^{\prime}$ , for any positive formula $\varphi\in\mathcal{L}_{D}^{+}$ , $M^{\prime}\models\varphi$ implies $M\models\varphi$ .

4.3 Non-existence of logical obstructions to the solvability of $\mathcal{IS}^{2}$ by $\mathcal{SA}_{2}$

Using a D-simulation, let us argue the unsolvability of the set agreement task for a particular case $\Pi=\{0,1,2\}$ . We leave the general case as an open problem because D-simulation for higher dimensional model would be much complicated and hard to construct.

The following binary relation $R^{p,q}$ defines a set of pairs of two vertices that we will constrain their decision values. Although it was sufficient to constrain each vertex individually when we constructed a K-simulation in Theorem 3.13, we need to consider constraints for each tuple of vertices in order to construct D-simulation.

Definition 4.9.

Let $V$ be the set of vertices and $S$ be the set of simplices for $\mathcal{I}[\mathcal{IS}^{2}]$ . For a vertex $x=(p,i_{p},v_{p})\in V$ and an agent $q\in\Pi$ , in abuse of notation, we write $q\in view(x)$ if there exists $i_{q}\in V^{in}$ such that $(q,i_{q})\in carrier(v_{p})$ and $q\notin view(x)$ otherwise. Given $p,q\in\Pi$ $(p<q)$ , We define a binary relation $R_{n}^{p,q}\subseteq V\times V$ for $n\in\mathbb{N}$ , by induction on $n$ as follows.

•

$x\mathrel{R_{0}^{p,q}}y$ if $\{x,y\}$ is a 1-simplex of $\mathcal{I}[\mathcal{IS}^{2}]$ and it holds either $p\notin view(x)$ or $q\notin view(y)$ .
•

$x\mathrel{R_{n+1}^{p,q}}y$ if either $x\mathrel{R_{n}^{p,q}}y$ or there exists $z\in V$ such that $x\mathrel{R_{n}^{p,q}}z$ , $z\mathrel{R_{n}^{p,q}}y$ and $\{x,y,z\}$ is a 2-simplex.

We further define a binary relation $R^{p,q}\subseteq V\times V$ as $R^{p,q}=\bigcup_{n\in\mathbb{N}}R_{n}^{p,q}\setminus R_{0}^{p.q}$ .

Determining Existence of Logical Obstructions to the Distributed Task Solvability ††thanks: This article is a revised version of aurthor’s Master’s thesis [Hoshino:Msc22].

Abstract

1 Introduction

2 Preliminaries

2.1 Simplicial models

Definition 2.1 (Chromatic simplicial complex).

Definition 2.2 (Simplicial model).

Definition 2.3 (Morphism between simplicial models).

Definition 2.4 (Input simplicial model).

2.2 Epistemic logic for simplicial models

Definition 2.5 (Epistemic formula).

Definition 2.6.

2.3 Protocols, tasks and solvability with DEL

Definition 2.7 (Simplicial action model and product update).

Definition 2.8 (Task).

Example 2.9 (kk-set agreement task).

Definition 2.10 (Solvability).

3 Non-existence of logical obstructions

3.1 Knowledge gain and logical obstruction

Theorem 3.1 (Knowledge gain [DBLP:journals/iandc/GoubaultLR21]).

Corollary 3.2.

Corollary 3.3.

3.2 Knowledge gain via simulation

Definition 3.4 (Simulation).

Proposition 3.5.

Proof.

Theorem 3.6.

Proof.

Corollary 3.7.

3.3 Non-existence of logical obstructions to the solvability of 𝒮𝒜k\mathcal{SA}_{k} by ℐ𝒮r\mathcal{IS}^{r}

Definition 3.8.

Definition 3.9.

Definition 3.10.

Definition 3.11.

Lemma 3.12.

Proof.

Theorem 3.13.

Proof.

4 Non-existence of logical obstructions with distributed knowledge operator

4.1 Knowledge gain and a logical obstruction to the solvability of 𝒮𝒜k\mathcal{SA}_{k} by ℐ𝒮1\mathcal{IS}^{1} with distributed knowledge

Theorem 4.1 (Knowledge gain with distributed knowledge operator).

Corollary 4.2.

Corollary 4.3.

Theorem 4.4.

4.2 Knowledge gain via D-simulation

Definition 4.5 (D-simulation).

Proposition 4.6.

Proof.

Theorem 4.7.

Proof.

Corollary 4.8.

4.3 Non-existence of logical obstructions to the solvability of ℐ𝒮2\mathcal{IS}^{2} by 𝒮𝒜2\mathcal{SA}_{2}

Definition 4.9.

Determining Existence of Logical Obstructions to the Distributed Task Solvability ^†^†thanks: This article is a revised version of aurthor’s Master’s thesis [Hoshino:Msc22].

Example 2.9 ( $k$ -set agreement task).

3.3 Non-existence of logical obstructions to the solvability of $\mathcal{SA}_{k}$ by $\mathcal{IS}^{r}$

4.1 Knowledge gain and a logical obstruction to the solvability of $\mathcal{SA}_{k}$ by $\mathcal{IS}^{1}$ with distributed knowledge

4.3 Non-existence of logical obstructions to the solvability of $\mathcal{IS}^{2}$ by $\mathcal{SA}_{2}$