# Verification and Synthesis of Symmetric Uni-Rings for Leads-To Properties

## TL;DR

This paper explores the verification and synthesis of symmetric uni-ring protocols satisfying leadsto properties, revealing undecidability in verification but decidability and polynomial-time synthesis methods for protocol generation.

## Contribution

It establishes the undecidability of verification and introduces a decidable, polynomial-time synthesis approach for symmetric uni-ring protocols satisfying leadsto properties.

## Key findings

- Verification of leadsto properties is undecidable.
- Synthesis of protocols satisfying leadsto is decidable and efficient.
- Synthesized protocols include agreement and parity protocols.

## Abstract

This paper investigates the verification and synthesis of parameterized protocols that satisfy leadsto properties $R \leadsto Q$ on symmetric unidirectional rings (a.k.a. uni-rings) of deterministic and constant-space processes under no fairness and interleaving semantics, where $R$ and $Q$ are global state predicates. First, we show that verifying $R \leadsto 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 \leadsto Q$ is actually decidable. We identify necessary and sufficient conditions for the decidability of synthesis based on which we devise a sound and complete polynomial-time algorithm that takes the predicates $R$ and $Q$, and automatically generates a parameterized protocol that satisfies $R \leadsto Q$ for unbounded (but finite) ring sizes. Moreover, we present some decidability results for cases where leadsto is required from multiple distinct $R$ predicates to different $Q$ predicates. To demonstrate the practicality of our synthesis method, we synthesize some parameterized protocols, including agreement and parity protocols.