{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,31]],"date-time":"2025-05-31T04:10:58Z","timestamp":1748664658750,"version":"3.41.0"},"publisher-location":"Cham","reference-count":33,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319246437"},{"type":"electronic","value":"9783319246444"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"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":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-319-24644-4_5","type":"book-chapter","created":{"date-parts":[[2015,9,24]],"date-time":"2015-09-24T05:34:39Z","timestamp":1443072879000},"page":"69-83","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":8,"title":["Modeling and Efficient Verification of Broadcasting Actors"],"prefix":"10.1007","author":[{"given":"Behnaz","family":"Yousefi","sequence":"first","affiliation":[]},{"given":"Fatemeh","family":"Ghassemi","sequence":"additional","affiliation":[]},{"given":"Ramtin","family":"Khosravi","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2015,11,12]]},"reference":[{"key":"5_CR1","unstructured":"Rebeca formal modeling language, http:\/\/www.rebeca-lang.org\/wiki\/pmwiki.php\/Tools\/Afra"},{"key":"5_CR2","unstructured":"Agha, G.A.: ACTORS - a model of concurrent computation in distributed systems. MIT Press series in artificial intelligence. MIT Press (1990)"},{"key":"5_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"64","DOI":"10.1007\/978-3-642-02658-4_9","volume-title":"Computer Aided Verification","author":"G. Basler","year":"2009","unstructured":"Basler, G., Mazzucchi, M., Wahl, T., Kroening, D.: Symbolic counter abstraction for concurrent software. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol.\u00a05643, pp. 64\u201378. Springer, Heidelberg (2009)"},{"issue":"4","key":"5_CR4","doi-asserted-by":"publisher","first-page":"824","DOI":"10.1145\/4221.214134","volume":"32","author":"G. Bracha","year":"1985","unstructured":"Bracha, G., Toueg, S.: Asynchronous consensus and broadcast protocols. Journal of the ACM\u00a032(4), 824\u2013840 (1985)","journal-title":"Journal of the ACM"},{"key":"5_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"524","DOI":"10.1007\/3-540-44647-8_31","volume-title":"Advances in Cryptology - CRYPTO 2001","author":"C. Cachin","year":"2001","unstructured":"Cachin, C., Kursawe, K., Petzold, F., Shoup, V.: Secure and efficient asynchronous broadcast protocols. In: Kilian, J. (ed.) CRYPTO 2001. LNCS, vol.\u00a02139, pp. 524\u2013541. Springer, Heidelberg (2001)"},{"key":"5_CR6","doi-asserted-by":"crossref","unstructured":"Clarke, E.M., Emerson, E.A., Jha, S., Sistla, A.P.: Symmetry reductions in model checking. In: Computer Aided Verification, pp. 147\u2013158. Springer (1998)","DOI":"10.1007\/BFb0028741"},{"issue":"2","key":"5_CR7","doi-asserted-by":"publisher","first-page":"141","DOI":"10.1504\/IJCCBS.2011.041257","volume":"2","author":"M. Correia","year":"2011","unstructured":"Correia, M., Veronese, G.S., Neves, N.F., Ver\u00edssimo, P.: Byzantine consensus in asynchronous message-passing systems: a survey. IJCCBS\u00a02(2), 141\u2013161 (2011)","journal-title":"IJCCBS"},{"key":"5_CR8","doi-asserted-by":"crossref","unstructured":"Cui, T., Chen, L., Ho, T.: Distributed optimization in wireless networks using broadcast advantage. In: Decision and Control, pp. 5839\u20135844. IEEE (2007)","DOI":"10.1109\/CDC.2007.4434958"},{"issue":"3","key":"5_CR9","doi-asserted-by":"publisher","first-page":"210","DOI":"10.1109\/TC.1986.1676745","volume":"35","author":"R. Dechter","year":"1986","unstructured":"Dechter, R., Kleinrock, L.: Broadcast communications and distributed algorithms. Trans. Computers\u00a035(3), 210\u2013219 (1986)","journal-title":"Trans. Computers"},{"key":"5_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"142","DOI":"10.1007\/3-540-48153-2_12","volume-title":"Correct Hardware Design and Verification Methods","author":"E.A. Emerson","year":"1999","unstructured":"Emerson, E.A., Trefler, R.J.: From asymmetry to full symmetry: New techniques for symmetry reduction in model checking. In: Pierre, L., Kropf, T. (eds.) CHARME 1999. LNCS, vol.\u00a01703, pp. 142\u2013157. Springer, Heidelberg (1999)"},{"key":"5_CR11","doi-asserted-by":"crossref","unstructured":"Fill, J.A., Mahmoud, H.M., Szpankowski, W.: On the distribution for the duration of a randomized leader election algorithm. Ann. Appl. Probab., 1260\u20131283 (1996)","DOI":"10.1214\/aoap\/1035463332"},{"key":"5_CR12","doi-asserted-by":"crossref","unstructured":"Godefroid, P.: Partial-Order Methods for the Verification of Concurrent Systems. LNCS, vol.\u00a01032. Springer (1996)","DOI":"10.1007\/3-540-60761-7"},{"issue":"3","key":"5_CR13","doi-asserted-by":"publisher","first-page":"323","DOI":"10.1016\/0004-3702(77)90033-9","volume":"8","author":"C. Hewitt","year":"1977","unstructured":"Hewitt, C.: Viewing control structures as patterns of passing messages. Artif. Intell.\u00a08(3), 323\u2013364 (1977)","journal-title":"Artif. Intell."},{"issue":"1","key":"5_CR14","doi-asserted-by":"publisher","first-page":"33","DOI":"10.1007\/s00236-009-0111-x","volume":"47","author":"M.M. Jaghoori","year":"2010","unstructured":"Jaghoori, M.M., Sirjani, M., Mousavi, M.R., Khamespanah, E., Movaghar, A.: Symmetry and partial order reduction techniques in model checking Rebeca. Acta Informatica\u00a047(1), 33\u201366 (2010)","journal-title":"Acta Informatica"},{"key":"5_CR15","doi-asserted-by":"crossref","unstructured":"Katoen, J.: Model checking: One can do much more than you think? In: Fundamentals of Software Engineering, pp. 1\u201314. Springer (2011)","DOI":"10.1007\/978-3-642-29320-7_1"},{"issue":"3","key":"5_CR16","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., Arriola, I.S., Corti\u00f1as, R.: Specifying and implementing an eventual leader service for dynamic systems. IJWGS\u00a08(3), 204\u2013224 (2012)","journal-title":"IJWGS"},{"key":"5_CR17","doi-asserted-by":"crossref","unstructured":"Levitan, S.P., Foster, C.C.: Finding an extremum in a network. In: 9th International Symposium on Computer Architecture, pp. 321\u2013325. ACM (1982)","DOI":"10.1145\/1067649.801741"},{"issue":"1","key":"5_CR18","doi-asserted-by":"publisher","first-page":"7","DOI":"10.1016\/0020-0190(94)90133-3","volume":"52","author":"C.U. Martel","year":"1994","unstructured":"Martel, C.U.: Maximum finding on a multiple access broadcast network. Inf. Process. Lett.\u00a052(1), 7\u201315 (1994)","journal-title":"Inf. Process. Lett."},{"key":"5_CR19","doi-asserted-by":"crossref","unstructured":"McMillan, K.L.: Symbolic model checking. Kluwer (1993)","DOI":"10.1007\/978-1-4615-3190-6"},{"issue":"1","key":"5_CR20","doi-asserted-by":"publisher","first-page":"17","DOI":"10.1109\/71.80121","volume":"1","author":"P.M. Melliar-Smith","year":"1990","unstructured":"Melliar-Smith, P.M., Moser, L.E., Agrawala, V.: Broadcast protocols for distributed systems. Trans. Parallel Distrib. Syst.\u00a01(1), 17\u201325 (1990)","journal-title":"Trans. Parallel Distrib. Syst."},{"key":"5_CR21","doi-asserted-by":"crossref","unstructured":"Most\u00e9faoui, A., Raynal, M., Travers, C.: Crash-resilient time-free eventual leadership. In: 23rd International Symposium on Reliable Distributed Systems, pp. 208\u2013217. IEEE Computer Society (2004)","DOI":"10.1109\/RELDIS.2004.1353022"},{"issue":"2","key":"5_CR22","doi-asserted-by":"publisher","first-page":"222","DOI":"10.1007\/s00224-007-9006-9","volume":"42","author":"M. Okun","year":"2008","unstructured":"Okun, M., Barak, A.: Efficient algorithms for anonymous byzantine agreement. Theory Comput. Syst.\u00a042(2), 222\u2013238 (2008)","journal-title":"Theory Comput. Syst."},{"key":"5_CR23","doi-asserted-by":"crossref","unstructured":"Ostrovsky, R., Rajagopalan, S., Vazirani, U.V.: Simple and efficient leader election in the full information model. In: Proceedings of the Twenty-Sixth Annual ACM Symposium on Theory of Computing, pp. 234\u2013242. ACM (1994)","DOI":"10.1145\/195058.195141"},{"key":"5_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1007\/3-540-45657-0_9","volume-title":"Computer Aided Verification","author":"A. Pnueli","year":"2002","unstructured":"Pnueli, A., Xu, J., Zuck, L.D.: Liveness with (0, 1, infty)-Counter Abstraction. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol.\u00a02404, pp. 107\u2013122. Springer, Heidelberg (2002)"},{"key":"5_CR25","doi-asserted-by":"publisher","first-page":"41","DOI":"10.1016\/j.scico.2014.01.008","volume":"89","author":"A.H. Reynisson","year":"2014","unstructured":"Reynisson, A.H., Sirjani, M., Aceto, L., Cimini, M., Jafari, A., Ing\u00f3lfsd\u00f3ttir, A., Sigurdarson, S.H.: Modelling and simulation of asynchronous real-time systems using Timed Rebeca. Sci. Comput. Program.\u00a089, 41\u201368 (2014)","journal-title":"Sci. Comput. Program."},{"key":"5_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"51","DOI":"10.1007\/978-3-642-40213-5_4","volume-title":"Fundamentals of Software Engineering","author":"H. Sabouri","year":"2013","unstructured":"Sabouri, H., Khosravi, R.: Delta modeling and model checking of product families. In: Arbab, F., Sirjani, M. (eds.) FSEN 2013. LNCS, vol.\u00a08161, pp. 51\u201365. Springer, Heidelberg (2013)"},{"key":"5_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"472","DOI":"10.1007\/BFb0030868","volume-title":"Computing and Combinatorics","author":"S. Shiau","year":"1995","unstructured":"Shiau, S., Yang, C.: A fast maximum finding algorithm on broadcast communication. In: Li, M., Du, D.-Z. (eds.) COCOON 1995. LNCS, vol.\u00a0959, pp. 472\u2013481. Springer, Heidelberg (1995)"},{"key":"5_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"252","DOI":"10.1007\/3-540-44968-X_25","volume-title":"Computing and Combinatorics","author":"S. Shiau","year":"2000","unstructured":"Shiau, S., Yang, C.: A fast sorting algorithm and its generalization on broadcast communications. In: Du, D.-Z., Eades, P., Sharma, A.K., Lin, X., Estivill-Castro, V. (eds.) COCOON 2000. LNCS, vol.\u00a01858, pp. 252\u2013261. Springer, Heidelberg (2000)"},{"key":"5_CR29","doi-asserted-by":"crossref","unstructured":"Sirjani, M., de Boer, F.S., Movaghar, A., Shali, A.: Extended Rebeca: A component-based actor language with synchronous message passing. In: Fifth International Conference on Application of Concurrency to System Design, pp. 212\u2013221. IEEE Computer Society (2005)","DOI":"10.1109\/ACSD.2005.12"},{"key":"5_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"20","DOI":"10.1007\/978-3-642-24933-4_3","volume-title":"Formal Modeling: Actors, Open Systems, Biological Systems","author":"M. Sirjani","year":"2011","unstructured":"Sirjani, M., Jaghoori, M.M.: Ten years of analyzing actors: Rebeca experience. In: Agha, G., Danvy, O., Meseguer, J. (eds.) Formal Modeling: Actors, Open Systems, Biological Systems. LNCS, vol.\u00a07000, pp. 20\u201356. Springer, Heidelberg (2011)"},{"issue":"4","key":"5_CR31","doi-asserted-by":"crossref","first-page":"385","DOI":"10.3233\/FUN-2004-63405","volume":"63","author":"M. Sirjani","year":"2004","unstructured":"Sirjani, M., Movaghar, A., Shali, A., de Boer, F.S.: Modeling and verification of reactive systems using Rebeca. Fundam. Inform.\u00a063(4), 385\u2013410 (2004)","journal-title":"Fundam. Inform."},{"key":"5_CR32","doi-asserted-by":"crossref","unstructured":"Sirjani, M., Shali, A., Jaghoori, M.M., Iravanchi, H., Movaghar, A.: A front-end tool for automated abstraction and modular verification of actor-based models. In: 4th International Conference on Application of Concurrency to System Design, pp. 145\u2013150. IEEE Computer Society (2004)","DOI":"10.1109\/CSD.2004.1309125"},{"key":"5_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"135","DOI":"10.1007\/978-3-642-34281-3_12","volume-title":"Formal Methods and Software Engineering","author":"M. Varshosaz","year":"2012","unstructured":"Varshosaz, M., Khosravi, R.: Modeling and verification of probabilistic actor systems using pRebeca. In: Aoki, T., Taguchi, K. (eds.) ICFEM 2012. LNCS, vol.\u00a07635, pp. 135\u2013150. Springer, Heidelberg (2012)"}],"container-title":["Lecture Notes in Computer Science","Fundamentals of Software Engineering"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-24644-4_5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,30]],"date-time":"2025-05-30T19:53:11Z","timestamp":1748634791000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-24644-4_5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783319246437","9783319246444"],"references-count":33,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-24644-4_5","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2015]]},"assertion":[{"value":"12 November 2015","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}