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.
|
