This repository contains supporting material related to the following paper:
- Danny Dolev, Keijo Heljanko, Matti Järvisalo, Janne H. Korhonen, Christoph Lenzen, Joel Rybicki, Jukka Suomela, and Siert Wieringa: "Synchronous Counting and Computational Algorithm Design", Journal of Computer and System Sciences (to appear), http://arxiv.org/abs/1304.5719
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).
In this repository we have computer-generated deterministic algorithms
that provide solutions to the following cases (see directory positive):
- s = 3, n ≥ 4, f = 1
- s = 2, n ≥ 6, f = 1
We also have a compact, computer-generated proof that the following
case is not solvable by any algorithm (see directory negative):
- s = 2, n = 4, f = 1
We provide Python scripts that can be used to verify that the algorithms
and the lower-bound proofs are correct (see directory code).
For a quick start, try:
cd code
./verify-all.sh
For some illustrations of the computer-generated algorithms, see the
directory illustrations.
Synthesis tools for finding computer-generated algorithms are given in
the synthesis directory.
- Danny Dolev, The Hebrew University of Jerusalem
- Keijo Heljanko, HIIT and Aalto University
- Matti Järvisalo HIIT and University of Helsinki
- Janne H. Korhonen, HIIT and University of Helsinki
- Christoph Lenzen, MPI Saarbrücken
- Joel Rybicki, HIIT and Aalto University
- Jukka Suomela, HIIT and Aalto University
- Siert Wieringa, HIIT and Aalto University