Faculty of Information Technology, BUT

Publication Details

Fair Termination for Parameterized Probabilistic Concurrent Systems

LENGÁL Ondřej, LIN Anthony W., MAJUMDAR Rupak and RUMMER Philipp. Fair Termination for Parameterized Probabilistic Concurrent Systems. In: Proceedings of TACAS'17. Lecture Notes in Computer Science, vol. 10205. Heidelberg: Springer Verlag, 2017, pp. 499-517. ISBN 978-3-662-46680-3. ISSN 0302-9743.
Czech title
Spravedlivá terminace pro parametrické pravděpodobnostní paralelní systémy
Type
conference paper
Language
english
Authors
Lengál Ondřej, Ing., Ph.D. (DITS FIT BUT)
Lin Anthony W. (UOx)
Majumdar Rupak (MPII)
Rummer Philipp (Uppsala)
Keywords

Probabilistic verification
Parameterized verification
Regular model checking
Fairness
Liveness
Abstract
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 infinite-state system: for each number n, the family consists of an instance with n finite-state 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 well-known symbolic framework for the parameterized verification of non-probabilistic 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, regularity-preserving, 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 fully-automatic method that can prove termination for these examples.
Published
2017
Pages
499-517
Journal
Lecture Notes in Computer Science, vol. 10205, ISSN 0302-9743
Proceedings
Proceedings of TACAS'17
Series
Lecture Notes in Computer Science
Conference
European Joint Conferences on Theory and Practice of Software, Uppsala, SE
ISBN
978-3-662-46680-3
Publisher
Springer Verlag
Place
Heidelberg, DE
DOI
BibTeX
@INPROCEEDINGS{FITPUB11324,
   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 = "499--517",
   booktitle = "Proceedings of TACAS'17",
   series = "Lecture Notes in Computer Science",
   journal = "Lecture Notes in Computer Science",
   volume = 10205,
   year = 2017,
   location = "Heidelberg, DE",
   publisher = "Springer Verlag",
   ISBN = "978-3-662-46680-3",
   ISSN = "0302-9743",
   doi = "10.1007/978-3-662-54577-5\_29",
   language = "english",
   url = "https://www.fit.vut.cz/research/publication/11324"
}
Back to top