Accelerating Protocol Synthesis and Detecting Unrealizability with Interpretation Reduction
Derek Egolf, Stavros Tripakis
TL;DR
This work tackles automated synthesis of symbolic distributed protocols by introducing a sketch-based CEGIS framework enhanced with interpretation reduction, which partitions the search space into equivalence classes to avoid redundant completions while pruning known counterexamples before verification. The approach formalizes protocols in TLA+ as $\langle Vars, Holes, Init, Next_0\rangle$ with holes carrying grammars, enabling parameterized sketches, and defines precise pruning constraints for safety, deadlock, and liveness (plus a practical stuttering variant) to guarantee soundness, completeness, and terminating behavior when there are finitely many interpretation-equivalence classes. The method, implemented in PolySemist, significantly outperforms the previous state of the art (Scythe) across realizable and unrealizable benchmarks, with rapid synthesis of entire protocols from scratch in under 3 minutes and substantially higher unrealizability detection rates. The results demonstrate that interpretation reduction, together with exact generalization of counterexamples, yields robust improvements in both efficiency and scalability for distributed protocol synthesis in temporal logic frameworks, enabling practical application to real-world protocols.
Abstract
We present a novel counterexample-guided, sketch-based method for the synthesis of symbolic distributed protocols in TLA+. Our method's chief novelty lies in a new search space reduction technique called interpretation reduction, which allows to not only eliminate incorrect candidate protocols before they are sent to the verifier, but also to avoid enumerating redundant candidates in the first place. Further performance improvements are achieved by an advanced technique for exact generalization of counterexamples. Experiments on a set of established benchmarks show that our tool is almost always faster than the state of the art, often by orders of magnitude, and was also able to synthesize an entire TLA+ protocol "from scratch" in less than 3 minutes where the state of the art timed out after an hour. Our method is sound, complete, and guaranteed to terminate on unrealizable synthesis instances under common assumptions which hold in all our benchmarks.