Checking Qualitative Liveness Properties of Replicated Systems with Stochastic Scheduling
| Authors | |
|---|---|
| Year of publication | 2020 |
| Type | Article in Proceedings |
| Conference | Computer Aided Verification, CAV 2020 |
| MU Faculty or unit | |
| Citation | |
| Web | https://doi.org/10.1007/978-3-030-53291-8_20 |
| Doi | http://dx.doi.org/10.1007/978-3-030-53291-8_20 |
| Keywords | Replicated systems; population protocols |
| Description | 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. |
| Related projects: |