More Web Proxy on the site http://driver.im/

Article

Algorithmic verification of population protocols

Authors:

Ioannis Chatzigiannakis,

Paul G. SpirakisAuthors Info & Claims

SSS'10: Proceedings of the 12th international conference on Stabilization, safety, and security of distributed systems

Pages 221 - 235

Published: 20 September 2010 Publication History

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.

References

[1]

Angluin, D., Aspnes, J., Diamadi, Z., Fischer, M.J., Peralta, R.: Computation in networks of passively mobile finite-state sensors. Distributed Computing 18(4), 235-253 (2006); Also in 23rd Annual ACM Symposium on Principles of Distributed Computing (PODC), pp. 290-299 (2004).

Digital Library

[2]

Angluin, D., Aspnes, J., Eisenstat, D., Ruppert, E.: The computational power of population protocols. Distributed Computing 20(4), 279-304 (2007).

[3]

Aspnes, J., Ruppert, E.: An introduction to population protocols. Bulletin of the European Association for Theoretical Computer Science 93, 98-117 (2007).

[4]

Bakhshi, R., Bonnet, F., Fokkink, W., Haverkort, B.: Formal analysis techniques for gossiping protocols. ACM SIGOPS Operating Systems Review, Special Issue on Gossip-Based Networking 41(5), 28-36 (2007).

Digital Library

[5]

Beauquier, J., Clement, J., Messika, S., Rosaz, L., Rozoy, B.: Self-stabilizing counting in mobile sensor networks. Technical Report 1470, LRI, Université Paris-Sud 11 (2007).

[6]

Behrmann, G., David, A., Larsen, K.G.: A tutorial on Uppaal. In: Bernardo, M., Corradini, F. (eds.) SFM-RT 2004. LNCS, vol. 3185, pp. 200-236. Springer, Heidelberg (2004).

[7]

Bournez, O., Chassaing, P., Cohen, J., Gerin, L., Koegler, X.: On the convergence of population protocols when population goes to infinity. Applied Mathematics and Computation 215(4), 1340-1350 (2009).

[8]

http://people.sc.fsu.edu/~burkardt/f_src/combo/combo.f90

[9]

Chatzigiannakis, I., Dolev, S., Fekete, S.P., Michail, O., Spirakis, P.G.: Not all fair probabilistic schedulers are equivalent. In: 13th International Conference on Principles of DIstributed Systems (OPODIS), pp. 33-47 (2009).

Digital Library

[10]

Chatzigiannakis, I., Michail, O., Spirakis, P.G.: Brief Announcement: Decidable graph languages by mediated population protocols. In: Keidar, I. (ed.) DISC 2009. LNCS, vol. 5805, pp. 239-240. Springer, Heidelberg (2009).

Digital Library

[11]

Chatzigiannakis, I., Michail, O., Spirakis, P.G.: Mediated population protocols. In: Albers, S., Marchetti-Spaccamela, A., Matias, Y., Nikoletseas, S., Thomas, W. (eds.) ICALP 2009. LNCS, vol. 5556, pp. 363-374. Springer, Heidelberg (2009).

Digital Library

[12]

Chatzigiannakis, I., Michail, O., Spirakis, P.G.: Recent advances in population protocols. In: Královič, R., Niwinski, D. (eds.) MFCS 2009. LNCS, vol. 5734, pp. 56-76. Springer, Heidelberg (2009).

Digital Library

[13]

Chatzigiannakis, I., Spirakis, P.G.: The dynamics of probabilistic population protocols. In: Taubenfeld, G. (ed.) DISC 2008. LNCS, vol. 5218, pp. 498-499. Springer, Heidelberg (2008).

Digital Library

[14]

Clarke, E.M., Grumberg, O., Peled, D.A.: Model checking. MIT Press, Cambridge (2000).

[15]

Fenichel, R.: Distribution of indistinguishable objects into distinguishable slots. Communications of the ACM 11(6), 430 (1968).

Digital Library

[16]

Guerraoui, R., Ruppert, E.: Names trump malice: Tiny mobile agents can tolerate byzantine failures. In: Albers, S., Marchetti-Spaccamela, A., Matias, Y., Nikoletseas, S., Thomas, W. (eds.) ICALP 2009. LNCS, vol. 5556, pp. 484-495. Springer, Heidelberg (2009).

Digital Library

[17]

Hinton, A., Kwiatkowska, M.Z., Norman, G., Parker, D.: Prism: A tool for automatic verification of probabilistic systems. In: Hermanns, H., Palsberg, J. (eds.) TACAS 2006. LNCS, vol. 3920, pp. 441-444. Springer, Heidelberg (2006).

Digital Library

[18]

Holzmann, G.: The Spin model checker, primer and reference manual. Addison-Wesley, Reading (2003).

Digital Library

[19]

Huth, M., Ryan, M.: Logic in Computer Science: Modelling and reasoning about systems. Cambridge University Press, Cambridge (2004).

Digital Library

[20]

Olveczky, P.C., Thorvaldsen, S.: Formal modeling and analysis of wireless sensor network algorithms in Real-Time Maude. In: Proceedings 20th IEEE International Parallel & Distributed Processing Symposium International, p. 157 (2006).

Digital Library

[21]

Tarjan, R.: Depth-first search and linear graph algorithms. SIAM Journal on Computing 1(2), 146-160 (1972).

Cited By

