Termination in Extended Probabilistic Threshold Automata

Scaling up distributed systems increases also the chance that some node ceases to operate correctly, which turns fault tolerance into an essential trait. To achieve fault tolerance, numerous distributed algorithms, including reliable broadcast and consensus, depend on threshold guards. A threshold guard can, for example, ensure that a process waits for a majority of its peers to acknowledge that they reached a certain state in the distributed algorithm, before the process makes any progress. Threshold automata are computational models that allow fully automated parameterized verification of single- and multi-round threshold-based distributed algorithms (FTDA), where often the number of processes and the proportion of faulty processes are parameters. However, due to the fact that such algorithms have to cope with faulty processes not answering or, more generally, behaving in an arbitrary potentially malicious manner, liveness must only depend on a subset of processes, while ideally all correct processes should be considered in the termination properties of such algorithm. In this paper, we present a novel reasoning technique for proving almost-sure termination in extended probablistic threshold automata, by detecting strongly connected components (SCCs) in extended probabilistic and in ordinary threshold automata to reduce almost-sure termination to reachability in a finite abstract system.