2017/10/29 by Ondřej Lengál, Anthony W. Lin, Lengal, Ondrej +5 · 2 citations
Computer Science · #Distributed #Distributed systems and fault tolerance #FOS: Computer and information sciences #Formal Languages and Automata Theory (cs.FL) #Formal Methods in Verification #Logic in Computer Science (cs.LO) #Logic, programming, and type systems #Model-Driven Software Engineering Techniques #Parallel #and Cluster Computing (cs.DC)
paper · pdf · doi:10.48550/arxiv.1710.10756
openalex publication_date 2017/10/29 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
We consider the problem of automatically verifying that a parameterized\nfamily of probabilistic concurrent systems terminates with probability one for\nall instances against adversarial schedulers. A parameterized family defines an\ninfinite-state system: for each number n, the family consists of an instance\nwith n finite-state processes. In contrast to safety, the parameterized\nverification of liveness is currently still considered extremely challenging\nespecially in the presence of probabilities in the model. One major challenge\nis to provide a sufficiently powerful symbolic framework. One well-known\nsymbolic framework for the parameterized verification of non-probabilistic\nconcurrent systems is regular model checking. Although the framework was\nrecently extended to probabilistic systems, incorporating fairness in the\nframework - often crucial for verifying termination - has been especially\ndifficult due to the presence of an infinite number of fairness constraints\n(one for each process). Our main contribution is a systematic,\nregularity-preserving, encoding of finitary fairness (a realistic notion of\nfairness proposed by Alur & Henzinger) in the framework of regular model\nchecking for probabilistic parameterized systems. Our encoding reduces\ntermination with finitary fairness to verifying parameterized termination\nwithout fairness over probabilistic systems in regular model checking (for\nwhich a verification framework already exists). We show that our algorithm\ncould verify termination for many interesting examples from distributed\nalgorithms (Herman's protocol) and evolutionary biology (Moran process, cell\ncycle switch), which do not hold under the standard notion of fairness. To the\nbest of our knowledge, our algorithm is the first fully-automatic method that\ncan prove termination for these examples.\n