Verification and synthesis of symmetric uni-rings for leads-to properties

This paper investigates the verification and synthesis of parameterized protocols that satisfy global leads to properties R ~→ Q on symmetric unidirectional rings (a.k.a. uni-rings) of deterministic and constant-space processes, where R and Q denote global state predicates. First, we show that verifying R ~→ Q for parameterized protocols on symmetric uni-rings is undecidable, even for deterministic and constant-space processes, and conjunctive state predicates. Then, we show that surprisingly synthesizing symmetric uni-ring protocols that satisfy R ~→ Q is actually decidable. We identify necessary and sufficient conditions for the decidability of synthesis based on which we devise a sound and complete algorithm that takes the predicates R and Q, and automatically generates a parameterized protocol that satisfies R ~→ Q for unbounded (but finite) ring sizes. We use our algorithm to synthesize some parameterized protocols, including an agreement protocol