{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,17]],"date-time":"2026-02-17T06:09:52Z","timestamp":1771308592636,"version":"3.50.1"},"publisher-location":"Singapore","reference-count":22,"publisher":"Springer Nature Singapore","isbn-type":[{"value":"9789819560318","type":"print"},{"value":"9789819560325","type":"electronic"}],"license":[{"start":{"date-parts":[[2026,1,1]],"date-time":"2026-01-01T00:00:00Z","timestamp":1767225600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2026,1,1]],"date-time":"2026-01-01T00:00:00Z","timestamp":1767225600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2026]]},"DOI":"10.1007\/978-981-95-6032-5_8","type":"book-chapter","created":{"date-parts":[[2026,2,17]],"date-time":"2026-02-17T05:22:27Z","timestamp":1771305747000},"page":"112-129","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["A Support Tool for\u00a0Verification of\u00a0Simulation Relations Between State Machines with\u00a0Maude"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0009-0009-3173-5273","authenticated-orcid":false,"given":"Takanori","family":"Ishibashi","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-6789-9688","authenticated-orcid":false,"given":"Masaki","family":"Nakamura","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4441-3259","authenticated-orcid":false,"given":"Kazuhiro","family":"Ogata","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2026,2,18]]},"reference":[{"key":"8_CR1","doi-asserted-by":"publisher","unstructured":"Bae, K., Escobar, S., Meseguer, J.: Abstract logical model checking of infinite-state systems using narrowing. In: van Raamsdonk, F. (ed.) 24th International Conference on Rewriting Techniques and Applications (RTA 2013). Leibniz International Proceedings in Informatics (LIPIcs), vol.\u00a021, pp. 81\u201396. Schloss Dagstuhl \u2013 Leibniz-Zentrum f\u00fcr Informatik, Dagstuhl, Germany (2013). https:\/\/doi.org\/10.4230\/LIPIcs.RTA.2013.81, https:\/\/drops.dagstuhl.de\/entities\/document\/10.4230\/LIPIcs.RTA.2013.81","DOI":"10.4230\/LIPIcs.RTA.2013.81"},{"key":"8_CR2","unstructured":"Baier, C., Katoen, J.: Principles of model checking. MIT Press (2008)"},{"key":"8_CR3","doi-asserted-by":"publisher","unstructured":"Bartlett, K.A., Scantlebury, R.A., Wilkinson, P.T.: A note on reliable full-duplex transmission over half-duplex links. Commun. ACM 12(5), 260\u2013261 (1969). https:\/\/doi.org\/10.1145\/362946.362970","DOI":"10.1145\/362946.362970"},{"key":"8_CR4","doi-asserted-by":"publisher","unstructured":"Clarke, E., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement for symbolic model checking. J. ACM 50(5), 752\u2013794 (2003). https:\/\/doi.org\/10.1145\/876638.876643","DOI":"10.1145\/876638.876643"},{"key":"8_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-540-69850-0_1","volume-title":"25 Years of Model Checking","author":"EM Clarke","year":"2008","unstructured":"Clarke, E.M.: The birth of model checking. In: Grumberg, O., Veith, H. (eds.) 25 Years of Model Checking. LNCS, vol. 5000, pp. 1\u201326. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-69850-0_1"},{"key":"8_CR6","doi-asserted-by":"publisher","unstructured":"Clarke, E.M., Grumberg, O., Long, D.E.: Model checking and abstraction. ACM Trans. Program. Lang. Syst. 16(5), 1512\u20131542 (1994). https:\/\/doi.org\/10.1145\/186025.186051","DOI":"10.1145\/186025.186051"},{"issue":"3","key":"8_CR7","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1007\/S100090050035","volume":"2","author":"EM Clarke","year":"1999","unstructured":"Clarke, E.M., Grumberg, O., Minea, M., Peled, D.A.: State space reduction using partial order techniques. Int. J. Softw. Tools Technol. Transf. 2(3), 279\u2013287 (1999). https:\/\/doi.org\/10.1007\/S100090050035","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"8_CR8","doi-asserted-by":"publisher","unstructured":"Clarke, E.M., Henzinger, T.A., Veith, H., Bloem, R. (eds.): Handbook of Model Checking. Springer (2018). https:\/\/doi.org\/10.1007\/978-3-319-10575-8","DOI":"10.1007\/978-3-319-10575-8"},{"key":"8_CR9","doi-asserted-by":"publisher","unstructured":"Clavel, M., et al.: (eds.): All About Maude - A High-Performance Logical Framework, How to Specify, Program and Verify Systems in Rewriting Logic, Lecture Notes in Computer Science, vol. 4350. Springer (2007). https:\/\/doi.org\/10.1007\/978-3-540-71999-1","DOI":"10.1007\/978-3-540-71999-1"},{"key":"8_CR10","doi-asserted-by":"crossref","unstructured":"Diaconescu, R., Futatsugi, K.: CafeOBJ report: the language, proof techniques, and methodologies for object-oriented algebraic specification, vol.\u00a06. World Scientific (1998)","DOI":"10.1142\/3831"},{"key":"8_CR11","doi-asserted-by":"publisher","first-page":"84","DOI":"10.1007\/978-3-031-65941-6_5","volume-title":"Rewriting Logic and Its Applications","author":"CM Do","year":"2024","unstructured":"Do, C.M., Ogata, K.: Equivalence checking of quantum circuits based on DIRAC notation in Maude. In: Ogata, K., Mart\u00ed-Oliet, N. (eds.) Rewriting Logic and Its Applications, pp. 84\u2013103. Springer Nature Switzerland, Cham (2024)"},{"key":"8_CR12","doi-asserted-by":"publisher","unstructured":"Dur\u00e1n, F., Escobar, S., Meseguer, J., Sapi\u00f1a, J.: Nuitp: An inductive theorem prover for equational program verification. In: Proceedings of the 26th International Symposium on Principles and Practice of Declarative Programming. PPDP \u201924, Association for Computing Machinery, New York, NY, USA (2024). https:\/\/doi.org\/10.1145\/3678232.3678236","DOI":"10.1145\/3678232.3678236"},{"key":"8_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-642-03829-7_1","volume-title":"Foundations of Security Analysis and Design V","author":"S Escobar","year":"2009","unstructured":"Escobar, S., Meadows, C., Meseguer, J.: Maude-NPA: cryptographic protocol analysis modulo equational properties. In: Aldini, A., Barthe, G., Gorrieri, R. (eds.) FOSAD 2007-2009. LNCS, vol. 5705, pp. 1\u201350. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-03829-7_1"},{"key":"8_CR14","volume-title":"Communicating sequential processes","author":"CAR Hoare","year":"1985","unstructured":"Hoare, C.A.R.: Communicating sequential processes. Prentice-Hall Inc, USA (1985)"},{"key":"8_CR15","unstructured":"Ishibashi, T., Ogata, K.: Combining model checking with simulation-based techniques for protocol verification (2025), manuscript submitted for publication"},{"key":"8_CR16","unstructured":"Lynch, N.A.: Distributed Algorithms. Morgan Kaufmann Publishers Inc., San Francisco, CA, USA (1996)"},{"key":"8_CR17","doi-asserted-by":"publisher","unstructured":"Meseguer, J., Palomino, M., Mart\u00c3\u00ad-Oliet, N.: Equational abstractions. Theoretical Comput. Sci. 403(2), 239\u2013264 (2008). https:\/\/doi.org\/10.1016\/j.tcs.2008.04.040, https:\/\/www.sciencedirect.com\/science\/article\/pii\/S0304397508003605","DOI":"10.1016\/j.tcs.2008.04.040"},{"key":"8_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-10235-3","volume-title":"A Calculus of Communicating Systems","year":"1980","unstructured":"Milner, R. (ed.): A Calculus of Communicating Systems. LNCS, vol. 92. Springer, Heidelberg (1980). https:\/\/doi.org\/10.1007\/3-540-10235-3"},{"key":"8_CR19","unstructured":"Milner, R.: Communication and concurrency. PHI Series in computer science, Prentice Hall (1989)"},{"key":"8_CR20","doi-asserted-by":"publisher","first-page":"127","DOI":"10.1016\/j.entcs.2008.02.018","volume":"201","author":"K Ogata","year":"2008","unstructured":"Ogata, K., Futatsugi, K.: Simulation-based verification for invariant properties in the OTS\/CafeOBJ method. Electron. Notes Theor. Comput. Sci. 201, 127\u2013154 (2008)","journal-title":"Electron. Notes Theor. Comput. Sci."},{"key":"8_CR21","doi-asserted-by":"publisher","first-page":"332","DOI":"10.1007\/978-3-540-78800-3_23","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"PC \u00d6lveczky","year":"2008","unstructured":"\u00d6lveczky, P.C., Meseguer, J.: The real-time Maude tool. In: Ramakrishnan, C.R., Rehof, J. (eds.) Tools and Algorithms for the Construction and Analysis of Systems, pp. 332\u2013336. Springer, Berlin Heidelberg, Berlin, Heidelberg (2008)"},{"issue":"2","key":"8_CR22","doi-asserted-by":"publisher","first-page":"309","DOI":"10.1007\/s00165-016-0398-7","volume":"29","author":"A Riesco","year":"2016","unstructured":"Riesco, A., Ogata, K., Futatsugi, K.: A Maude environment for CafeOBJ. Formal Aspects Comput. 29(2), 309\u2013334 (2016). https:\/\/doi.org\/10.1007\/s00165-016-0398-7","journal-title":"Formal Aspects Comput."}],"container-title":["Lecture Notes in Computer Science","Software Fault Prevention, Verification, and Validation"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-981-95-6032-5_8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,2,17]],"date-time":"2026-02-17T05:22:28Z","timestamp":1771305748000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-981-95-6032-5_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026]]},"ISBN":["9789819560318","9789819560325"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/978-981-95-6032-5_8","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2026]]},"assertion":[{"value":"18 February 2026","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"SFPVV","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Symposium on Software Fault Prevention, Verification, and Validation","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Shanghai","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"China","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2025","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"8 November 2025","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"9 November 2025","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"sfpvv2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/sfpvv2025.world\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}