Synchronous counting and computational algorithm design
Synchronous counting and computational algorithm design
复制标题
同步计数与计算算法设计
DOI：
10.1016/j.jcss.2015.09.002
复制
发表时间：
2013
影响因子：
5.9
通讯作者：
Siert Wieringa
中科院分区：
文献类型：
--
作者：
D. Dolev;Keijo Heljanko;Matti Järvisalo;Janne H. Korhonen;C. Lenzen;Joel Rybicki;J. Suomela;Siert Wieringa
考虑一个由n个节点组成的完整通信网络。在同步2计数中，节点接收公共时钟脉冲，并且它们必须就哪些脉冲是“奇”而哪些是“偶”达成一致。此外，解决方案需要自稳定（从任何初始状态达到正确的操作）并容忍f拜占庭故障（发送任意错误信息的节点）。先前的算法要么需要随机位的源，要么每个节点需要大量的状态。在这项工作中，我们给出了快速的状态最优确定性算法的第一个非平凡的情况下f= 1。为了获得这些算法，我们开发和评估两种不同的算法合成技术。两者都是基于铸造的综合问题作为一个命题可满足性（SAT）的问题，直接编码是有效的合成时间最优算法，而基于反例指导抽象细化的方法发现非最优算法迅速。
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.
DOI：
10.1016/j.jcss.2007.07.005
发表时间：
2008-09
期刊：
J. Comput. Syst. Sci.
影响因子：
--
作者：
Jeremy T. Bradley;S. Gilmore;J. Hillston
通讯作者：
Jeremy T. Bradley;S. Gilmore;J. Hillston