Title
Specification-based Synthesis of Distributed Self-Stabilizing Protocols
Abstract
In this paper, we introduce an SMT-based method that automatically synthesizes a distributed self-stabilizing protocol from a given high-level specification and the 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 also extend our approach to synthesize ideal-stabilizing protocols, where every state is legitimate. Our proposed methods are implemented and we report successful synthesis of Dijkstra's token ring and a self-stabilizing version of Raymond's mutual exclusion algorithm, as well as ideal-stabilizing leader election and local mutual exclusion.
Year
DOI
Venue
2015
10.1007/978-3-319-39570-8_9
FORTE
Field
DocType
Volume
Leader election,Suzuki-Kasami algorithm,Computer science,Token ring,Network topology,Theoretical computer science,Mutual exclusion,Distributed computing,Dijkstra's algorithm
Journal
abs/1509.05664
ISSN
Citations 
PageRank 
0302-9743
2
0.36
References 
Authors
12
4
Name
Order
Citations
PageRank
Fathiyeh Faghih1114.33
Borzoo Bonakdarpour249045.02
Sebastien Tixeuil31028.38
Sandeep S. Kulkarni486379.94