Fair Termination for Parameterized Probabilistic Concurrent Systems

Result code in IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216305%3A26230%2F17%3APU123659" target="_blank" >RIV/00216305:26230/17:PU123659 - isvavai.cz</a>

Result on the web

<a href="https://www.fit.vut.cz/research/publication/11324/" target="_blank" >https://www.fit.vut.cz/research/publication/11324/</a>

DOI - Digital Object Identifier

<a href="http://dx.doi.org/10.1007/978-3-662-54577-5_29" target="_blank" >10.1007/978-3-662-54577-5_29</a>

Result language

angličtina

Original language name

Fair Termination for Parameterized Probabilistic Concurrent Systems

Original language description

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.

Czech name

—

Czech description

—

Type

D - Article in proceedings

CEP classification

—

OECD FORD branch

10201 - Computer sciences, information science, bioinformathics (hardware development to be 2.2, social aspect to be 5.8)

Project

Result was created during the realization of more than one project. More information in the Projects tab.

Continuities

P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)

Publication year

2017

Confidentiality

S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů

Article name in the collection

Proceedings of TACAS'17

ISBN

978-3-662-46680-3

ISSN

0302-9743

e-ISSN

—

Number of pages

19

Pages from-to

499-517

Publisher name

Springer Verlag

Place of publication

Heidelberg

Event location

Uppsala

Event date

Apr 22, 2017

Type of event by nationality

WRD - Celosvětová akce

UT code for WoS article

000440734900029