{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T04:58:27Z","timestamp":1750309107108,"version":"3.41.0"},"reference-count":47,"publisher":"Association for Computing Machinery (ACM)","issue":"4","license":[{"start":{"date-parts":[[2004,10,1]],"date-time":"2004-10-01T00:00:00Z","timestamp":1096588800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Comput. Logic"],"published-print":{"date-parts":[[2004,10]]},"abstract":"<jats:p>In existing simulation proof techniques, a single step in a lower-level specification may be simulated by an extended execution fragment in a higher-level one. As a result, it is cumbersome to mechanize these techniques using general-purpose theorem provers. Moreover, it is undecidable whether a given relation is a simulation, even if tautology checking is decidable for the underlying specification logic. This article studies various types of &lt;i&gt;normed simulations&lt;\/i&gt;. In a normed simulation, each step in a lower-level specification can be simulated by at most one step in the higher-level one, for any related pair of states. In earlier work we demonstrated that normed simulations are quite useful as a vehicle for the formalization of refinement proofs via theorem provers. Here we show that normed simulations also have pleasant theoretical properties: (1) under some reasonable assumptions, it is decidable whether a given relation is a normed forward simulation, provided tautology checking is decidable for the underlying logic; (2) at the semantic level, normed forward and backward simulations together form a complete proof method for establishing behavior inclusion, provided that the higher-level specification has finite invisible nondeterminism.<\/jats:p>","DOI":"10.1145\/1024922.1024923","type":"journal-article","created":{"date-parts":[[2004,10,7]],"date-time":"2004-10-07T17:38:56Z","timestamp":1097170736000},"page":"577-610","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":3,"title":["A theory of normed simulations"],"prefix":"10.1145","volume":"5","author":[{"given":"David","family":"Griffioen","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Frits","family":"Vaandrager","sequence":"additional","affiliation":[{"name":"Radboud University Nijmegen, The Netherlands"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2004,10]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(91)90224-P"},{"key":"e_1_2_1_2_1","doi-asserted-by":"crossref","unstructured":"Ariola Z. and Klop J. 1996. Equational term graph rewriting. Fundamenta Informaticae 26 3\/4 207--240. Extended version published as Tech. rep. CIS-TR-95-16 University of Oregon Eugene OR.]]   Ariola Z. and Klop J. 1996. Equational term graph rewriting. Fundamenta Informaticae 26 3\/4 207--240. Extended version published as Tech. rep. CIS-TR-95-16 University of Oregon Eugene OR.]]","DOI":"10.3233\/FI-1996-263401"},{"volume-title":"Proceedings of 3rd International Conference on Foundations of Science and Computation Structures (FOSSACS)","year":"2000","author":"Baier C.","key":"e_1_2_1_3_1"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1016\/0020-0190(96)00034-8"},{"volume-title":"LFM 2000: Fifth NASA Langley Formal Methods Workshop, C. M. Holloway, Ed. NASA Langley Research Center","author":"Bensalem S.","key":"e_1_2_1_5_1"},{"volume":"1102","volume-title":"Proceedings of the 8th International Conference on Computer Aided Verification","author":"Bensalem S.","key":"e_1_2_1_6_1"},{"key":"e_1_2_1_7_1","doi-asserted-by":"crossref","unstructured":"Browne M. Clarke E. and Gr\u00fcmberg O. 1988. Characterizing finite Kripke structures in propositional temporal logic. Theor. Comput. Sci. 59 1 2 115--131.]] 10.1016\/0304-3975(88)90098-9   Browne M. Clarke E. and Gr\u00fcmberg O. 1988. Characterizing finite Kripke structures in propositional temporal logic. Theor. Comput. Sci. 59 1 2 115--131.]] 10.1016\/0304-3975(88)90098-9","DOI":"10.1016\/0304-3975(88)90098-9"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/201019.201032"},{"volume":"1275","volume-title":"10th International Conference on Theorem Proving in Higher Order Logics (TPHOLs'97)","author":"Devillers M.","key":"e_1_2_1_9_1"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1008764923992"},{"volume-title":"IOA: A language for specifiying, programming, and validating distributed systems. Available through URL http:\/\/larch.lcs.mit.edu:8001\/&sim;garland\/ioaLanguage.html.]]","year":"1997","author":"Garland S.","key":"e_1_2_1_11_1"},{"key":"e_1_2_1_12_1","doi-asserted-by":"crossref","unstructured":"Gawlick R. Segala R. S\u00f8gaard-Andersen J. and Lynch N. 1993. Liveness in timed and untimed systems. Tech. rep. MIT\/LCS\/TR-587. Laboratory for Computer Science MIT Cambridge MA.]]   Gawlick R. Segala R. S\u00f8gaard-Andersen J. and Lynch N. 1993. Liveness in timed and untimed systems. Tech. rep. MIT\/LCS\/TR-587. Laboratory for Computer Science MIT Cambridge MA.]]","DOI":"10.1007\/3-540-58201-0_66"},{"key":"e_1_2_1_13_1","doi-asserted-by":"crossref","unstructured":"Ginzburg A. 1968. Algebraic Theory of Automata. Academic Press New York NY and London U.K.]]  Ginzburg A. 1968. Algebraic Theory of Automata. Academic Press New York NY and London U.K.]]","DOI":"10.1016\/B978-1-4832-0013-2.50009-6"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/233551.233556"},{"key":"e_1_2_1_15_1","unstructured":"Griffioen W. 2000. Studies in computer aided verification of protocols. Ph.D. dissertation. University of Nijmegen Nijmegen The Netherlands. Postscript and PVS sources available via http:\/\/www.cs.kun.nl\/ita\/former_members\/davidg\/.]]  Griffioen W. 2000. Studies in computer aided verification of protocols. Ph.D. dissertation. University of Nijmegen Nijmegen The Netherlands. Postscript and PVS sources available via http:\/\/www.cs.kun.nl\/ita\/former_members\/davidg\/.]]"},{"volume":"1427","volume-title":"Proceedings of the 10th International Conference on Computer Aided Verification","author":"Griffioen W.","key":"e_1_2_1_16_1"},{"volume-title":"Report CS-R9566, Department of Software Technology, CWI","year":"1995","author":"Groote J.","key":"e_1_2_1_17_1"},{"key":"e_1_2_1_18_1","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4612-2704-5","volume-title":"Larch: Languages and Tools for Formal Specification","author":"Guttag J.","year":"1993"},{"volume-title":"Proceedings of the International Workshop TYPES'93","year":"1993","author":"Helmink L.","key":"e_1_2_1_19_1"},{"volume-title":"Proceedings of the 4th Annual ACM Symposium on Principles of Distributed Computing (Minaki","year":"1985","author":"Jonsson B.","key":"e_1_2_1_20_1"},{"key":"e_1_2_1_21_1","unstructured":"Jonsson B. 1987. Compositional verification of distributed systems. Ph.D. dissertation Department of Computer Systems Uppsala University Uppsala Sweden. DoCS 87\/09.]]  Jonsson B. 1987. Compositional verification of distributed systems. Ph.D. dissertation Department of Computer Systems Uppsala University Uppsala Sweden. DoCS 87\/09.]]"},{"volume-title":"Proceedings of the REX Workshop on Stepwise Refinement of Distributed Systems: Models, Formalism, Correctness (Mook, The Netherlands, May\/June","year":"1989","author":"Jonsson B.","key":"e_1_2_1_22_1"},{"key":"e_1_2_1_23_1","volume-title":"Proceedings of CONCUR 91","volume":"527","author":"Jonsson B.","year":"1991"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/174662.174665"},{"key":"e_1_2_1_25_1","unstructured":"Klarlund N. and Schneider F. 1989. Verifying safety properties using infinite-state automata. Tech. rep. 89-1039. Department of Computer Science Cornell University Ithaca NY.]]   Klarlund N. and Schneider F. 1989. Verifying safety properties using infinite-state automata. Tech. rep. 89-1039. Department of Computer Science Cornell University Ithaca NY.]]"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1993.1064"},{"key":"e_1_2_1_27_1","volume-title":"The Art of Computer Programming","volume":"1","author":"Knuth D.","year":"1997"},{"volume":"2031","volume-title":"Proceedings of the International Conference on Tools and Algorithms for the Construction and Analysis of Systems","author":"Lakhnech Y.","key":"e_1_2_1_28_1"},{"key":"e_1_2_1_29_1","unstructured":"Lamport L. 1983. What good is temporal logic? In Information Processing 83 R. Mason Ed. North-Holland Amsterdam The Netherlands 657--668.]]  Lamport L. 1983. What good is temporal logic? In Information Processing 83 R. Mason Ed. North-Holland Amsterdam The Netherlands 657--668.]]"},{"key":"e_1_2_1_30_1","unstructured":"Lynch N. 1996. Distributed Algorithms. Morgan Kaufmann Publishers Inc. San Fransisco CA.]]   Lynch N. 1996. Distributed Algorithms. Morgan Kaufmann Publishers Inc. San Fransisco CA.]]"},{"volume-title":"Proceedings of the 6th Annual ACM Symposium on Principles of Distributed Computing. 137--151","year":"1840","author":"Lynch N.","key":"e_1_2_1_31_1"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1995.1134"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1996.0060"},{"volume":"1548","volume-title":"Proceedings AMAST'98","author":"Manna Z.","key":"e_1_2_1_34_1"},{"volume-title":"Proceedings of the 2nd Joint Conference on Artificial Intelligence. British Computer Society Press","year":"1971","author":"Milner R.","key":"e_1_2_1_35_1"},{"key":"e_1_2_1_36_1","unstructured":"Milner R. 1989. Communication and Concurrency. Prentice-Hall International Englewood Cliffs NJ.]]   Milner R. 1989. Communication and Concurrency. Prentice-Hall International Englewood Cliffs NJ.]]"},{"key":"e_1_2_1_37_1","unstructured":"Mueller O. 1998. A verification environment for I\/O automata based on formalized meta-theory. Ph.D. dissertation. Technical University of Munich Munich Germany.]]  Mueller O. 1998. A verification environment for I\/O automata based on formalized meta-theory. Ph.D. dissertation. Technical University of Munich Munich Germany.]]"},{"key":"e_1_2_1_38_1","volume-title":"Proceedings of the 17th Conference on Foundations of Software Technology and Theoretical Computer Science","volume":"1346","author":"Namjoshi K.","year":"1997"},{"volume":"996","volume-title":"Eds. Lecture Notes in Computer Science","author":"Nipkow T.","key":"e_1_2_1_39_1"},{"key":"e_1_2_1_40_1","doi-asserted-by":"crossref","first-page":"319","DOI":"10.1007\/BF00268134","article-title":"An axiomatic proof technique for parallel programs","volume":"6","author":"Owicki S.","year":"1976","journal-title":"Acta Inf."},{"key":"e_1_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1109\/32.345827"},{"key":"e_1_2_1_42_1","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9780511663079","volume-title":"Data Refinement: Model-Oriented Proof Methods and their Comparison","author":"Roever W. De.","year":"1998"},{"key":"e_1_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1016\/0020-0190(91)90061-L"},{"volume":"697","volume-title":"Proceedings of the 5th International Conference on Computer Aided Verification","author":"S\u00f8gaard-Andersen J.","key":"e_1_2_1_44_1"},{"key":"e_1_2_1_45_1","unstructured":"S\u00f8gaard-Andersen J. Lynch N. and Lampson B. 1993b. Correctness of communication protocols---a case study. Tech. rep. MIT\/LCS\/TR-589. Laboratory for Computer Science MIT Cambridge MA.]]   S\u00f8gaard-Andersen J. Lynch N. and Lampson B. 1993b. Correctness of communication protocols---a case study. Tech. rep. MIT\/LCS\/TR-589. Laboratory for Computer Science MIT Cambridge MA.]]"},{"key":"e_1_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(86)90007-1"},{"key":"e_1_2_1_47_1","first-page":"1","article-title":"The meaning of formal: from weak to strong formal methods","volume":"1","author":"Wolper P.","year":"1997","journal-title":"Springer Int. J. Softw. Tools Tech. Trans."}],"container-title":["ACM Transactions on Computational Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1024922.1024923","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1024922.1024923","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T22:48:46Z","timestamp":1750286926000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1024922.1024923"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2004,10]]},"references-count":47,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2004,10]]}},"alternative-id":["10.1145\/1024922.1024923"],"URL":"https:\/\/doi.org\/10.1145\/1024922.1024923","relation":{},"ISSN":["1529-3785","1557-945X"],"issn-type":[{"type":"print","value":"1529-3785"},{"type":"electronic","value":"1557-945X"}],"subject":[],"published":{"date-parts":[[2004,10]]},"assertion":[{"value":"2004-10-01","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}