Termination complexity of Parameterized Population Protocols

Population protocols form a model where identical finite-state agents interact to collectively decide whether their initial configuration, given by the initial number of agents in each state, satisfies a given property, e.g., . A protocol is correct if the agents correctly decide the property for all of the infinitely many initial configurations. This makes automatic formal analysis challenging. Furthermore, the literature often describes \emph{parameterized families} of protocols, e.g., a family of protocols for the predicates . We describe a methodology for the automatic analysis of asymptotic running time of such families, based on abstraction techniques, and report on an implementation on top of a constraint-solver. Our results show that it is possible to check properties of \emph{infinitely many} protocols in finite time. The presentation is based on recent unpublished results achieved jointly with Michael Blondin, Javier Esparza, Stefan Jaax, and Philipp J. Meyer.

Authors

• Antonin Kucera.

Keywords

No keywords are indexed for this paper.