Partial Product Updates for Agents of Detectable Failure and Logical Obstruction to Task Solvability

In the topological method [6], distributed systems are modeled by simplicial complexes. A global state of a distributed system is modeled by a simplex, i.e., a nonempty set of vertexes, where each vertex represents the local state of a particular agent. The nonderteministic set of global states of a distributed system is modeled by a simplicial complex, a set of simplexes that is closed under set inclusion. The topological model uses the so called chromatic simplicial complex, whose vertexes are properly ‘colored’ with agent ids.

For brevity, we often write complexes (resp., simplexes) to mean chromatic simplicial complexes (resp., chromatic simplexes).

A simplex $X$ is of dimension $d$, if $\lvert X\rvert=d+1$. The dimension of a complex $\mathcal{C}$ is the maximum dimension of the simplexes contained in $\mathcal{C}$. A simplex $X$ is called a facet of $\mathcal{C}$, if $X$ is a maximal simplex, i.e., $\mathcal{C}$ contains no facet that is properly larger than $X$. We write $\mathcal{F}(\mathcal{C})$ for the set of facets of $\mathcal{C}$. A complex is called pure (of dimension $n-1$) if all facets are of the same dimension $n-1$; otherwise, the complex is called impure. An impure complex contains a facet of dimension less than $n-1$. Such a facet represents a global state of the distributed system where some agents are ‘dead’ due to crash.

Given complexes $\mathcal{C}=\langle V,S,\chi\rangle$ and $\mathcal{C}^{\prime}=\langle V^{\prime},S^{\prime},\chi^{\prime}\rangle$, a simplicial map $\delta:\mathcal{C}\to\mathcal{C}^{\prime}$ is a color-preserving map from $V$ to $V^{\prime}$ such that:

• •

  $f(X)\in S^{\prime}$ for every $X\in S$;

• •

  $\chi^{\prime}(f(v))=\chi(v)$ for every $v\in V$.

We are concerned with the analysis of distributed computability with epistemic logic [1], a propositional logic augmented with a knowledge modality.

Following [4], below we define the semantics of epistemic logic in a partial epistemic model.

When $w\sim_{a}w^{\prime}$ holds in a partial epistemic model, it means that agent $a$ is alive in both of the possible worlds $w$ and $w^{\prime}$ and it cannot distinguish between these worlds. Particularly, $w\not\sim_{a}w$ implies that an agent $a$ is dead in a possible world $w$. We write $\overline{w}$ for the set of agents that is alive in $w$, i.e., $\overline{w}=\{a\in\mathsf{Ag}\mid w\sim_{a}w\}$. For $A\subseteq\mathsf{Ag}$, we also write $w\sim_{A}w^{\prime}$ to mean $w\sim_{a}w^{\prime}$ for every $a\in A$.

Partial epistemic models generalize the usual epistemic models: Indistinguishability relations are given by equivalence relations instead of PERs, which means that every agent is alive in epistemic models.

Partial epistemic models form a category whose objects are partial epistemic models and morphisms are the functions defined as follows. A morphism $f$ from $\mathcal{M}=\langle W,\sim,L\rangle$ to $\mathcal{M}^{\prime}=\langle W^{\prime},\sim^{\prime},L^{\prime}\rangle$ is a function $f:W\to 2^{W^{\prime}}$ satisfying the following properties:

• •

  (Preservation of $\sim$) For all $a\in\mathsf{Ag}$ and $w,w^{\prime}\in M$, $w\sim_{a}w^{\prime}$ implies $u\sim_{a}^{\prime}u^{\prime}$ for every $u\in f(w)$ and $u^{\prime}\in f(w^{\prime})$.

• •

  (Saturation) For all $w\in W$, there exists $w^{\prime}\in f(w)$ such that $f(w)=\mathsf{sat}_{\overline{w}}(w^{\prime})$, where $\mathsf{sat}_{U}(v)=\{w\in W\mid v\sim_{U}w\}$ is a saturation, the set of all possible worlds that cannot be distinguished from $w$ by any agent $a\in U$.

• •

  (Preservation of atomic formulas) For all $w\in M$ and $w^{\prime}\in f(w)$, $L(w)\cap\mathsf{At}_{\overline{w}}=L^{\prime}(w)\cap\mathsf{At}_{\overline{w}}$.

In order to show unsolvability results in this paper, we will use the knowledge gain property, which states that the amount of knowledge is never increased along a morphism from one Kripke model to another. For partial epistemic models, the knowledge gain property holds for any guarded positive formula [4].

