Verification and Synthesis of Responsive Symmetric Uni-Rings
Ali Ebnenasir · IEEE Transactions on Software Engineering · 2021
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.