*Journal of Computer and System Sciences* · volume 82, issue 2, pages 310–332, 2016 · doi:10.1016/j.jcss.2015.09.002

Consider a complete communication network on $n$ nodes, each of which is a state machine. 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.

This work consists of two parts. In the first part, we use computational techniques (often known as *synthesis*) 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 per node are sufficient for all values $n \ge 4$. Moreover, the problem cannot be solved with only 2 states per node for $n = 4$, but there is a 2-state solution for all values $n \ge 6$.

In the second part, we develop and compare two different approaches for synthesising synchronous counting algorithms. Both approaches are based on casting the synthesis problem as a propositional satisfiability (SAT) problem and employing modern SAT-solvers. The difference lies in how to solve the SAT problem: either in a direct fashion, or incrementally within a *counter-example guided abstraction refinement* loop. Empirical results suggest that the former technique is more efficient if we want to synthesise time-optimal algorithms, while the latter technique discovers non-optimal algorithms more quickly.

- Danny Dolev, Janne H. Korhonen, Christoph Lenzen, Joel Rybicki, and Jukka Suomela: Synchronous counting and computational algorithm design · SSS 2013