×

zbMATH — the first resource for mathematics

Verification of population protocols. (English) Zbl 1364.68081
Summary: Population protocols [D. Angluin et al., in: Proceedings of the 23rd annual ACM symposium on principles of distributed computing, PODC’04. New York, NY: Association for Computing Machinery (ACM). 290–299 (2004; Zbl 1321.68058)] are a formal model of sensor networks consisting of identical mobile devices. Two devices can interact and thereby change their states. Computations are infinite sequences of interactions satisfying a strong fairness constraint. A population protocol is well specified if for every initial configuration \(C\) of devices, and every computation starting at \(C\), all devices eventually agree on a consensus value depending only on \(C\). If a protocol is well specified, then it is said to compute the predicate that assigns to each initial configuration its consensus value. While the computational power of well-specified protocols has been extensively studied, the two basic verification problems remain open: Is a given protocol well specified? Does a given protocol compute a given predicate? We prove that both problems are decidable by reduction to the reachability problem of Petri nets. We also give a new proof of the fact that the predicates computed by well-defined protocols are those definable in Presburger arithmetic [D. Angluin et al., in: Proceedings of the 25th annual ACM symposium on principles of distributed computing, PODC’06. New York, NY: Association for Computing Machinery (ACM). 292–299 (2006; Zbl 1314.68054)].

