Synchronous counting and computational algorithm design
作者：
Highlights：
• 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.
摘要
•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.
论文关键词：Distributed computing,Self-stabilisation,Byzantine fault tolerance,Synthesis,Formal methods,SAT
论文评审过程：Received 8 January 2015, Revised 1 September 2015, Accepted 11 September 2015, Available online 23 October 2015, Version of Record 27 November 2015.
论文官网地址：https://doi.org/10.1016/j.jcss.2015.09.002