From the topological structure of a given (not necessarily pure) simplicial complex, we can derive simplicial models [4].

The set $\ell(X)$ of atomic propositions determines the local states of agents in a given global state represented by $X$.

From a simplicial model $\mathcal{C}=\langle V,S,\chi,\ell\rangle$, we can derive a partial epistemic model $\langle{\mathcal{F}(\mathcal{C}),\sim,L}\rangle$ such that

• •

  The set of possible worlds is $\mathcal{F}(\mathcal{C})$, the set of facets of the complex $\mathcal{C}$;

• •

  The indistinguishability relation is defined by $X\sim_{a}Y$ if and only if $a\in\chi(X\cap Y)$. That means, the facets $X$ and $Y$ sharing a common vertex of color $a$ are indistinguishable by the agent $a$;

• •

  The labeling $L$ on possible worlds is defined by $L(X)=\ell(X)$ for each $X\in\mathcal{F}(\mathcal{C})$.

The partial epistemic model derived from a simplicial model in this way is a proper Kripke model. A Kripke model $\mathcal{M}=\langle W,\sim,L\rangle$ is called proper if $w\neq w^{\prime}$ implies $\exists a\in\mathsf{Ag}.~{}w\not\sim_{a}w^{\prime}$ for all $w,w^{\prime}\in W$. It has been shown that the category $\mathcal{PM}$ of proper partial epistemic models is equivalent to the category $\mathcal{SM}$ of simplicial models [4], where a morphism $f$ from $\mathcal{C}=\langle V,S,\chi,\ell\rangle$ to $\mathcal{C}^{\prime}=\langle V^{\prime},S^{\prime},\chi^{\prime},\ell^{\prime}\rangle$ in $\mathcal{SM}$ is a simplicial map $f:\mathcal{C}\to\mathcal{C}^{\prime}$ satisfying $\ell(X)\cap\mathsf{At}_{\chi(X)}=\ell^{\prime}(Y)\cap\mathsf{At}_{\chi(X)}$ for every $X\in\mathcal{F}(\mathcal{C})$ and $Y\in\mathcal{F}(\mathcal{C}^{\prime})$ such that $f(X)\subseteq Y$.

Due to this equivalence, in the sequel we will occasionally confuse simplicial models with proper partial epistemic models. We regard facets of a complex $\mathcal{C}$, say $X,Y\in\mathcal{F}(\mathcal{C})$, as possible worlds of the corresponding partial epistemic model and argue the indistinguishability by the property of the facets. For example, $X\sim_{a}Y$ in a partial equivalence model is interpreted as $a\in\chi(X\cap Y)$; The notation $\overline{X}$, which denotes the set of live agents in a facet $X$ of a simplicial model, is given by $\overline{X}=\chi(X)$.

The precondition $\mathsf{pre}(t)$ describes the condition for the action $t$ to occur.

The original product update ${\mathcal{M}}\left[{\mathbf{A}}\right]$ [3] is an instance of the partial product update ${\mathcal{M}}\left\{{\mathbf{A}}\right\}$. When the indistinguishability relations of both $\mathcal{M}$ and $\mathbf{A}$ are equivalence relations, rather than partial equivalence relations, and $\mathcal{M}$ is proper, every possible world $(\left[{X}\right]_{t}^{\mathsf{pre}},t)$ in ${\mathcal{M}}\left\{{\mathbf{A}}\right\}$ can be identified with $(X,t)$ in ${\mathcal{M}}\left[{\mathbf{A}}\right]$. This is because $\left[{X}\right]_{t}^{\mathsf{pre}}=\{X\}$, since $\overline{t}=\mathsf{Ag}$ for all $t\in\mathbf{A}$ and $\mathcal{M}$ is proper.

In the sequel, we assume that the set $\mathsf{At}$ of atomic propositions is given by $\mathsf{At}=\bigcup_{a\in\mathsf{Ag}}\mathsf{At}_{a}$ with $\mathsf{At}_{a}=\{\mathsf{input}_{a}^{v}\mid v\in\mathsf{Value}\}$ for each $a\in\mathsf{Ag}$, where $\mathsf{Value}$ is the set of possible input values. Without loss of generality, we may assume that the set of input values coincides with the set of agent ids, i.e., $\mathsf{Value}=\mathsf{Ag}=\{0,\cdots,n-1\}$.

The input model for a system with $n$ agents is given as follows.

