2022/05/13 by Susumu Nishimura, Nishimura, Susumu
Computer Science · Social Sciences · #Access Control and Trust #C.2.4 #Distributed #Distributed systems and fault tolerance #F.3.1 #FOS: Computer and information sciences #Logic in Computer Science (cs.LO) #Logic, Reasoning, and Knowledge #Parallel #and Cluster Computing (cs.DC)
paper · pdf · doi:10.48550/arxiv.2205.06452
openalex publication_date 2022/05/13 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
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.