{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,8]],"date-time":"2024-09-08T04:06:00Z","timestamp":1725768360953},"publisher-location":"Berlin, Heidelberg","reference-count":22,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642540127"},{"type":"electronic","value":"9783642540134"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2014]]},"DOI":"10.1007\/978-3-642-54013-4_13","type":"book-chapter","created":{"date-parts":[[2014,1,3]],"date-time":"2014-01-03T01:08:09Z","timestamp":1388711289000},"page":"222-241","source":"Crossref","is-referenced-by-count":0,"title":["Message-Passing Algorithms for the Verification of Distributed Protocols"],"prefix":"10.1007","author":[{"given":"Lo\u00efg","family":"Jezequel","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Javier","family":"Esparza","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"13_CR1","unstructured":"Fabre, E.: Bayesian Networks of Dynamic Systems. Habilitation \u00e0 diriger des recherches, Universit\u00e9 de Rennes1 (2007)"},{"key":"13_CR2","doi-asserted-by":"crossref","unstructured":"Fabre, E., Jezequel, L.: Distributed optimal planning: an approach by weighted automata calculus. In: CDC, pp. 211\u2013216 (2009)","DOI":"10.1109\/CDC.2009.5400084"},{"key":"13_CR3","doi-asserted-by":"crossref","unstructured":"Fabre, E., Jezequel, L., Haslum, P., Thi\u00e9baux, S.: Cost-optimal factored planning: Promises and pitfalls. In: ICAPS, pp. 65\u201372 (2010)","DOI":"10.1609\/icaps.v20i1.13415"},{"issue":"1","key":"13_CR4","first-page":"61","volume":"7","author":"K. Raymond","year":"1989","unstructured":"Raymond, K.: A tree-based algorithm for distributed mutual exclusion. TCS\u00a07(1), 61\u201377 (1989)","journal-title":"TCS"},{"key":"13_CR5","doi-asserted-by":"crossref","unstructured":"Speakman, T., et al.: PGM reliable transport protocol specification. RFC 3208 (Experimental) of the IETF (2001)","DOI":"10.17487\/rfc3208"},{"key":"13_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"331","DOI":"10.1007\/3-540-36577-X_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"J.M. Cobleigh","year":"2003","unstructured":"Cobleigh, J.M., Giannakopoulou, D., P\u0103s\u0103reanu, C.S.: Learning assumptions for compositional verification. In: Garavel, H., Hatcliff, J. (eds.) TACAS 2003. LNCS, vol.\u00a02619, pp. 331\u2013346. Springer, Heidelberg (2003)"},{"key":"13_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"213","DOI":"10.1007\/3-540-44829-2_14","volume-title":"Model Checking Software","author":"C. Flanagan","year":"2003","unstructured":"Flanagan, C., Qadeer, S.: Thread-modular model checking. In: Ball, T., Rajamani, S.K. (eds.) SPIN 2003. LNCS, vol.\u00a02648, pp. 213\u2013224. Springer, Heidelberg (2003)"},{"key":"13_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"186","DOI":"10.1007\/BFb0023732","volume-title":"Computer-Aided Verification","author":"S. Graf","year":"1991","unstructured":"Graf, S., Steffen, B.: Compositional minimization of finite state systems. In: Clarke, E., Kurshan, R.P. (eds.) CAV 1990. LNCS, vol.\u00a0531, pp. 186\u2013196. Springer, Heidelberg (1991)"},{"issue":"3","key":"13_CR9","doi-asserted-by":"publisher","first-page":"843","DOI":"10.1145\/177492.177725","volume":"16","author":"O. Grumberg","year":"1994","unstructured":"Grumberg, O., Long, D.E.: Model checking and modular verification. TOPLAS\u00a016(3), 843\u2013871 (1994)","journal-title":"TOPLAS"},{"key":"13_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"133","DOI":"10.1007\/3-540-60630-0_7","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A.W. Roscoe","year":"1995","unstructured":"Roscoe, A.W., Gardiner, P.H.B., Goldsmith, M.H., Hullance, J.R., Jackson, D.M., Scattergood, J.B.: Hierarchical compression for model-checking CSP or how to check 1020 dining philosophers for deadlock. In: Brinksma, E., Steffen, B., Cleaveland, W.R., Larsen, K.G., Margaria, T. (eds.) TACAS 1995. LNCS, vol.\u00a01019, pp. 133\u2013152. Springer, Heidelberg (1995)"},{"key":"13_CR11","unstructured":"FRD2 user manual (2009)"},{"issue":"1","key":"13_CR12","doi-asserted-by":"publisher","first-page":"36","DOI":"10.1145\/151646.151648","volume":"15","author":"R. Cleaveland","year":"1993","unstructured":"Cleaveland, R., Parrow, J., Steffen, B.: The concurrency workbench: A semantics-based tool for the verification of concurrent systems. TOPLAS\u00a015(1), 36\u201372 (1993)","journal-title":"TOPLAS"},{"issue":"2","key":"13_CR13","doi-asserted-by":"publisher","first-page":"89","DOI":"10.1007\/s10009-012-0244-z","volume":"15","author":"H. Garavel","year":"2013","unstructured":"Garavel, H., Lang, F., Mateescu, R., Serwe, W.: CADP 2011: a toolbox for the construction and analysis of distributed processes. STTT\u00a015(2), 89\u2013107 (2013)","journal-title":"STTT"},{"issue":"2","key":"13_CR14","doi-asserted-by":"publisher","first-page":"109","DOI":"10.1007\/s10009-011-0216-8","volume":"14","author":"P.A. Abdulla","year":"2012","unstructured":"Abdulla, P.A.: Regular model checking. STTT\u00a014(2), 109\u2013118 (2012)","journal-title":"STTT"},{"issue":"14","key":"13_CR15","doi-asserted-by":"publisher","first-page":"2773","DOI":"10.1080\/00207540410001705220","volume":"42","author":"B. B\u00e9rard","year":"2004","unstructured":"B\u00e9rard, B., Bouyer, P., Petit, A.: Analysing the PGM protocol with UPPAAL. International Journal of Production Research\u00a042(14), 2773\u20132791 (2004)","journal-title":"International Journal of Production Research"},{"key":"13_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"264","DOI":"10.1007\/978-3-540-45236-2_16","volume-title":"FME 2003: Formal Methods","author":"M. Boyer","year":"2003","unstructured":"Boyer, M., Sighireanu, M.: Synthesis and verification of constraints in the PGM protocol. In: Araki, K., Gnesi, S., Mandrioli, D. (eds.) FME 2003. LNCS, vol.\u00a02805, pp. 264\u2013281. Springer, Heidelberg (2003)"},{"key":"13_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"128","DOI":"10.1007\/3-540-36577-X_10","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"J. Esparza","year":"2003","unstructured":"Esparza, J., Maidl, M.: Simple representative instantiations for multicast protocols. In: Garavel, H., Hatcliff, J. (eds.) TACAS 2003. LNCS, vol.\u00a02619, pp. 128\u2013143. Springer, Heidelberg (2003)"},{"key":"13_CR18","doi-asserted-by":"crossref","unstructured":"Bodlaender, H.: A linear time algorithm for finding tree-decompositions of small treewidth. In: STC, pp. 226\u2013234 (1993)","DOI":"10.1145\/167088.167161"},{"key":"13_CR19","unstructured":"Sakarovitch, J.: \u00c9l\u00e9ments de th\u00e9orie des automates. Vuibert (2003)"},{"key":"13_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"281","DOI":"10.1007\/3-540-15670-4_14","volume-title":"Seminar on Concurrency","author":"S.D. Brookes","year":"1985","unstructured":"Brookes, S.D., Roscoe, A.W.: An improved failures model for communicating processes. In: Brookes, S.D., Winskel, G., Roscoe, A.W. (eds.) Seminar on Concurrency. LNCS, vol.\u00a0197, pp. 281\u2013305. Springer, Heidelberg (1985)"},{"key":"13_CR21","doi-asserted-by":"crossref","unstructured":"Valmari, A.: All linear-time congruences for finite LTSs and familiar operators. In: ACSD (2012)","DOI":"10.1109\/ACSD.2012.14"},{"key":"13_CR22","unstructured":"Holzmann, G.: The SPIN model checker: primer and reference manual. Addison-Wesley Professional (2003)"}],"container-title":["Lecture Notes in Computer Science","Verification, Model Checking, and Abstract Interpretation"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-54013-4_13","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,7,9]],"date-time":"2023-07-09T12:03:15Z","timestamp":1688904195000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-54013-4_13"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014]]},"ISBN":["9783642540127","9783642540134"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-54013-4_13","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2014]]}}}