Other formats:
BibTeX
LaTeX
RIS
@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.
|