Checking Qualitative Liveness Properties of Replicated Systems with Stochastic Scheduling
| Autoři | |
|---|---|
| Rok publikování | 2020 |
| Druh | Článek ve sborníku |
| Konference | Computer Aided Verification, CAV 2020 |
| Fakulta / Pracoviště MU | |
| 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: |