In this work, we study the Population Protocol model of Angluin et al. from the perspective of protocol verification. In particular, we are interested in algorithmically solving the problem of determining whether a given population protocol conforms to its specifications. Since this is the first work on verification of population protocols, we redefine most notions of population protocols in order to make them suitable for algorithmic verification. Moreover, we formally define the general verification problem and some interesting special cases. All these problems are shown to be NP-hard. We next propose some first algorithmic solutions for a natural special case. Finally, we conduct experiments and algorithmic engineering in order to improve our verifiers' running times.
Algorithmic verification of population protocols / Chatzigiannakis, Ioannis; Michail, O.; Spirakis, P. G.. - STAMPA. - 6366 LNCS:(2010), pp. 221-235. (Intervento presentato al convegno 12th International Symposium on Stabilization, Safety, and Security of Distributed Systems tenutosi a New York; USA) [10.1007/978-3-642-16023-3_19].
Algorithmic verification of population protocols
CHATZIGIANNAKIS, IOANNIS;
2010
Abstract
In this work, we study the Population Protocol model of Angluin et al. from the perspective of protocol verification. In particular, we are interested in algorithmically solving the problem of determining whether a given population protocol conforms to its specifications. Since this is the first work on verification of population protocols, we redefine most notions of population protocols in order to make them suitable for algorithmic verification. Moreover, we formally define the general verification problem and some interesting special cases. All these problems are shown to be NP-hard. We next propose some first algorithmic solutions for a natural special case. Finally, we conduct experiments and algorithmic engineering in order to improve our verifiers' running times.File | Dimensione | Formato | |
---|---|---|---|
Chatzigiannakis_Algorithmic_2010.pdf
solo gestori archivio
Tipologia:
Documento in Post-print (versione successiva alla peer review e accettata per la pubblicazione)
Licenza:
Tutti i diritti riservati (All rights reserved)
Dimensione
173.27 kB
Formato
Adobe PDF
|
173.27 kB | Adobe PDF | Contatta l'autore |
VE_2010_11573-914464.pdf
solo gestori archivio
Tipologia:
Versione editoriale (versione pubblicata con il layout dell'editore)
Licenza:
Tutti i diritti riservati (All rights reserved)
Dimensione
170.06 kB
Formato
Adobe PDF
|
170.06 kB | Adobe PDF | Contatta l'autore |
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.