Synchronous counting and computational algorithm design

Danny Dolev, Keijo Heljanko, Matti Järvisalo, Janne Korhonen, Christoph Lenzen, Joel Rybicki*, Jukka Suomela, Siert Wieringa

*Corresponding author for this work

Research output: Contribution to journalArticleScientificpeer-review

11 Citations (Scopus)


Consider a complete communication network on n nodes. 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". Furthermore, the solution needs to be self-stabilising (reaching correct operation from any initial state) and tolerate f Byzantine failures (nodes that send arbitrary misinformation). Prior algorithms either require a source of random bits or a large number of states per node. In this work, we give fast state-optimal deterministic algorithms for the first non-trivial case f=1. To obtain these algorithms, we develop and evaluate two different techniques for algorithm synthesis. Both are based on casting the synthesis problem as a propositional satisfiability (SAT) problem; a direct encoding is efficient for synthesising time-optimal algorithms, while an approach based on counter-example guided abstraction refinement discovers non-optimal algorithms quickly.

Original languageEnglish
Pages (from-to)310-332
Number of pages23
Issue number2
Publication statusPublished - 1 Mar 2016
MoE publication typeA1 Journal article-refereed


  • Byzantine fault tolerance
  • Distributed computing
  • Formal methods
  • SAT
  • Self-stabilisation
  • Synthesis

Fingerprint Dive into the research topics of 'Synchronous counting and computational algorithm design'. Together they form a unique fingerprint.

Cite this