%0 Conference Proceedings
%T Specification-Based Synthesis of Distributed Self-Stabilizing Protocols
%+ McMaster University [Hamilton, Ontario]
%+ Université Pierre et Marie Curie - Paris 6 (UPMC)
%+ Michigan State University [East Lansing]
%A Faghih, Fathiyeh
%A Bonakdarpour, Borzoo
%A Tixeuil, Sébastien
%A Kulkarni, Sandeep
%< avec comité de lecture
%( Lecture Notes in Computer Science
%B 36th International Conference on Formal Techniques for Distributed Objects, Components, and Systems (FORTE)
%C Heraklion, Greece
%Y Elvira Albert
%Y Ivan Lanese
%3 Formal Techniques for Distributed Objects, Components, and Systems
%V LNCS-9688
%P 124-141
%8 2016-06-06
%D 2016
%R 10.1007/978-3-319-39570-8_9
%Z Computer Science [cs]
%Z Computer Science [cs]/Networking and Internet Architecture [cs.NI]Conference papers
%X 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.
%G English
%Z TC 6
%Z WG 6.1
%2 https://inria.hal.science/hal-01432932/document
%2 https://inria.hal.science/hal-01432932/file/426757_1_En_9_Chapter.pdf
%L hal-01432932
%U https://inria.hal.science/hal-01432932
%~ UPMC
%~ IFIP-LNCS
%~ IFIP
%~ IFIP-TC
%~ IFIP-WG
%~ IFIP-TC6
%~ IFIP-WG6-1
%~ IFIP-FORTE
%~ IFIP-LNCS-9688
%~ SORBONNE-UNIVERSITE
%~ SU-TI
%~ ALLIANCE-SU