In the rest of the paper, we write $\mathcal{I}$ to refer to this particular input simplicial model. The underlying simplicial complex $\langle V,S,\chi\rangle$ of $\mathcal{I}$ is a pure complex of dimension $n-1$, where each vertex $(a,v)$ represents a local state of the agent $a$ that has $v$ as the input value. The set of facets in the complex represents all the possible assignments of input values to the agents, and the labeling $\ell$ interprets such assignments by giving the relevant set of atomic propositions for each facet $X$, so that $\mathsf{input}_{a}^{v}\in\ell(X)$ if and only if $(a,v)\in X$.

For example, Figure 3 illustrates the underlying complex of the input simplicial model $\mathcal{I}$ for $2$ agents (i.e, $\mathsf{Ag}=\{0,1\}$). In the figure, we write $X_{ij}$ to stand for a facet $\{(0,i),(1,j)\}$ of $\mathcal{I}$. The labeling is determined by $\ell(X_{ij})=\{\mathsf{input}_{0}^{i},\mathsf{input}_{1}^{j}\}$.

Now we define task solvability, using partial product update.

Schematically, this definition of solvability can be presented by the following diagram-like picture:

where $\pi_{1}$ is the first projection.

Suppose a morphism $\delta_{\mathrm{krip}}$ associates $([X_{p}]_{p}^{\mathrm{pre}},p)\in\mathcal{I}\{\mathbf{P}\}$ with $([X_{t}]_{t}^{\mathrm{pre}},t)\in\mathcal{I}\{\mathbf{T}\}$. Then, in order for this association to be admissible, it must respect the inclusion of (3.1), meaning that, when $\delta_{\mathrm{krip}}$ decides an output $t$ from an intermediate output $p$ by the protocol, every input contained in $[X_{p}]_{p}^{\mathrm{pre}}$, i.e., the set of inputs from which the protocol may produce the output $p$, must be an input contained in $[X_{t}]_{t}^{\mathrm{pre}}$, i.e., the set of inputs that admit $t$ as the output of the task.

This generalizes the original definition of task solvability given in [3], which makes use of (non-partial) product updates. The original definition is given by the following commutative diagram, which is obtained by replacing the models by the product update models, written $\mathcal{I}[\mathbf{P}]$ and $\mathcal{I}[\mathbf{T}]$, and the inclusion in (3.1) by equality $=$.

This definition of the task solvability using product update models is equivalent to the topological definition using simplicial complexes [3]. We can also establish the same equivalence for partial product update models, in the following sense: Suppose we are given a pair of functions over simplicial complexes specifying a task and a protocol. From these specifications we can derive the corresponding partial product update models. Then the task is solvable by the protocol, using partial product update models as defined in Definition 3.5, if and only if the task is solvable in the topological sense, i.e., there exists a simplicial map that mediates between the complexes of the protocol and the task.

The formal argument for this equivalence is deferred to Appendix A. There we also show that the action model $\mathbf{A}$ and the partial product update model ${\mathcal{I}}\left\{{\mathbf{A}}\right\}$ have isomorphic partial epistemic frames, under a suitable condition.

Combining the above task solvability with the knowledge gain property (Proposition 2.5), we obtain a proof method for refuting task solvability by a formula of epistemic logic, called a logical obstruction [3]. A logical obstruction $\varphi$ is a guarded positive formula that is valid in the partial product update model ${\mathcal{I}}\left\{{\mathbf{T}}\right\}$ of a task, but not in the model ${\mathcal{I}}\left\{{\mathbf{P}}\right\}$ of a protocol.

In the synchronous message passing protocol, each agent sends its local private value to all the agents in the system. When an agent crashes, only the messages that have already been sent before the crash are properly delivered to other agents; the rest are not. In a synchronous distributed environment, a correct agent can detect the exact set of crashed agents in the system: An agent is dead (i.e., it has crashed), if no message is received from the agent within a sufficiently long but finite period of time. The protocol complex for the synchronous message passing protocol thus forms an impure simplicial complex [7], in which the vertexes corresponding to dead agents are missing in a facet.

In the impure protocol complex, each different facet arises from each different ‘pattern of failure’ in message delivery, where each specific pattern of failure can be described by a set of orderings of the form $a<b$, which means that the agent $a$ has crashed and failed to send the message to the agent $b$, a correct agent that did not crash. This motivates us to define actions by relevant orderings over the set of agents that satisfy the following properties.

• •

  An agent $a$ is dead after an action (i.e., the agent has crashed during the execution of the protocol) if and only if the corresponding poset of the action admits an ordering $a<b$ for some agent $b$.

