Conference paperLENGÁL Ondřej, LIN Anthony W., MAJUMDAR Rupak and RUMMER Philipp. Fair Termination for Parameterized Probabilistic Concurrent Systems. In: Proceedings of TACAS'17. Heidelberg: Springer Verlag, 2017, pp. 499517. ISBN 9783662466803. ISSN 03029743.  Publication language:  english 

Original title:  Fair Termination for Parameterized Probabilistic Concurrent Systems 

Title (cs):  Spravedlivá terminace pro parametrické pravděpodobnostní paralelní systémy 

Pages:  499517 

Proceedings:  Proceedings of TACAS'17 

Conference:  European Joint Conferences on Theory and Practice of Software 

Series:  LNCS 10205 

Place:  Heidelberg, DE 

Year:  2017 

ISBN:  9783662466803 

Journal:  Lecture Notes in Computer Science, No. 10205, DE 

ISSN:  03029743 

DOI:  10.1007/9783662545775_29 

Publisher:  Springer Verlag 

Keywords 

Probabilistic verification Parameterized verification Regular model checking Fairness Liveness 
Annotation 

We consider the problem of automatically verifying that a parameterized family of probabilistic concurrent systems terminates with probability one for all instances against adversarial schedulers. A parameterized family defines an infinitestate system: for each number n, the family consists of an instance with n finitestate processes. In contrast to safety, the parameterized verification of liveness is currently still considered extremely challenging especially in the presence of probabilities in the model. One major challenge is to provide a sufficiently powerful symbolic framework. One wellknown symbolic framework for the parameterized verification of nonprobabilistic concurrent systems is regular model checking. Although the framework was recently extended to probabilistic systems, incorporating fairness in the framework  often crucial for verifying termination  has been especially difficult due to the presence of an infinite number of fairness constraints (one for each process). Our main contribution is a systematic, regularitypreserving, encoding of finitary fairness (a realistic notion of fairness proposed by Alur & Henzinger) in the framework of regular model checking for probabilistic parameterized systems. Our encoding reduces termination with finitary fairness to verifying parameterized termination without fairness over probabilistic systems in regular model checking (for which a verification framework already exists). We show that our algorithm could verify termination for many interesting examples from distributed algorithms (Hermans protocol) and evolutionary biology (Moran process, cell cycle switch), which do not hold under the standard notion of fairness. To the best of our knowledge, our algorithm is the first fullyautomatic method that can prove termination for these examples. 
BibTeX: 

@INPROCEEDINGS{
author = {Ond{\v{r}}ej Leng{\'{a}}l and W. Anthony Lin and
Rupak Majumdar and Philipp Rummer},
title = {Fair Termination for Parameterized Probabilistic
Concurrent Systems},
pages = {499517},
booktitle = {Proceedings of TACAS'17},
series = {LNCS 10205},
journal = {Lecture Notes in Computer Science},
number = 10205,
year = 2017,
location = {Heidelberg, DE},
publisher = {Springer Verlag},
ISBN = {9783662466803},
ISSN = {03029743},
doi = {10.1007/9783662545775_29},
language = {english},
url = {http://www.fit.vutbr.cz/research/view_pub.php?id=11324}
} 
