کد مقاله | کد نشریه | سال انتشار | مقاله انگلیسی | نسخه تمام متن |
---|---|---|---|---|
429774 | 687672 | 2016 | 23 صفحه PDF | دانلود رایگان |
• We develop computational techniques to find algorithms for synchronous 2-counting.
• Automated synthesis yields state-optimal self-stabilising fault-tolerant algorithms.
• We give a thorough experimental comparison of our two SAT-based synthesis techniques.
• A direct SAT encoding is more efficient for finding time-optimal algorithms.
• An iterative CEGAR-based approach finds non-optimal algorithms quickly.
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=1f=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.
Journal: Journal of Computer and System Sciences - Volume 82, Issue 2, March 2016, Pages 310–332