• •

  An agent $a$ is alive after an action if and only if the corresponding poset of the action does not admit an ordering $a<b$ for any agent $b$.

• •

  If a poset contains an ordering $a<b$, the poset does not admit an ordering $c<a$ or $b<c$ for any agent $c$. (This is because the ordering $a<b$ indicates that $a$ is a dead agent and $b$ is a correct agent but $c<a$ or $b<c$ implies otherwise.)

This ordering can be formalized as a poset (partially ordered set) $(\mathsf{Ag},\leq)$ of rank at most $1$. A poset is of rank $k$, if the maximum number of elements contained in a totally ordered subset of the poset is $k+1$. [10] As usual, the strict ordering $a<b$ holds if and only if $a\leq b$ and $a\neq b$.

Let us define $\operatorname{lo}(\leq)=\{a\in\mathsf{Ag}\mid\exists b\in\mathsf{Ag},a<b\}$ to denote the set of dead agents. Notice that the reflexive ordering $a\leq a$ is not counted as a failure of message delivery. We are not interested in the success or failure of self-delivery of message: If successful, the agent $a$ trivially receives its own local private value; Otherwise, the agent $a$ is dead and its received messages are lost. In this respect, we indicate a poset by a set $S$ of strict orderings and write $S^{\ast}$ to denote the minimum poset containing $S$, i.e., the reflexive closure of $S$. For example, $\{0<1,2<3\}^{\ast}$ defines a poset ordering $\leq$ over $\mathsf{Ag}$ such that $a\leq b$ holds if and only if either $a=0$ and $b=1$, $a=2$ and $b=3$, or $a=b$. In particular, $\emptyset^{\ast}$ is a discrete poset (of rank $0$) over $\mathsf{Ag}$, in which any pair of distinct agents are incomparable.

Let us first consider the action model for the ‘inputless’ case, where the initial inputs to the agents are insignificant. In this case, the actions for the synchronous message passing protocol is simply modeled by the posets over $\mathsf{Ag}$ of rank at most $1$.

From the inputless action model, we construct a full action model of the synchronous message passing protocol, where the protocol accepts a class of sets of input values. Suppose $\mathcal{I}$ is a simplicial model, whose facets specify the allowed combinations of input values. Then one might expect that an action in the full action model would be expressed by a pair $(X,t)$, where $X$ is a facet of $\mathcal{I}$ and $t$ is an action of the inputless action, but this does not give an appropriate model. Consider the case, say, $t={\{b<a\}}^{*}$, $X\sim_{a}^{\mathcal{I}}Y$, and $X\not\sim_{b}^{\mathcal{I}}Y$. In this case, $(X,t)$ and $(Y,t)$ are different actions but the live agent $a$ should not distinguish them because the action $t$ indicates that the agent $a$ has not received a message from the agent $b$ and therefore it cannot tell which is the original input, either $X$ or $Y$. In other words, the two facets $X$ and $Y$ should be identified.

For this identification of facets w.r.t. an action $t$ of the inputless model, we introduce an equivalence class, written $\left[{X}\right]_{\approx_{t}}$, and define an action in the full action model by a pair $(\left[{X}\right]_{\approx_{t}},t)$.

In words, ${X}\approx_{t}{Y}$ indicates that, for every agent $a$ that is alive in the action $t$, $X$ and $Y$ should have the same input for the agent $b$, if ${b}\not<_{t}{a}$, i.e., the message from $b$ is successfully received by $a$. (Otherwise, the agent $a$ should be aware that $X$ and $Y$ are different facets.) The relation $\approx_{t}$ is an equivalence relation, as we will show below. The relation $\sim^{\mathbf{MP}}_{a}$ defines a PER, where $(\left[{X}\right]_{\approx_{t}},t)\sim^{\mathbf{MP}}_{a}(\left[{Y}\right]_{\approx_{s}},s)$ indicates that the agent $a$ is alive and every agent $b$ that successfully sends a message to $a$ (i.e., ${b}\not<_{t}{a}$) has the same input value that has been assigned in both $X$ and $Y$. The precondition $\mathsf{pre}^{\mathbf{MP}}\bigl{(}(\left[{X}\right]_{\approx_{t}},t)\bigr{)}$ is intended to mean that, for an action $(\left[{X}\right]_{\approx_{t}},t)\in T^{\mathbf{MP}}$, every atomic proposition in $\ell^{\mathcal{I}}(Y)$ is true for some $Y\in\left[{X}\right]_{\approx_{t}}$.