{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,27]],"date-time":"2025-03-27T19:52:57Z","timestamp":1743105177984,"version":"3.40.3"},"publisher-location":"Cham","reference-count":27,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030021450"},{"type":"electronic","value":"9783030021467"}],"license":[{"start":{"date-parts":[[2018,1,1]],"date-time":"2018-01-01T00:00:00Z","timestamp":1514764800000},"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":[[2018]]},"DOI":"10.1007\/978-3-030-02146-7_13","type":"book-chapter","created":{"date-parts":[[2018,10,5]],"date-time":"2018-10-05T21:44:02Z","timestamp":1538775842000},"page":"256-276","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Dynamic Cut-Off Algorithm for Parameterised Refinement Checking"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-9118-5087","authenticated-orcid":false,"given":"Antti","family":"Siirtola","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4547-2701","authenticated-orcid":false,"given":"Keijo","family":"Heljanko","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2018,10,5]]},"reference":[{"issue":"2","key":"13_CR1","doi-asserted-by":"publisher","first-page":"153","DOI":"10.1016\/j.jsc.2009.03.003","volume":"45","author":"A Abadi","year":"2010","unstructured":"Abadi, A., Rabinovich, A., Sagiv, M.: Decidable fragments of many-sorted logic. J. Symb. Comput. 45(2), 153\u2013172 (2010)","journal-title":"J. Symb. Comput."},{"key":"13_CR2","unstructured":"Creese, S.J.: Data Independent Induction: CSP Model Checking of Arbitrary Sized Networks. Ph.D. thesis, Oxford University (2001)"},{"key":"13_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L Moura de","year":"2008","unstructured":"de Moura, L., Bj\u00f8rner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337\u2013340. Springer, Heidelberg (2008). \n                      https:\/\/doi.org\/10.1007\/978-3-540-78800-3_24"},{"key":"13_CR4","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"236","DOI":"10.1007\/10721959_19","volume-title":"Automated Deduction - CADE-17","author":"EA Emerson","year":"2000","unstructured":"Emerson, E.A., Kahlon, V.: Reducing model checking of the many to the few. In: McAllester, D. (ed.) CADE 2000. LNCS (LNAI), vol. 1831, pp. 236\u2013254. Springer, Heidelberg (2000). \n                      https:\/\/doi.org\/10.1007\/10721959_19"},{"issue":"1","key":"13_CR5","doi-asserted-by":"publisher","first-page":"63","DOI":"10.1016\/S0304-3975(00)00102-X","volume":"256","author":"A Finkel","year":"2001","unstructured":"Finkel, A., Schnoebelen, P.: Well-structured transition systems everywhere!. Theor. Comput. Sci. 256(1), 63\u201392 (2001)","journal-title":"Theor. Comput. Sci."},{"key":"13_CR6","unstructured":"Gallier, J.H.: Logic for Computer Science: Foundations of Automatic Theorem Proving. Courier Dover Publications, New York (2015)"},{"issue":"2","key":"13_CR7","doi-asserted-by":"publisher","first-page":"149","DOI":"10.1007\/s10009-015-0377-y","volume":"18","author":"Thomas Gibson-Robinson","year":"2015","unstructured":"Gibson-Robinson, T., Armstrong, P., Boulgakov, A., Roscoe, A.W.: FDR3: a parallel refinement checker for CSP. STTT 18(2), 149\u2013167 (2016)","journal-title":"International Journal on Software Tools for Technology Transfer"},{"key":"13_CR8","series-title":"World Scientific Series in Computer Science","doi-asserted-by":"publisher","first-page":"254","DOI":"10.1142\/9789812794499_0020","volume-title":"Current Trends in Theoretical Computer Science: Essays and Tutorials","author":"Y Gurevich","year":"1993","unstructured":"Gurevich, Y.: On the classical decision problem. In: Rozenberg, G., Salomaa, A. (eds.) Current Trends in Theoretical Computer Science: Essays and Tutorials. World Scientific Series in Computer Science, vol. 40, pp. 254\u2013265. World Scientific, Singapore (1993)"},{"key":"13_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"338","DOI":"10.1007\/978-3-642-16901-4_23","volume-title":"Formal Methods and Software Engineering","author":"Y Hanna","year":"2010","unstructured":"Hanna, Y., Samuelson, D., Basu, S., Rajan, H.: Automating cut-off for multi-parameterized systems. In: Dong, J.S., Zhu, H. (eds.) ICFEM 2010. LNCS, vol. 6447, pp. 338\u2013354. Springer, Heidelberg (2010). \n                      https:\/\/doi.org\/10.1007\/978-3-642-16901-4_23"},{"issue":"1","key":"13_CR10","doi-asserted-by":"publisher","first-page":"147","DOI":"10.1016\/j.datak.2007.11.001","volume":"65","author":"M Haustein","year":"2008","unstructured":"Haustein, M., H\u00e4rder, T.: Optimizing lock protocols for native XML processing. Data Knowl. Eng. 65(1), 147\u2013173 (2008)","journal-title":"Data Knowl. Eng."},{"key":"13_CR11","volume-title":"Communicating Sequential Processes","author":"CAR Hoare","year":"1985","unstructured":"Hoare, C.A.R.: Communicating Sequential Processes. Prentice-Hall, New York (1985)"},{"key":"13_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"645","DOI":"10.1007\/978-3-642-14295-6_55","volume-title":"Computer Aided Verification","author":"A Kaiser","year":"2010","unstructured":"Kaiser, A., Kroening, D., Wahl, T.: Dynamic cutoff detection in parameterized concurrent programs. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol. 6174, pp. 645\u2013659. Springer, Heidelberg (2010). \n                      https:\/\/doi.org\/10.1007\/978-3-642-14295-6_55"},{"key":"13_CR13","unstructured":"Lazi\u0107, R.: A Semantic Study of Data Independence with Applications to Model Checking. Ph.D. thesis, Oxford University (1999)"},{"key":"13_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"581","DOI":"10.1007\/3-540-44618-4_41","volume-title":"CONCUR 2000 \u2014 Concurrency Theory","author":"R Lazi\u0107","year":"2000","unstructured":"Lazi\u0107, R., Nowak, D.: A unifying approach to data-independence. In: Palamidessi, C. (ed.) CONCUR 2000. LNCS, vol. 1877, pp. 581\u2013596. Springer, Heidelberg (2000). \n                      https:\/\/doi.org\/10.1007\/3-540-44618-4_41"},{"key":"13_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"217","DOI":"10.1007\/978-3-319-63390-9_12","volume-title":"Computer Aided Verification","author":"O Mari\u0107","year":"2017","unstructured":"Mari\u0107, O., Sprenger, C., Basin, D.: Cutoff bounds for consensus algorithms. In: Majumdar, R., Kun\u010dak, V. (eds.) CAV 2017. LNCS, vol. 10427, pp. 217\u2013237. Springer, Cham (2017). \n                      https:\/\/doi.org\/10.1007\/978-3-319-63390-9_12"},{"key":"13_CR16","doi-asserted-by":"publisher","first-page":"94","DOI":"10.1016\/j.jsc.2013.09.003","volume":"60","author":"BD McKay","year":"2014","unstructured":"McKay, B.D., Piperno, A.: Practical graph isomorphism II. J. Symb. Comput. 60, 94\u2013112 (2014)","journal-title":"J. Symb. Comput."},{"key":"13_CR17","unstructured":"Ongaro, D., Ousterhout, J.: In search of an understandable consensus algorithm. In: Gibson, G., Zeldovich, N. (eds.) USENIX ATC 2014, pp. 305\u2013320. USENIX Association (2014)"},{"key":"13_CR18","series-title":"Texts in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-84882-258-0","volume-title":"Understanding Concurrent Systems","author":"A.W. Roscoe","year":"2010","unstructured":"Roscoe, A.W.: Understanding Concurrent Systems. Springer, Berlin (2010)"},{"key":"13_CR19","doi-asserted-by":"crossref","unstructured":"Siirtola, A.: Algorithmic Multiparameterised Verification of Safety Properties. Process Algebraic Approach. Ph.D. thesis, University of Oulu (2010)","DOI":"10.1007\/978-3-642-16901-4_22"},{"key":"13_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"599","DOI":"10.1007\/978-3-642-54862-8_52","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A Siirtola","year":"2014","unstructured":"Siirtola, A.: Bounds2: a tool for compositional multi-parametrised verification. In: \u00c1brah\u00e1m, E., Havelund, K. (eds.) TACAS 2014. LNCS, vol. 8413, pp. 599\u2013604. Springer, Heidelberg (2014). \n                      https:\/\/doi.org\/10.1007\/978-3-642-54862-8_52"},{"key":"13_CR21","doi-asserted-by":"crossref","unstructured":"Siirtola, A.: Refinement checking parameterised quorum systems. In: Legay, A., Schneider, K. (eds.) ACSD 2017, pp. 39\u201348. IEEE (2017)","DOI":"10.1109\/ACSD.2017.15"},{"key":"13_CR22","unstructured":"Siirtola, A., Heljanko, K.: Online appendix, \n                      http:\/\/cc.oulu.fi\/~asiirtol\/papers\/dyncutoffapp.pdf"},{"issue":"4","key":"13_CR23","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/2776892","volume":"14","author":"Antti Siirtola","year":"2015","unstructured":"Siirtola, A., Heljanko, K.: Parametrised modal interface automata. ACM Trans. Embed. Comput. Syst. 14(4), 65:1\u201365:25 (2015)","journal-title":"ACM Transactions on Embedded Computing Systems"},{"key":"13_CR24","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1016\/j.ic.2015.08.002","volume":"244","author":"A Siirtola","year":"2015","unstructured":"Siirtola, A., Kortelainen, J.: Multi-parameterised compositional verification of safety properties. Inform. Comput. 244, 23\u201348 (2015)","journal-title":"Inform. Comput."},{"key":"13_CR25","unstructured":"Valmari, A., Tienari, M.: An improved failures equivalence for finite-state systems with a reduction algorithm. In: Jonsson, B., Parrow, J., Pehrson, B. (eds.) PSTV 1991, pp. 3\u201318. North-Holland (1991)"},{"key":"13_CR26","doi-asserted-by":"crossref","unstructured":"Yang, Q., Li, M.: A cut-off approach for bounded verification of parameterized systems. In: Kramer, J., Bishop, J., Devanbu, P.T., Uchitel, S. (eds.) ICSE 2010, pp. 345\u2013354. ACM (2010)","DOI":"10.1145\/1806799.1806851"},{"issue":"3","key":"13_CR27","first-page":"139","volume":"30","author":"L Zuck","year":"2004","unstructured":"Zuck, L., Pnueli, A.: Model checking and abstraction to the aid of parameterized systems (a survey). Comput. Lang. Syst. Struct. 30(3), 139\u2013169 (2004)","journal-title":"Comput. Lang. Syst. Struct."}],"container-title":["Lecture Notes in Computer Science","Formal Aspects of Component Software"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-02146-7_13","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,20]],"date-time":"2019-05-20T05:04:53Z","timestamp":1558328693000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-02146-7_13"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018]]},"ISBN":["9783030021450","9783030021467"],"references-count":27,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-02146-7_13","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2018]]},"assertion":[{"value":"5 October 2018","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"FACS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Formal Aspects of Component Software","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Pohang","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Korea (Republic of)","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2018","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"10 October 2018","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"12 October 2018","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"15","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"facs2018","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/sevlab.postech.ac.kr\/facs18","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}