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.

Základní údaje

Originální název

Checking Qualitative Liveness Properties of Replicated Systems with Stochastic Scheduling

Autoři

BLONDIN, Michael (124 Kanada), Javier ESPARZA (724 Španělsko), Martin HELFRICH (276 Německo), Antonín KUČERA (203 Česká republika, garant, domácí) a Philipp MEYER (276 Německo)

Vydání

Cham, Německo, Computer Aided Verification, CAV 2020, od s. 372-397, 26 s. 2020

Nakladatel

Springer International Publishing

Další údaje

Jazyk

angličtina

Typ výsledku

Stať ve sborníku

Obor

10200 1.2 Computer and information sciences

Stát vydavatele

Německo

Utajení

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

Forma vydání

tištěná verze "print"

Odkazy

URL

Impakt faktor

Impact factor: 0.402 v roce 2005

Kód RIV

RIV/00216224:14330/20:00114297

Organizační jednotka

Fakulta informatiky

ISBN

978-3-030-53290-1

ISSN

DOI

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

UT WoS

000695272500020

Klíčová slova anglicky

Replicated systems; population protocols

Štítky

core_A, firank_1

Příznaky

Mezinárodní význam, Recenzováno

Změněno: 29. 4. 2021 12:28, RNDr. Pavel Šmerk, Ph.D.

Anotace

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.

Návaznosti

GA18-11193S, projekt VaV

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

Investor: Grantová agentura ČR, Algoritmy pro diskrétní systémy a hry s nekonečně mnoha stavy

Citovat

BLONDIN, Michael, Javier ESPARZA, Martin HELFRICH, Antonín KUČERA a 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, s. 372-397. ISBN 978-3-030-53290-1. Dostupné z: 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 a 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, s.~372-397. ISBN~978-3-030-53290-1. Dostupné z: https://dx.doi.org/10.1007/978-3-030-53291-8\_{}20.

Podrobný výpis o publikaci