MSC:
68M12 Network protocols
03B70 Logic in computer science
68Q60 Specification and verification (program logics, model checking, etc.)
Software:
Coq; PAT
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Abdulla, P.A., Cerans, K., Jonsson, B., Tsay, Y.-K.: General decidability theorems for infinite-state systems. In: LICS’96: Proceedings of the 11th Annual IEEE Symposium on Logic in Computer Science, pp. 313-321. IEEE Computer Society (1996)
[2] Angluin, D., Aspnes, J., Diamadi, Z., Fischer, M.J., Peralta, R.: Computation in networks of passively mobile finite-state sensors. In: PODC’04, pp. 290-299. ACM (2004) · Zbl 1321.68058
[3] Angluin, D; Aspnes, J; Diamadi, Z; Fischer, MJ; Peralta, R, Computation in networks of passively mobile finite-state sensors, Distrib. Comput., 18, 235-253, (2006) · Zbl 1266.68042
[4] Angluin, D., Aspnes, J., Eisenstat, D.: Fast computation by population protocols with a leader. In: DISC’06, Volume 4167 of LNCS, pp. 61-75. Springer, Berlin (2006) · Zbl 1155.68389
[5] Angluin, D., Aspnes, J., Eisenstat, D.: Stably computable predicates are semilinear. In: PODC’06, pp. 292-299. ACM (2006) · Zbl 1314.68054
[6] Angluin, D; Aspnes, J; Eisenstat, D, Fast computation by population protocols with a leader, Distrib. Comput., 21, 183-199, (2008) · Zbl 1267.68306
[7] Angluin, D; Aspnes, J; Eisenstat, D; Ruppert, E, The computational power of population protocols, Distrib. Comput., 20, 279-304, (2007) · Zbl 1266.68043
[8] Apt, KR; Kozen, DC, Limits for automatic verification of finite-state concurrent systems, Inf. Process. Lett., 22, 307-309, (1986)
[9] Bouziane, Z; Finkel, A, Cyclic Petri net reachability sets are semi-linear effectively constructible, Electron. Notes Theor. Comput. Sci., 9, 15-24, (1997) · Zbl 0907.68131
[10] Chatzigiannakis, I., Michail, O., Spirakis, P.G.: Algorithmic verification of population protocols. In: SSS’10, Volume 6366 of LNCS, pp. 221-235. Springer, Berlin (2010)
[11] Clement, J., Delporte-Gallet, C., Fauconnier, H., Sighireanu, M.: Guidelines for the verification of population protocols. In: ICDCS’11, pp. 215-224 (2011) · Zbl 0206.02703
[12] Deng, Y., Monin, J.: Verifying self-stabilizing population protocols with coq. In: TASE’09, pp. 201-208. IEEE Computer Society (2009)
[13] Diamadi, Z; Fischer, MJ, A simple game for the study of trust in distributed systems, Wuhan Univ. J. Nat. Sci., 6, 72-82, (2001)
[14] Eilenberg, S; Schützenberger, MP, Rational sets in commutative monoids, J. Algebra, 13, 173-191, (1969) · Zbl 0206.02703
[15] Enderton, H.B.: A Mathematical Introduction to Logic. Academic Press, San Diego (2001) · Zbl 0992.03001
[16] Finkel, A., Leroux, J.: How to compose presburger-accelerations: Applications to broadcast protocols. In: FST TCS’02, Volume 2556 of Lecture Notes in Computer Science, pp. 145-156. Springer, Berlin (2002) · Zbl 1027.68616
[17] Finkel, A; Schnoebelen, P, Well-structured transition systems everywhere!, Theor. Comput. Sci., 256, 63-92, (2001) · Zbl 0973.68170
[18] Fribourg, L., Olsén, H.: Reductions of petri nets and unfolding of propositional logic programs. In: LOPSTR’96, Volume 1207 of Lecture Notes in Computer Science, pp. 187-203. Springer, Berlin (1996) · Zbl 0907.68131
[19] Ginsburg, S; Spanier, EH, Semigroups, Presburger formulas, and languages, Pac. J. Math., 16, 285-296, (1966) · Zbl 0143.01602
[20] Hack, M.H.T.: Decidability questions for Petri nets. Technical Report 161, MIT (1976) · Zbl 1266.68043
[21] Hirshfeld, Y.: Congruences in Commutative Semigroups. LFCS, Department of Computer Science, University of Edinburgh, Edinburgh (1994)
[22] Leroux, J.: The general vector addition system reachability problem by Presburger inductive invariants. In: LICS’09, pp. 4-13. IEEE Computer Society (2009)
[23] Leroux, J.: Vector addition system reversible reachability problem. In: CONCUR’11, Volume 6901 of LNCS, pp. 327-341. Springer, Berlin (2011) · Zbl 1343.68173
[24] Leroux, J.: Vector addition systems reachability problem (a simpler solution). In: Turing-100: The Alan Turing Centenary Conference, Volume 10 of EPiC Series, pp. 214-228. EasyChair (2012) · Zbl 0907.68131
[25] Leroux, J.: Presburger vector addition systems. In: LICS’13, pp. 23-32. IEEE Computer Society (2013) · Zbl 1366.68209
[26] Leroux, J.: Vector addition system reversible reachability problem. Log. Methods Comput. Sci. 9(1) (2013) · Zbl 1260.68271
[27] Leroux, J., Schmitz, S.: Demystifying reachability in vector addition systems. In: LICS’15, pp. 56-67. IEEE Computer Society (2015) · Zbl 1392.68308
[28] Leroux, J., Sutre, G.: Flat counter automata almost everywhere!. In: Peled, D.A., Tsay, Y. (eds.), Automated Technology for Verification and Analysis, Third International Symposium, ATVA 2005, Taipei, Taiwan, October 4-7, 2005, Proceedings, Volume 3707 of Lecture Notes in Computer Science, pp. 489-503. Springer, Berlin (2005) · Zbl 1170.68519
[29] Lipton, R.: The Reachability Problem is Exponential-Space Hard. Technical Report 62, Department of Computer Science, Yale University (1976)
[30] Mayr, E.W.: An algorithm for the general petri net reachability problem. In: STOC’81, pp. 238-246. ACM (1981) · Zbl 1267.68306
[31] Navlakha, S; Bar-Joseph, Z, Distributed information processing in biological and computational systems, Commun. ACM, 58, 94-102, (2014)
[32] Pang, J., Luo, Z., Deng, Y.: On automatic verification of self-stabilizing population protocols. In: TASE’08, pp. 185-192. IEEE Computer Society (2008)
[33] Sun, J., Liu, Y., Dong, J.S., Pang, J.: PAT: towards flexible verification under fairness. In: CAV’09, Volume 5643 of LNCS, pp. 709-714. Springer, Berlin (2009)
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.