{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,23]],"date-time":"2025-06-23T09:27:41Z","timestamp":1750670861342,"version":"3.41.0"},"publisher-location":"Berlin, Heidelberg","reference-count":29,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783662545768"},{"type":"electronic","value":"9783662545775"}],"license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2017]]},"DOI":"10.1007\/978-3-662-54577-5_2","type":"book-chapter","created":{"date-parts":[[2017,3,30]],"date-time":"2017-03-30T10:48:06Z","timestamp":1490870886000},"page":"23-40","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["An Abstraction Technique for Parameterized Model Checking of Leader Election Protocols: Application to FTSP"],"prefix":"10.1007","author":[{"given":"Ocan","family":"Sankur","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jean-Pierre","family":"Talpin","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2017,3,31]]},"reference":[{"issue":"2","key":"2_CR1","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1016\/0304-3975(94)90010-8","volume":"126","author":"R Alur","year":"1994","unstructured":"Alur, R., Dill, D.L.: A theory of timed automata. Theoret. Comput. Sci. 126(2), 183\u2013235 (1994)","journal-title":"Theoret. Comput. Sci."},{"issue":"6","key":"2_CR2","doi-asserted-by":"publisher","first-page":"307","DOI":"10.1016\/0020-0190(86)90071-2","volume":"22","author":"KR Apt","year":"1986","unstructured":"Apt, K.R., Kozen, D.C.: Limits for automatic verification of finite-state concurrent systems. Inf. Process. Lett. 22(6), 307\u2013309 (1986)","journal-title":"Inf. Process. Lett."},{"key":"2_CR3","volume-title":"Principles of Model Checking","author":"C Baier","year":"2008","unstructured":"Baier, C., Katoen, J.-P.: Principles of Model Checking. MIT press, Cambridge (2008)"},{"issue":"5","key":"2_CR4","doi-asserted-by":"publisher","first-page":"28","DOI":"10.1145\/1317379.1317385","volume":"41","author":"R Bakhshi","year":"2007","unstructured":"Bakhshi, R., Bonnet, F., Fokkink, W., Haverkort, B.: Formal analysis techniques for gossiping protocols. ACM SIGOPS Oper. Syst. Rev. 41(5), 28\u201336 (2007)","journal-title":"ACM SIGOPS Oper. Syst. Rev."},{"key":"2_CR5","doi-asserted-by":"crossref","unstructured":"Bingham, J.: Automatic non-interference lemmas for parameterized model checking. In: Proceedings of the 2008 International Conference on Formal Methods in Computer-Aided Design, FMCAD 2008, Piscataway, NJ, USA, pp. 11:1\u201311:8. IEEE Press (2008)","DOI":"10.1109\/FMCAD.2008.ECP.15"},{"issue":"5","key":"2_CR6","doi-asserted-by":"publisher","first-page":"281","DOI":"10.1145\/359104.359108","volume":"22","author":"E Chang","year":"1979","unstructured":"Chang, E., Roberts, R.: An improved algorithm for decentralized extrema-finding in circular configurations of processes. Commun. ACM 22(5), 281\u2013283 (1979)","journal-title":"Commun. ACM"},{"key":"2_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"382","DOI":"10.1007\/978-3-540-30494-4_27","volume-title":"Formal Methods in Computer-Aided Design","author":"C-T Chou","year":"2004","unstructured":"Chou, C.-T., Mannava, P.K., Park, S.: A simple method for parameterized verification of cache coherence protocols. In: Hu, A.J., Martin, A.K. (eds.) FMCAD 2004. LNCS, vol. 3312, pp. 382\u2013398. Springer, Heidelberg (2004). doi:10.1007\/978-3-540-30494-4_27"},{"key":"2_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"33","DOI":"10.1007\/978-3-540-78800-3_4","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"E Clarke","year":"2008","unstructured":"Clarke, E., Talupur, M., Veith, H.: Proving ptolemy right: the environment abstraction framework for model checking concurrent systems. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 33\u201347. Springer, Heidelberg (2008). doi:10.1007\/978-3-540-78800-3_4"},{"issue":"5","key":"2_CR9","doi-asserted-by":"publisher","first-page":"1512","DOI":"10.1145\/186025.186051","volume":"16","author":"EM Clarke","year":"1994","unstructured":"Clarke, E.M., Grumberg, O., Long, D.E.: Model checking and abstraction. ACM Trans. Program. Lang. Syst. (TOPLAS) 16(5), 1512\u20131542 (1994)","journal-title":"ACM Trans. Program. Lang. Syst. (TOPLAS)"},{"key":"2_CR10","volume-title":"Model Checking","author":"EM Clarke Jr","year":"1999","unstructured":"Clarke Jr., E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, Cambridge (1999)"},{"key":"2_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"109","DOI":"10.1007\/978-3-642-41036-9_11","volume-title":"Reachability Problems","author":"G Delzanno","year":"2013","unstructured":"Delzanno, G., Sangnier, A., Traverso, R.: Parameterized verification of broadcast networks of register automata. In: Abdulla, P.A., Potapov, I. (eds.) RP 2013. LNCS, vol. 8169, pp. 109\u2013121. Springer, Heidelberg (2013). doi:10.1007\/978-3-642-41036-9_11"},{"key":"2_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"429","DOI":"10.1007\/978-3-319-21668-3_25","volume-title":"Computer Aided Verification","author":"A Desai","year":"2015","unstructured":"Desai, A., Seshia, S.A., Qadeer, S., Broman, D., Eidson, J.C.: Approximate synchrony: an abstraction for distributed almost-synchronous systems. In: Kroening, D., P\u0103s\u0103reanu, C.S. (eds.) CAV 2015. LNCS, vol. 9207, pp. 429\u2013448. Springer, Cham (2015). doi:10.1007\/978-3-319-21668-3_25"},{"issue":"3","key":"2_CR13","doi-asserted-by":"publisher","first-page":"245","DOI":"10.1016\/0196-6774(82)90023-2","volume":"3","author":"D Dolev","year":"1982","unstructured":"Dolev, D., Klawe, M., Rodeh, M.: An o (n log n) unidirectional distributed algorithm for extrema finding in a circle. J. Algorithms 3(3), 245\u2013260 (1982)","journal-title":"J. Algorithms"},{"key":"2_CR14","doi-asserted-by":"crossref","unstructured":"Emerson, E.A., Namjoshi, K.S.: Reasoning about rings. In: Proceedings of the 22nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 1995, pp. 85\u201394. ACM, New York (1995)","DOI":"10.1145\/199448.199468"},{"issue":"1","key":"2_CR15","doi-asserted-by":"publisher","first-page":"171","DOI":"10.1016\/S0167-6423(96)00034-2","volume":"29","author":"H Garavel","year":"1997","unstructured":"Garavel, H., Mounier, L.: Specification and verification of various distributed leader election algorithms for unidirectional ring networks. Sci. Comput. Program. 29(1), 171\u2013197 (1997)","journal-title":"Sci. Comput. Program."},{"key":"2_CR16","doi-asserted-by":"crossref","unstructured":"John, A., Konnov, I., Schmid, U., Veith, H., Widder, J.: Parameterized model checking of fault-tolerant distributed algorithms by abstraction. In: FMCAD, pp. 201\u2013209 (2013)","DOI":"10.1007\/978-3-642-39176-7_14"},{"issue":"2","key":"2_CR17","doi-asserted-by":"publisher","first-page":"459","DOI":"10.1016\/S0304-3975(96)00256-3","volume":"177","author":"L Fredlund","year":"1997","unstructured":"Fredlund, L., Groote, J.F., Korver, V.: Formal verification of a leader election protocol in process algebra. Theoret. Comput. Sci. 177(2), 459\u2013486 (1997)","journal-title":"Theoret. Comput. Sci."},{"key":"2_CR18","unstructured":"Krstic, S.: Parameterized system verification with guard strengthening and parameter abstraction. In: Automated Verification of Infinite State Systems (2005)"},{"key":"2_CR19","unstructured":"Kusy, B., Abdelwahed, S.: FTSP protocol verification using SPIN, May 2006"},{"key":"2_CR20","doi-asserted-by":"crossref","unstructured":"Mar\u00f3ti, M., Kusy, B., Simon, G., L\u00e9deczi, A.: The flooding time synchronization protocol. In: Proceedings of the 2nd International Conference on Embedded Networked Sensor Systems, SenSys 2004, pp. 39\u201349. ACM, New York (2004)","DOI":"10.1145\/1031495.1031501"},{"key":"2_CR21","doi-asserted-by":"crossref","unstructured":"McInnes, A.I.: Model-checking the flooding time synchronization protocol. In: IEEE International Conference on Control and Automation, ICCA 2009, pp. 422\u2013429, December 2009","DOI":"10.1109\/ICCA.2009.5410508"},{"key":"2_CR22","doi-asserted-by":"publisher","unstructured":"McMillan, K.L.: Parameterized verification of the FLASH cache coherence protocol by compositional model checking. In: Margaria, T., Melham, T. (eds.) CHARME 2001. LNCS, vol. 2144, pp. 179\u2013195. Springer, Heidelberg (2001). doi:10.1007\/3-540-44798-9_17","DOI":"10.1007\/3-540-44798-9_17"},{"key":"2_CR23","volume-title":"A Calculus of Communicating Systems","author":"R Milner","year":"1982","unstructured":"Milner, R.: A Calculus of Communicating Systems. Springer, New York (1982)"},{"key":"2_CR24","doi-asserted-by":"crossref","unstructured":"Pnueli, A.: The temporal logic of programs. In: 18th Annual Symposium on Foundations of Computer Science, pp. 46\u201357, October 1977","DOI":"10.1109\/SFCS.1977.32"},{"key":"2_CR25","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.: Liveness with (0,1, $$\\infty $$)- counter abstraction. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 107\u2013122. Springer, Heidelberg (2002). doi:10.1007\/3-540-45657-0_9"},{"key":"2_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"130","DOI":"10.1007\/978-3-642-19186-2_9","volume-title":"Wireless Sensor Networks","author":"R Sugihara","year":"2011","unstructured":"Sugihara, R., Gupta, R.K.: Clock synchronization with deterministic accuracy guarantee. In: Marr\u00f3n, P.J., Whitehouse, K. (eds.) EWSN 2011. LNCS, vol. 6567, pp. 130\u2013146. Springer, Heidelberg (2011). doi:10.1007\/978-3-642-19186-2_9"},{"key":"2_CR27","doi-asserted-by":"crossref","unstructured":"Talupur, M., Tuttle, M.R.: Going with the flow: parameterized verification using message flows. In: Formal Methods in Computer-Aided Design, FMCAD 2008, pp. 1\u20138, November 2008","DOI":"10.1109\/FMCAD.2008.ECP.14"},{"key":"2_CR28","doi-asserted-by":"crossref","unstructured":"Tan, L., Bu, L., Zhao, J., Wang, L.: Analyzing the robustness of FTSP with timed automata. In: Proceedings of the Second Asia-Pacific Symposium on Internetware, Internetware 2010, pp. 21:1\u201321:4. ACM, New York (2010)","DOI":"10.1145\/2020723.2020744"},{"key":"2_CR29","doi-asserted-by":"crossref","unstructured":"Vasudevan, S., Kurose, J., Towsley, D.: Design and analysis of a leader election algorithm for mobile ad hoc networks. In: Proceedings of the 12th IEEE International Conference on Network Protocols, ICNP 2004, pp. 350\u2013360. IEEE (2004)","DOI":"10.1109\/ICNP.2004.1348124"}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-662-54577-5_2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T19:34:25Z","timestamp":1750188865000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-662-54577-5_2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783662545768","9783662545775"],"references-count":29,"URL":"https:\/\/doi.org\/10.1007\/978-3-662-54577-5_2","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2017]]},"assertion":[{"value":"31 March 2017","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"TACAS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Tools and Algorithms for the Construction and Analysis of Systems","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Uppsala","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Sweden","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2017","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"24 April 2017","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"28 April 2017","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"23","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"tacas2017","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/www.etaps.org\/index.php\/2017\/tacas","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"This content has been made available to all.","name":"free","label":"Free to read"}]}}