Proving Unsolvability of Set Agreement Task with Epistemic mu-Calculus
share
This paper shows, in the framework of the logical method,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 μ-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 μ-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.
READ FULL TEXT