{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,3,30]],"date-time":"2022-03-30T20:28:06Z","timestamp":1648672086726},"reference-count":28,"publisher":"Springer Science and Business Media LLC","issue":"4","license":[{"start":{"date-parts":[[2018,3,15]],"date-time":"2018-03-15T00:00:00Z","timestamp":1521072000000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Front. Comput. Sci."],"published-print":{"date-parts":[[2018,8]]},"DOI":"10.1007\/s11704-018-6173-6","type":"journal-article","created":{"date-parts":[[2018,3,14]],"date-time":"2018-03-14T22:06:07Z","timestamp":1521065167000},"page":"763-776","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Probabilistic verification of hierarchical leader election protocol in dynamic systems"],"prefix":"10.1007","volume":"12","author":[{"given":"Yu","family":"Zhou","sequence":"first","affiliation":[]},{"given":"Nvqi","family":"Zhou","sequence":"additional","affiliation":[]},{"given":"Tingting","family":"Han","sequence":"additional","affiliation":[]},{"given":"Jiayi","family":"Gu","sequence":"additional","affiliation":[]},{"given":"Weigang","family":"Wu","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2018,3,15]]},"reference":[{"key":"6173_CR1","first-page":"127","volume-title":"Proceedings of European Dependable Computing Conference (EDCC)","author":"S Tucci-Piergiovanni","year":"2010","unstructured":"Tucci-Piergiovanni S, Baldoni R. Eventual leader election in infinite arrival message-passing system model with bounded concurrency. In: Proceedings of European Dependable Computing Conference (EDCC). 2010, 127\u2013134"},{"issue":"3","key":"6173_CR2","doi-asserted-by":"publisher","first-page":"231","DOI":"10.1109\/71.491576","volume":"7","author":"G Singh","year":"1996","unstructured":"Singh G. Leader election in the presence of link failures. IEEE Transactions on Parallel & Distributed Systems, 1996, 7(3): 231\u2013236","journal-title":"IEEE Transactions on Parallel & Distributed Systems"},{"key":"6173_CR3","first-page":"63","volume-title":"Proceedings of International Symposium on Parallel Architectures, Algorithms and Networks","author":"K Nakano","year":"2002","unstructured":"Nakano K, Olariu S. A survey on leader election protocols for radio networks. In: Proceedings of International Symposium on Parallel Architectures, Algorithms and Networks. 2002, 63\u201368"},{"key":"6173_CR4","doi-asserted-by":"publisher","first-page":"395","DOI":"10.1007\/11945529_28","volume-title":"Proceedings of the 10th International Conference on Principles of Distributed Systems","author":"M Fischer","year":"2006","unstructured":"Fischer M, Jiang H. Self-stabilizing leader election in networks of finite-state anonymous agents. In: Proceedings of the 10th International Conference on Principles of Distributed Systems. 2006, 395\u2013409"},{"key":"6173_CR5","first-page":"57","volume-title":"Proceedings of the 5th IFIP International Conference on Theoretical Computer Science\u2013Tcs","author":"R Bakhshi","year":"2008","unstructured":"Bakhshi R, Fokkink W, Pang J, Van De Pol J. Leader election in anonymous rings: Franklin goes probabilistic. In: Proceedings of the 5th IFIP International Conference on Theoretical Computer Science\u2013Tcs. 2008, 57\u201372"},{"key":"6173_CR6","doi-asserted-by":"crossref","first-page":"109","DOI":"10.1109\/RELDIS.2005.19","volume-title":"Proceedings of the 24th IEEE Symposium on Reliable Distributed Systems","author":"A Mostefaoui","year":"2005","unstructured":"Mostefaoui A, Raynal M, Travers C, Patterson S, Agrawal D, Abbadi A. From static distributed systems to dynamic systems. In: Proceedings of the 24th IEEE Symposium on Reliable Distributed Systems. 2005, 109\u2013118"},{"issue":"3","key":"6173_CR7","doi-asserted-by":"publisher","first-page":"204","DOI":"10.1504\/IJWGS.2012.049167","volume":"8","author":"M Larrea","year":"2012","unstructured":"Larrea M, Raynal M, Soraluze I, Corti\u00f1as R. Specifying and implementing an eventual leader service for dynamic systems. International Journal of Web and Grid Services. 2012, 8(3): 204\u2013224","journal-title":"International Journal of Web and Grid Services"},{"key":"6173_CR8","first-page":"78","volume-title":"Proceedings of the 19th Pacific Rim International Symposium on Dependable Computing","author":"C G\u00f3mez-Calzado","year":"2013","unstructured":"G\u00f3mez-Calzado C, Lafuente A, Larrea M, Raynal M. Fault-tolerant leader election in mobile dynamic distributed systems. In: Proceedings of the 19th Pacific Rim International Symposium on Dependable Computing. 2013, 78\u201387"},{"key":"6173_CR9","first-page":"338","volume-title":"Proceedings of International Conference on Algorithms and Architectures for Parallel Processing","author":"H G Li","year":"2014","unstructured":"Li H G, Wu W G, Zhou Y. Hierarchical eventual leader election for dynamic systems. In: Proceedings of International Conference on Algorithms and Architectures for Parallel Processing. 2014, 338\u2013351"},{"key":"6173_CR10","volume-title":"Cambridge: MIT Press","author":"C Baier","year":"2008","unstructured":"Baier C, Katoen J P. Principles of Model Checking. Cambridge: MIT Press. 2008."},{"key":"6173_CR11","first-page":"53","volume-title":"Formal Methods for the Design of Computer, Communication and Software Systems. Springer International Publishing","author":"V Forejt","year":"2011","unstructured":"Forejt V, Kwiatkowska M, Norman G, Parker D. Automated verification techniques for probabilistic systems. In: Bernardo M, Issarny V, eds. Formal Methods for the Design of Computer, Communication and Software Systems. Springer International Publishing, 2011, 53\u2013113"},{"key":"6173_CR12","first-page":"585","volume":"6806","author":"M Kwiatkowska","year":"2011","unstructured":"Kwiatkowska M, Norman G, Parker D. Prism 4. 0: verification of probabilistic real-time systems. Lecture Notes in Computer Science. 2011, 6806: 585\u2013591","journal-title":"0: verification of probabilistic real-time systems. Lecture Notes in Computer Science"},{"key":"6173_CR13","doi-asserted-by":"publisher","first-page":"192","DOI":"10.1007\/978-3-319-27051-7_17","volume-title":"Proceedings of International Conference on Cloud Computing and Security","author":"J Y Gu","year":"2015","unstructured":"Gu J Y, Zhou Y, Chen T L, Wu W G. Analyzing eventual leader election protocols for dynamic systems by probabilistic model checking. In: Proceedings of International Conference on Cloud Computing and Security. 2015, 192\u2013205"},{"issue":"6","key":"6173_CR14","doi-asserted-by":"publisher","first-page":"753","DOI":"10.1109\/TPDS.2008.266","volume":"20","author":"W G Wu","year":"2009","unstructured":"Wu W G, Cao J N, Raynal M. Eventual clusterer: a modular approach to designing hierarchical consensus protocols in manets. IEEE Transactions on Parallel and Distributed Systems. 2009, 20(6): 753\u2013765","journal-title":"IEEE Transactions on Parallel and Distributed Systems"},{"key":"6173_CR15","first-page":"603","volume-title":"Proceedings of the 42nd International Conference on Parallel Processing","author":"Z W Yang","year":"2013","unstructured":"Yang Z W, Wu WG, Chen Y S, Zhang J. Efficient information dissemination in dynamic networks. In: Proceedings of the 42nd International Conference on Parallel Processing. 2013, 603\u2013610"},{"key":"6173_CR16","first-page":"23","volume-title":"Proceedings of International Conference on Tools and Algorithms for the Construction and Analysis of Systems","author":"M Kwiatkowska","year":"2010","unstructured":"Kwiatkowska M, Norman G, Parker D, Qu H Y. Assume-guarantee verification for probabilistic systems. In: Proceedings of International Conference on Tools and Algorithms for the Construction and Analysis of Systems. 2010, 23\u201337"},{"key":"6173_CR17","doi-asserted-by":"publisher","first-page":"38","DOI":"10.1016\/j.ic.2013.10.001","volume":"232","author":"M Kwiatkowska","year":"2013","unstructured":"Kwiatkowska M, Norman G, Parker D, Qu H Y. Compositional probabilistic verification through multi-objective model checking. Information and Computation. 2013, 232: 38\u201365","journal-title":"Information and Computation"},{"issue":"1","key":"6173_CR18","first-page":"171","volume":"16","author":"J T H Shen","year":"2015","unstructured":"Shen J, Tan HW, Wang J, Wang J W, Lee S Y. A novel routing protocol providing good transmission reliability in underwater sensor networks. Journal of Internet Technology. 2015, 16(1): 171\u2013178","journal-title":"Journal of Internet Technology"},{"issue":"1","key":"6173_CR19","doi-asserted-by":"publisher","first-page":"231","DOI":"10.1007\/s11277-014-1748-5","volume":"78","author":"S D Xie","year":"2014","unstructured":"Xie S D, Wang Y X. Construction of tree network with limited delivery latency in homogeneous wireless sensor networks. Wireless Personal Communications. 2014, 78(1): 231\u2013246","journal-title":"Wireless Personal Communications"},{"key":"6173_CR20","doi-asserted-by":"publisher","first-page":"247","DOI":"10.1007\/978-3-642-13568-2_18","volume-title":"Proceedings of International Conference on Analytical and Stochastic Modeling Techniques and Applications","author":"H D Yue","year":"2010","unstructured":"Yue H D, Katoen J P. Leader election in anonymous radio networks: model checking energy consumption. In: Proceedings of International Conference on Analytical and Stochastic Modeling Techniques and Applications. 2010, 247\u2013261"},{"key":"6173_CR21","doi-asserted-by":"publisher","first-page":"104","DOI":"10.1016\/j.comnet.2014.03.027","volume":"67","author":"T Rault","year":"2014","unstructured":"Rault T, Bouabdallah A, Challal Y. Energy efficiency in wireless sensor networks: A top-down survey. Computer Networks. 2014, 67: 104\u2013122","journal-title":"Computer Networks"},{"key":"6173_CR22","doi-asserted-by":"crossref","first-page":"89","DOI":"10.1007\/3-540-40026-5_6","volume-title":"Proceedings of International Symposium on Distributed Computing","author":"I Gupta","year":"2000","unstructured":"Gupta I, Van Renesse R, Birman K P. A probabilistically correct leader election protocol for large groups. In: Proceedings of International Symposium on Distributed Computing. 2000, 89\u2013103"},{"issue":"10","key":"6173_CR23","doi-asserted-by":"publisher","first-page":"3726","DOI":"10.1007\/s11227-015-1460-6","volume":"71","author":"E Jim\u00e9nez","year":"2015","unstructured":"Jim\u00e9nez E, Ar\u00e9valo V E, Herrera C, Tang J. Eventual election of multiple leaders for solving consensus in anonymous systems. The Journal of Supercomputing. 2015, 71(10): 3726\u20133743","journal-title":"The Journal of Supercomputing"},{"key":"6173_CR24","doi-asserted-by":"publisher","first-page":"133","DOI":"10.1002\/9781118459898.ch7","volume-title":"Formal Methods for Industrial Critical Systems: A Survey of Applications. Wiley","author":"M Duflot","year":"2012","unstructured":"Duflot M, Kwiatkowska M, Norman G, Parker D, Peyronnet D, Picaronny C, Sproston J. Practical applications of probabilistic model checking to communication protocols. In: Gnesi S, Margaria T, eds. Formal Methods for Industrial Critical Systems: A Survey of Applications. Wiley, 2012, 133\u2013150"},{"key":"6173_CR25","doi-asserted-by":"publisher","first-page":"96","DOI":"10.1007\/978-3-319-06880-0_5","volume-title":"Horizons of the Mind. A Tribute to Prakash Panangaden. Springer International Publishing","author":"C Baier","year":"2014","unstructured":"Baier C, Dubslaff C, Klein J, Kl\u00fc ppelholz S, Wunderlich S. Probabilistic model checking for energy-utility analysis. In: van Breugel F, Kashefi E, Palamidessi C, et al, eds. Horizons of the Mind. A Tribute to Prakash Panangaden. Springer International Publishing, 2014, 96\u2013123"},{"key":"6173_CR26","first-page":"31","volume-title":"Proceedings of the 15th IEEE\/ACM International Symposium on Cluster, Cloud and Grid Computing","author":"A Naskos","year":"2015","unstructured":"Naskos A, Stachtiari E, Gounaris A, Katsaros P, Tsoumakos D, Konstantinou I, Sioutas S. Dependable horizontal scaling based on probabilistic model checking. In: Proceedings of the 15th IEEE\/ACM International Symposium on Cluster, Cloud and Grid Computing. 2015, 31\u201340"},{"key":"6173_CR27","first-page":"135","volume-title":"Proceedings of International Symposium on Theoretical Aspects of Software Engineering","author":"K L He","year":"2015","unstructured":"He K L, Zhang M, He J, Chen Y X. Probabilistic model checking of pipe protocol. In: Proceedings of International Symposium on Theoretical Aspects of Software Engineering. 2015, 135\u2013138"},{"key":"6173_CR28","doi-asserted-by":"publisher","first-page":"261","DOI":"10.1016\/j.entcs.2013.09.001","volume":"296","author":"F L Zhang","year":"2013","unstructured":"Zhang F L, Bu L, Wang L Z, Zhao J H, Chen X, Zhang T, Li X D. Modeling and evaluation of wireless sensor network protocols by stochastic timed automata. Electronic Notes in Theoretical Computer Science. 2013, 296: 261\u2013277","journal-title":"Electronic Notes in Theoretical Computer Science"}],"container-title":["Frontiers of Computer Science"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s11704-018-6173-6\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s11704-018-6173-6.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s11704-018-6173-6.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,3,14]],"date-time":"2019-03-14T21:00:50Z","timestamp":1552597250000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s11704-018-6173-6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018,3,15]]},"references-count":28,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2018,8]]}},"alternative-id":["6173"],"URL":"https:\/\/doi.org\/10.1007\/s11704-018-6173-6","relation":{},"ISSN":["2095-2228","2095-2236"],"issn-type":[{"value":"2095-2228","type":"print"},{"value":"2095-2236","type":"electronic"}],"subject":[],"published":{"date-parts":[[2018,3,15]]},"assertion":[{"value":"23 March 2016","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"10 July 2017","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"15 March 2018","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}