Synchronous counting and computational algorithm design
| العنوان: | Synchronous counting and computational algorithm design |
|---|---|
| المؤلفون: | Keijo Heljanko, Christoph Lenzen, Jukka Suomela, Matti Järvisalo, Joel Rybicki, Danny Dolev, Siert Wieringa, Janne H. Korhonen |
| المصدر: | JOURNAL OF COMPUTER AND SYSTEM SCIENCES. 82(2):310-332 |
| سنة النشر: | 2016 |
| مصطلحات موضوعية: | FOS: Computer and information sciences, Theoretical computer science, Computational complexity theory, Computer Networks and Communications, Deterministic algorithm, Computer science, Boolean circuit, Self-stabilisation, 02 engineering and technology, Computational Complexity (cs.CC), Theoretical Computer Science, Byzantine fault tolerance, Synthesis, Consensus, 020204 information systems, Computer Science - Data Structures and Algorithms, 0202 electrical engineering, electronic engineering, information engineering, Data Structures and Algorithms (cs.DS), ta518, ta515, ta113, ta112, ta213, Applied Mathematics, Formal methods, Data structure, Satisfiability, Distributed computing, Computer Science - Computational Complexity, Computational Theory and Mathematics, Computer Science - Distributed, Parallel, and Cluster Computing, ta5141, 020201 artificial intelligence & image processing, Node (circuits), SAT, Distributed, Parallel, and Cluster Computing (cs.DC), Algorithm |
| الوصف: | 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. 35 pages, extended and revised version |
| اللغة: | English |
| تدمد: | 0022-0000 |
| URL الوصول: | https://explore.openaire.eu/search/publication?articleId=doi_dedup___::f39fbd20df8b4b32d12d8f75c41e499f http://juuli.fi/Record/0281959416 |
| حقوق: | OPEN |
| رقم الأكسشن: | edsair.doi.dedup.....f39fbd20df8b4b32d12d8f75c41e499f |
| قاعدة البيانات: | OpenAIRE |
| تدمد: | 00220000 |
|---|