Blondin MEsparza JJaax SKučera A(2018)Black Ninjas in the DarkProceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science10.1145/3209108.3209110(1-10)Online publication date: 9-Jul-2018
https://dl.acm.org/doi/10.1145/3209108.3209110
Bérard BLafourcade PMillet LPotop-Butucaru MThierry-Mieg YTixeuil S(2016)Formal verification of mobile robot protocolsDistributed Computing10.1007/s00446-016-0271-129:6(459-487)Online publication date: 1-Nov-2016
https://dl.acm.org/doi/10.1007/s00446-016-0271-1
Elberfeld MSegev DDavidson CSilverbush DSharan R(2013)Approximation algorithms for orienting mixed graphsTheoretical Computer Science10.1016/j.tcs.2012.03.044483(96-103)Online publication date: 1-Apr-2013
https://dl.acm.org/doi/10.1016/j.tcs.2012.03.044
Show More Cited By

Recommendations

Verification of Population Ring Protocols in PAT
TASE '09: Proceedings of the 2009 Third IEEE International Symposium on Theoretical Aspects of Software Engineering

The population protocol model has emerged as an elegant paradigm for describing mobile ad hoc networks, consisting of a number of nodes that interact with each other to carry out a computation. One essential property of self-stabilizing population ...
Towards Efficient Verification of Population Protocols
PODC '17: Proceedings of the ACM Symposium on Principles of Distributed Computing

Population protocols are a well established model of computation by anonymous, identical finite state agents. A protocol is well-specified if from every initial configuration, all fair executions of the protocol reach a common consensus. The central ...
Towards efficient verification of population protocols
Abstract
Population protocols are a well established model of computation by anonymous, identical finite-state agents. A protocol is well-specified if from every initial configuration, all fair executions of the protocol reach a common consensus. The ... $^{}$ $^{}$ $^{}$

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Guide Proceedings

SSS'10: Proceedings of the 12th international conference on Stabilization, safety, and security of distributed systems

September 2010

602 pages

ISBN:3642160220

Editors:
Shlomi Dolev
Ben-Gurion University of the Negev, Department of Computer Science, Beer-Sheva, Israel
,
Jorge Cobb
The University of Texas at Dallas, Department of Computer Science, Richardson, TX
,
Michael Fischer
Yale University, Department of Computer Science, New Haven, CT
,
Moti Yung
Columbia University, Department of Computer Science, NewYork, NY

Publisher

Springer-Verlag

Berlin, Heidelberg

Publication History

Published: 20 September 2010

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

19
Total Citations
View Citations
0
Total Downloads

Downloads (Last 12 months)0
Downloads (Last 6 weeks)0

Reflects downloads up to 04 Jan 2025

Other Metrics

View Author Metrics

Citations

Cited By

Blondin MEsparza JJaax SKučera A(2018)Black Ninjas in the DarkProceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science10.1145/3209108.3209110(1-10)Online publication date: 9-Jul-2018
https://dl.acm.org/doi/10.1145/3209108.3209110
Bérard BLafourcade PMillet LPotop-Butucaru MThierry-Mieg YTixeuil S(2016)Formal verification of mobile robot protocolsDistributed Computing10.1007/s00446-016-0271-129:6(459-487)Online publication date: 1-Nov-2016
https://dl.acm.org/doi/10.1007/s00446-016-0271-1
Elberfeld MSegev DDavidson CSilverbush DSharan R(2013)Approximation algorithms for orienting mixed graphsTheoretical Computer Science10.1016/j.tcs.2012.03.044483(96-103)Online publication date: 1-Apr-2013
https://dl.acm.org/doi/10.1016/j.tcs.2012.03.044
Calegari DSzasz N(2013)Verification of Model TransformationsElectronic Notes in Theoretical Computer Science (ENTCS)10.1016/j.entcs.2013.02.002292(5-25)Online publication date: 1-Mar-2013
https://dl.acm.org/doi/10.1016/j.entcs.2013.02.002
Shokripour AOthman MIbrahim HSubramaniam S(2012)New method for scheduling heterogeneous multi-installment systemsFuture Generation Computer Systems10.1016/j.future.2012.03.00828:8(1205-1216)Online publication date: 1-Oct-2012
https://dl.acm.org/doi/10.1016/j.future.2012.03.008
Bournez OFraigniaud PKoegler X(2012)Computing with large populations using interactionsProceedings of the 37th international conference on Mathematical Foundations of Computer Science10.1007/978-3-642-32589-2_23(234-246)Online publication date: 27-Aug-2012
https://dl.acm.org/doi/10.1007/978-3-642-32589-2_23
Michail OChatzigiannakis ISpirakis P(2011)Mediated population protocolsTheoretical Computer Science10.1016/j.tcs.2011.02.003412:22(2434-2450)Online publication date: 1-May-2011
https://dl.acm.org/doi/10.1016/j.tcs.2011.02.003
Krause CMaraikar ZLazovik AArbab F(2011)Modeling dynamic reconfigurations in Reo using high-level replacement systemsScience of Computer Programming10.1016/j.scico.2009.10.00676:1(23-36)Online publication date: 1-Jan-2011
https://dl.acm.org/doi/10.1016/j.scico.2009.10.006
Do T(2011)An initiative for a classified bibliography on G-networksPerformance Evaluation10.1016/j.peva.2010.10.00168:4(385-394)Online publication date: 1-Apr-2011
https://dl.acm.org/doi/10.1016/j.peva.2010.10.001
Ketema JSimonsen J(2011)Infinitary Combinatory Reduction SystemsInformation and Computation10.1016/j.ic.2011.01.007209:6(893-926)Online publication date: 1-Jun-2011
https://dl.acm.org/doi/10.1016/j.ic.2011.01.007
Show More Cited By

View Options

View options

Media

Figures

Other

Tables

View Table of Contents