Abstract
The logical method proposed by Goubault, Ledent, and Rajsbaum provides a means of demonstrating the unsolvability of distributed tasks within the epistemic logic framework. To show that a task is unsolvable, we need to find a logical obstruction, which is an epistemic logic formula describing the reason for the unsolvability, or more precisely, the incompatibility between the task, which is a model of what is to be solved, and the protocol, which is a model of what the distributed system can compute. To date, only a few concrete instances of logical obstructions have been devised. In particular, existing proposals of logical obstruction to the k-set agreement task are unsatisfactory because they work only for the case \(k=1\) or the protocol is restricted to single-round execution. This is because the unsolvability of the k-set agreement task is tied with the higher-dimensional property of the corresponding combinatorial topological model, while the language of epistemic logic has a limited ability to express it. This study proposes the use of an epistemic \(\mu \)-calculus variant, which extends epistemic logic with distributed knowledge modalities and propositional greatest fixpoints. With these extensions, we can define an epistemic formula whose epistemic content contradicts a property regarding the higher-dimensional connectivity, which is indicated in the proof of Sperner’s lemma. This formula thus works as a logical obstruction, showing that the k-set agreement task is unsolvable by the multiple-round immediate snapshot protocol. Further, we show that the same formula works as a logical obstruction for the k-concurrency, which is a protocol of a limited degree of concurrency.
This is a preview of subscription content, log in via an institution to check access.
Similar content being viewed by others
Notes
In this paper, we use “process” as a synonym for “agent” in multi-agent epistemic logic.
More precisely, this is a Kripke model for multi-agent epistemic logic with axiom system \(\textbf{S5}_n\), where each indistinguishability relation \(\sim ^{}_{a}\) is an equivalence relation (Fagin et al. 1995).
The logic in this study does not include the least fixpoint \(\mu Z.\varphi \). Its logical equivalent \(\lnot \nu Z.\lnot \varphi \) is not included either, as it is not a positive formula.
The distributed knowledge operator with a singleton set of processes \(\mathop {\textrm{D}_{\{a\}}} \varphi \) is known as the knowledge operator \(\mathop {\textrm{K}_{a}} \varphi \), which is omitted from the language of the logic in this study.
We abbreviate a facet of \(\mathcal {I}[\mathcal{I}\mathcal{S}^{}]\) as \(X\mathop {\rtimes }\gamma \), where we omit the duplicate of X in the formal notation \(X \times (X\mathop {\rtimes }\gamma )\). The redundancy in the formal notation is due to the definition of product update, where the action model \(\mathcal{I}\mathcal{S}{}\) must be defined relative to the input complex \(\mathcal {I}\), in order for a precondition to relate each action in \(\mathcal{I}\mathcal{S}{}\) (i.e., a facet of the standard chromatic subdivision) with an appropriate set of facets in \(\mathcal {I}\).
In topological arguments, some of the invariant properties such as \(\textrm{OFUN}\), \(\textrm{VALID}\), and \(\textrm{KNOW}\) are often left implicit, because they are readily obtained from the simplicial complex model. In contrast, we must make them explicit to promote logical reasoning, at every step of unfolding of the fixpoint.
Here we define the contention set differently from the original one (Gafni et al. 2016) for clarity, albeit the two definitions are equivalent.
References
Alistarh, D., Aspnes, J., Ellen, F., et al.: Why extension-based proofs fail. SIAM J. Comput. 52(4), 913–944 (2023)
Baltag, A., Moss, L.S., Solecki, S.: The logic of public announcements, common knowledge, and private suspicions. In: Arló-Costa, H., Hendricks, V.F., van Benthem, J. (eds.) Readings in Formal Epistemology: Sourcebook. Springer, chap 39, pp. 773–812 (2016)
Baltag, A., Smets, S.: Learning what others know. In: LPAR-23: 23rd International Conference on Logic for Programming, Artificial Intelligence and Reasoning, pp. 90–119 (2020)
Borowsky, E., Gafni, E.: Generalized FLP impossibility result for t-resilient asynchronous computations. In: Proceedings of the 25th Annual ACM Symposium on Theory of Computing, STOC. ACM, pp. 91–100 (1993a)
Borowsky, E., Gafni, E.: Immediate atomic snapshots and fast renaming (extended abstract). In: Proceedings of the 12th Annual ACM Symposium on Principles of Distributed Computing. ACM, pp. 41–51 (1993b)
Bradfield, J.C., Stirling, C.: Modal mu-calculi. In: Blackburn, P., van Benthem, J.F.A.K., Wolter, F. (eds.) Handbook of Modal Logic, Studies in logic and practical reasoning, vol. 3, pp. 721–756. North-Holland (2007)
Castañeda, A., Fraigniaud, P., Paz, A., et al.: A topological perspective on distributed network algorithms. Theor. Comput. Sci. 849, 121–137 (2021)
de Longueville, M.: A Course in Topological Combinatorics. Universitext, Springer (2013)
Fagin, R., Halpern, J.Y., Moses, Y., et al.: Reasoning About Knowledge. MIT Press, Cambridge (1995)
Fischer, M.J., Lynch, N.A., Paterson, M.: Impossibility of distributed consensus with one faulty process. J. ACM 32(2), 374–382 (1985)
Gafni, E., He, Y., Kuznetsov, P., et al.: Read-write memory and \(k\)-set consensus as an affine task. In: 20th International Conference on Principles of Distributed Systems (OPODIS 2016), pp. 6:1–6:17 (2016)
Goubault, É., Lazic, M., Ledent, J., et al.: Wait-free solvability of equality negation tasks. In: 33rd International Symposium on Distributed Computing, DISC 2019, LIPIcs, vol 146. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, pp 21:1–21:16 (2019)
Goubault, É., Ledent, J., Rajsbaum, S.: A simplicial complex model for dynamic epistemic logic to study distributed task computability. Information and Computation 278:104,597. An earlier version appeared in Proceedings of of 9th International Symposium on Games, Automata, Logics, and Formal Verification, GandALF 2018 (2021)
Guerraoui, R., Kuznetsov, P.: Algorithms for Concurrent Systems. EPFL Press. (2018)
Halpern, J.Y., Moses, Y.: Knowledge and common knowledge in a distributed environment. J. ACM 37(3), 549–587 (1990)
Halpern, J.Y., Vardi, M.Y.: The complexity of reasoning about knowledge and time. I. Lower bounds. J. Comput. Syst. Sci. 38(1), 195–237 (1989)
Henle, M.: A Combinatorial Introduction to Topology. Dover (1983)
Herlihy, M., Kozlov, D.N., Rajsbaum, S.: Distributed Computing Through Combinatorial Topology. Morgan Kaufmann (2013)
Herlihy, M., Rajsbaum, S.: Set consensus using arbitrary objects (preliminary version). In: Proceedings of the 13th Annual ACM Symposium on Principles of Distributed Computing. ACM, pp. 324–333 (1994)
Herlihy, M., Rajsbaum, S.: Algebraic spans. Math. Struct. Comput. Sci. 10(4), 549–573 (2000)
Herlihy, M., Shavit, N.: The topological structure of asynchronous computability. J. ACM 46(6), 858–923 (1999)
Hintikka, J.: Knowledge and belief: An introduction to the logic of the two notions. Cornell University Press, Ithaca (1962)
Hoshino, S.: Determining existence of logical obstructions to the distributed task solvability. (2022). arXiv:2203.05153
Kozen, D.: Results on the propositional \(\mu \)-calculus. Theoret. Comput. Sci. 27(3), 333–354 (1983)
Kozlov, D.: Combinatorial Algebraic Topology. Springer, Berlin (2008)
Kozlov, D.N.: Chromatic subdivision of a simplicial complex. Homol. Homotopy Appl. 14(2), 197–209 (2012)
Nishida, Y.: Impossibility of \(k\)-set agreement via dynamic epistemic logic (in Japanese). In: Algebraic system, Logic, Language and Related Areas in Computer Sciences II, pp. 96–105, (2020) http://hdl.handle.net/2433/265621
Nishimura, S.: Schlegel diagram and optimizable immediate snapshot protocol. In: 21st International Conference on Principles of Distributed Systems, OPODIS 2017, pp. 22:1–22:16 (2017)
Saraph, V., Herlihy, M., Gafni, E.: Asynchronous computability theorems for t-resilient systems. In: Distributed Computing, 30th International Symposium, DISC 2016, pp. 428–441 (2016)
Shilov, N.V., Garanina, N.O.: Model checking knowledge and fixpoints. Fixed Points Comput. Sci. FICS 2002, 25–39 (2002)
Sperner, E.: Neuer beweis für die invarianz der dimensionszahl und des gebietes. Abhandlungen Hamburg 6, 265–272 (1928)
van Ditmarsch, H., Goubault, E., Ledent, J., et al.: Knowledge and simplicial complexes. arXiv:2002.08863 (2020)
van Ditmarsch, H., van der Hoek, W., Kooi, B.: Dynamic Epistemic Logic, Synthese Library, vol. 337. Springer, Berlin (2008)
van Ditmarsch, H., Goubault, É., Lazic, M., et al.: A dynamic epistemic logic analysis of equality negation and other epistemic covering tasks. J. Logical Algebraic Methods Program. 121(100), 662 (2021)
Velázquez, D.A., Castañeda, A., Rosenblueth, D.A.: Communication pattern models: An extension of action models for dynamic-network distributed systems. Proceedings Eighteenth Conference on Theoretical Aspects of Rationality and Knowledge, TARK 2021, 307–321 (2021)
Yagi, K., Nishimura, S.: Logical obstruction to set agreement tasks for superset-closed adversaries. (2020). arXiv:2011.13630
Acknowledgements
The author would like to thank the anonymous reviewers for their careful reading of the manuscript and their comments that were helpful for improving the paper. The author is supported by JSPS KAKENHI Grant Number 20K11678.
Author information
Authors and Affiliations
Corresponding author
Ethics declarations
Conflict of interest
The author has no competing interests to declare that are relevant to the content of this article.
Additional information
Publisher's Note
Springer Nature remains neutral with regard to jurisdictional claims in published maps and institutional affiliations.
Rights and permissions
Springer Nature or its licensor (e.g. a society or other partner) holds exclusive rights to this article under a publishing agreement with the author(s) or other rightsholder(s); author self-archiving of the accepted manuscript version of this article is solely governed by the terms of such publishing agreement and applicable law.
About this article
Cite this article
Nishimura, S. Defining logical obstruction with fixpoints in epistemic logic. J Appl. and Comput. Topology 8, 941–970 (2024). https://doi.org/10.1007/s41468-023-00151-8
Received:
Revised:
Accepted:
Published:
Issue Date:
DOI: https://doi.org/10.1007/s41468-023-00151-8