Checking Qualitative Liveness Properties of Replicated Systems
with Stochastic Scheduling

D 2020

Checking Qualitative Liveness Properties of Replicated Systems with Stochastic Scheduling

BLONDIN, Michael, Javier ESPARZA, Martin HELFRICH, Antonín KUČERA, Philipp MEYER et. al.

Basic information

Original name

Checking Qualitative Liveness Properties of Replicated Systems with Stochastic Scheduling

Authors

BLONDIN, Michael (124 Canada), Javier ESPARZA (724 Spain), Martin HELFRICH (276 Germany), Antonín KUČERA (203 Czech Republic, guarantor, belonging to the institution) and Philipp MEYER (276 Germany)

Edition

Cham, Německo, Computer Aided Verification, CAV 2020, p. 372-397, 26 pp. 2020

Publisher

Springer International Publishing

Other information

Language

English

Type of outcome

Stať ve sborníku

Field of Study

10200 1.2 Computer and information sciences

Country of publisher

Germany

Confidentiality degree

není předmětem státního či obchodního tajemství

Publication form

printed version "print"

References:

URL

Impact factor

Impact factor: 0.402 in 2005

RIV identification code

RIV/00216224:14330/20:00114297

Organization unit

Faculty of Informatics

ISBN

978-3-030-53290-1

ISSN

DOI

http://dx.doi.org/10.1007/978-3-030-53291-8_20

UT WoS

000695272500020

Keywords in English

Replicated systems; population protocols

Abstract

V originále

We present a sound and complete method for the verification of qualitative liveness properties of replicated systems under stochastic scheduling. These are systems consisting of a finite-state program, executed by an unknown number of indistinguishable agents, where the next agent to make a move is determined by the result of a random experiment. We show that if a property of such a system holds, then there is always a witness in the shape of a Presburger stage graph: a finite graph whose nodes are Presburger-definable sets of configurations. Due to the high complexity of the verification problem (non-elementary), we introduce an incomplete procedure for the construction of Presburger stage graphs, and implement it on top of an SMT solver. The procedure makes extensive use of the theory of well-quasi-orders, and of the structural theory of Petri nets and vector addition systems. We apply our results to a set of benchmarks, in particular to a large collection of population protocols, a model of distributed computation extensively studied by the distributed computing community.

Links

GA18-11193S, research and development project

Name: Algoritmy pro diskrétní systémy a hry s nekonečně mnoha stavy

Investor: Czech Science Foundation

Citovat

BLONDIN, Michael, Javier ESPARZA, Martin HELFRICH, Antonín KUČERA and Philipp MEYER. Checking Qualitative Liveness Properties of Replicated Systems with Stochastic Scheduling. In Shuvendu K. Lahiri, Chao Wang. Computer Aided Verification, CAV 2020. Cham, Německo: Springer International Publishing, 2020, p. 372-397. ISBN 978-3-030-53290-1. Available from: https://dx.doi.org/10.1007/978-3-030-53291-8_20.

@inproceedings{1676581,
   author = {Blondin, Michael and Esparza, Javier and Helfrich, Martin and Kučera, Antonín and Meyer, Philipp},
   address = {Cham, Německo},
   booktitle = {Computer Aided Verification, CAV 2020},
   doi = {http://dx.doi.org/10.1007/978-3-030-53291-8_20},
   editor = {Shuvendu K. Lahiri, Chao Wang},
   keywords = {Replicated systems; population protocols},
   howpublished = {tištěná verze "print"},
   language = {eng},
   location = {Cham, Německo},
   isbn = {978-3-030-53290-1},
   pages = {372-397},
   publisher = {Springer International Publishing},
   title = {Checking Qualitative Liveness Properties of Replicated Systems with Stochastic Scheduling},
   url = {https://doi.org/10.1007/978-3-030-53291-8_20},
   year = {2020}
}

TY  - JOUR
ID  - 1676581
AU  - Blondin, Michael - Esparza, Javier - Helfrich, Martin - Kučera, Antonín - Meyer, Philipp
PY  - 2020
TI  - Checking Qualitative Liveness Properties of Replicated Systems with Stochastic Scheduling
PB  - Springer International Publishing
CY  - Cham, Německo
SN  - 9783030532901
KW  - Replicated systems
KW  - population protocols
UR  - https://doi.org/10.1007/978-3-030-53291-8_20
L2  - https://doi.org/10.1007/978-3-030-53291-8_20
N2  - We present a sound and complete method for the verification of qualitative liveness properties of replicated systems under stochastic scheduling. These are systems consisting of a finite-state program, executed by an unknown number of indistinguishable agents, where the next agent to make a move is determined by the result of a random experiment. We show that if a property of such a system holds, then there is always a witness in the shape of a Presburger stage graph: a finite graph whose nodes are Presburger-definable sets of configurations. Due to the high complexity of the verification problem (non-elementary), we introduce an incomplete procedure for the construction of Presburger stage graphs, and implement it on top of an SMT solver. The procedure makes extensive use of the theory of well-quasi-orders, and of the structural theory of Petri nets and vector addition systems. We apply our results to a set of benchmarks, in particular to a large collection of population protocols, a model of distributed computation extensively studied by the distributed computing community.
ER  -

BLONDIN, Michael, Javier ESPARZA, Martin HELFRICH, Antonín KUČERA and Philipp MEYER. Checking Qualitative Liveness Properties of Replicated Systems with Stochastic Scheduling. In Shuvendu K. Lahiri, Chao Wang. \textit{Computer Aided Verification, CAV 2020}. Cham, Německo: Springer International Publishing, 2020, p.~372-397. ISBN~978-3-030-53290-1. Available from: https://dx.doi.org/10.1007/978-3-030-53291-8\_{}20.

Detailed Information on Publication Record