- Specification's authors: Giuliano Losa
- Original paper: Kumar, Devendra. A class of termination detection algorithms for distributed computations. International Conference on Foundations of Software Technology and Theoretical Computer Science. Springer, Berlin, Heidelberg, 1985.
- Also appears in: Mattern, Friedemann. Algorithms for distributed termination detection. Distributed computing 2.3 (1987): 161-175.
- Extended modules: Integers, FiniteSets, Apalache, Sequences
- Computation models: asynchronous without faults
- Some properties checked with Apalache: an inductive invariant implying safety (checked inductive for 5 processes)
- TLA+ files and explanations