Abstract
Consider a complete communication network on n nodes, each of which is a state machine with s states. In synchronous 2-counting, the nodes receive a common clock pulse and they have to agree on which pulses are “odd” and which are “even”. We require that the solution is self-stabilising (reaching the correct operation from any initial state) and it tolerates f Byzantine failures (nodes that send arbitrary misinformation). Prior algorithms are expensive to implement in hardware: they require a source of random bits or a large number of states s. We use computational techniques to construct very compact deterministic algorithms for the first non-trivial case of f = 1. While no algorithm exists for n < 4, we show that as few as 3 states are sufficient for all values n ≥ 4. We prove that the problem cannot be solved with only 2 states for n = 4, but there is a 2-state solution for all values n ≥ 6.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
Computer-generated proofs, https://github.com/suomela/counting (primary), https://bitbucket.org/suomela/counting (backup)
Ben-Or, M., Dolev, D., Hoch, E.N.: Fast self-stabilizing Byzantine tolerant digital clock synchronization. In: Proc. 27th Symposium on Principles of Distributed Computing (PODC 2008), pp. 385–394. ACM Press, New York (2008)
Biere, A.: PicoSAT essentials. Journal on Satisfiability, Boolean Modeling and Computation 4, 75–97 (2008)
Biere, A.: Lingeling and friends entering the SAT challenge 2012. In: Proceedings of SAT Challenge 2012; Solver and Benchmark Descriptions. Department of Computer Science Series of Publications B, vol. B-2012-2, pp. 33–34. University of Helsinki (2012)
Clarke, E.M., Emerson, E.A.: Design and synthesis of synchronization skeletons using branching time temporal logic. In: Proc. 3rd Workshop on Logic of Programs (LOP 1981). LNCS, vol. 131, pp. 52–71. Springer, Berlin (1982)
Daliot, A., Dolev, D., Parnas, H.: Self-stabilizing pulse synchronization inspired by biological pacemaker networks. In: Huang, S.-T., Herman, T. (eds.) SSS 2003. LNCS, vol. 2704, pp. 32–48. Springer, Heidelberg (2003)
Dolev, D., Hoch, E.N.: On self-stabilizing synchronous actions despite Byzantine attacks. In: Pelc, A. (ed.) DISC 2007. LNCS, vol. 4731, pp. 193–207. Springer, Heidelberg (2007)
Dolev, S.: Self-Stabilization. The MIT Press, Cambridge (2000)
Dolev, S., Welch, J.L.: Self-stabilizing clock synchronization in the presence of Byzantine faults. Journal of the ACM 51(5), 780–799 (2004)
Fischer, M.J., Lynch, N.A.: A lower bound for the time to assure interactive consistency. Information Processing Letters 14(4), 183–186 (1982)
Fuhs, C., Schneider-Kamp, P.: Synthesizing shortest linear straight-line programs over GF(2) using SAT. In: Strichman, O., Szeider, S. (eds.) SAT 2010. LNCS, vol. 6175, pp. 71–84. Springer, Heidelberg (2010)
Järvisalo, M., Kaski, P., Koivisto, M., Korhonen, J.H.: Finding efficient circuits for ensemble computation. In: Cimatti, A., Sebastiani, R. (eds.) SAT 2012. LNCS, vol. 7317, pp. 369–382. Springer, Heidelberg (2012)
Junttila, T.A., Niemelä, I.: Towards an efficient tableau method for Boolean circuit satisfiability checking. In: Palamidessi, C., et al. (eds.) CL 2000. LNCS (LNAI), vol. 1861, pp. 553–567. Springer, Heidelberg (2000)
Kojevnikov, A., Kulikov, A.S., Yaroslavtsev, G.: Finding efficient circuits using SAT-solvers. In: Kullmann, O. (ed.) SAT 2009. LNCS, vol. 5584, pp. 32–44. Springer, Heidelberg (2009)
Lynch, N.A.: Distributed Algorithms. Morgan Kaufmann, San Francisco (1996)
Manna, Z., Wolper, P.: Synthesis of communicating processes from temporal logic specifications. ACM Transactions on Programming Languages and Systems 6(1), 68–93 (1984)
Moscibroda, T., Oshman, R.: Resilience of mutual exclusion algorithms to transient memory faults. In: Proc. 30th Symposium on Principles of Distributed Computing (PODC 2011), pp. 69–78. ACM Press, New York (2011)
Pease, M.C., Shostak, R.E., Lamport, L.: Reaching agreement in the presence of faults. Journal of the ACM 27(2), 228–234 (1980)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2013 Springer International Publishing Switzerland
About this paper
Cite this paper
Dolev, D., Korhonen, J.H., Lenzen, C., Rybicki, J., Suomela, J. (2013). Synchronous Counting and Computational Algorithm Design. In: Higashino, T., Katayama, Y., Masuzawa, T., Potop-Butucaru, M., Yamashita, M. (eds) Stabilization, Safety, and Security of Distributed Systems. SSS 2013. Lecture Notes in Computer Science, vol 8255. Springer, Cham. https://doi.org/10.1007/978-3-319-03089-0_17
Download citation
DOI: https://doi.org/10.1007/978-3-319-03089-0_17
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-03088-3
Online ISBN: 978-3-319-03089-0
eBook Packages: Computer ScienceComputer Science (R0)