一句话：提出基于SMT的方法，从高层规约和网络拓扑自动合成分布式自稳定协议。
现有自稳定协议合成方法通常需要显式给出合法状态集合，限制了自动化程度。本文提出一种基于SMT的自动合成方法，仅需高层规约中的时序行为与网络拓扑，即可生成分布式自稳定协议。作者进一步将方法扩展到理想稳定协议（每个状态均合法）和单调稳定协议（恢复期间每进程至多执行一次动作）。方法已完整实现，并成功合成Dijkstra令牌环、Raymond互斥算法的自稳定版本、理想稳定的领导者选举与局部互斥，以及单调稳定的最大独立集和分布式Grundy着色等经典协议。
In this paper, we introduce an SMT-based method that automatically synthesizes a distributed self-stabilizing protocol from a given high-level specification and network topology. Unlike existing approaches, where synthesis algorithms require the explicit description of the set of legitimate states, our technique only needs the temporal behavior of the protocol. We extend our approach to synthesize ideal-stabilizing protocols, where every state is legitimate. We also extend our technique to synthesize monotonic-stabilizing protocols, where during recovery, each process can execute an most once one action. Our proposed methods are fully implemented and we report successful synthesis of well-known protocols such as Dijkstra's token ring, a self-stabilizing version of Raymond's mutual exclusion algorithm, ideal-stabilizing leader election and local mutual exclusion, as well as monotonic-stabilizing maximal independent set and distributed Grundy coloring.
@article{paperbot430,
title = {Automated Synthesis of Distributed Self-Stabilizing Protocols},
author = {Fathiyeh Faghih and Borzoo Bonakdarpour and Sebastien Tixeuil and Sandeep Kulkarni},
journal = {Logical Methods in Computer Science},
volume = {Volume 14, Issue 1},
year = {2018},
doi = {10.23638/lmcs-14(1:12)2018}
}