Checking Qualitative Liveness Properties of Replicated Systems with Stochastic Scheduling

Logo poskytovatele

Varování

Publikace nespadá pod Ekonomicko-správní fakultu, ale pod Fakultu informatiky. Oficiální stránka publikace je na webu muni.cz.
Autoři

BLONDIN Michael ESPARZA Javier HELFRICH Martin KUČERA Antonín MEYER Philipp

Rok publikování 2020
Druh Článek ve sborníku
Konference Computer Aided Verification, CAV 2020
Fakulta / Pracoviště MU

Fakulta informatiky

Citace
www https://doi.org/10.1007/978-3-030-53291-8_20
Doi http://dx.doi.org/10.1007/978-3-030-53291-8_20
Klíčová slova Replicated systems; population protocols
Popis 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.
Související projekty:

Používáte starou verzi internetového prohlížeče. Doporučujeme aktualizovat Váš prohlížeč na nejnovější verzi.