Verification and Synthesis of Responsive Symmetric Uni-Rings

This paper investigates the verification and synthesis of parameterized protocols that satisfy leadsto properties on symmetric unidirectional rings (a.k.a. uni-rings) of deterministic, self-disabling and constant-space processes. First, we show that when
$R$
and
$Q$
are conjunctive global state predicates, verifying ‘
$R$
leadsto
$Q$
’ (denoted
$R \leadsto Q$
) for parameterized protocols on symmetric uni-rings is undecidable. 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 design and implement a sound and complete 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 show that verifying leadsto properties remains undecidable even if
$R$
and
$Q$
are local state predicates! This result would lead to the impossibility of computing a cutoff for local leadsto on symmetric rings of deterministic, self-disabling and constant-space processes. We further show that verifying local and global deadlocks in our formal setting are decidable problems. We also present a cutoff theorem that enables the construction of symmetric rings where deadlocks are reachable.