{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,8,6]],"date-time":"2025-08-06T13:40:15Z","timestamp":1754487615377},"publisher-location":"Berlin, Heidelberg","reference-count":19,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540646082"},{"type":"electronic","value":"9783540693390"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1998]]},"DOI":"10.1007\/bfb0028756","type":"book-chapter","created":{"date-parts":[[2005,12,1]],"date-time":"2005-12-01T06:48:09Z","timestamp":1133419689000},"page":"332-344","source":"Crossref","is-referenced-by-count":6,"title":["Normed simulations"],"prefix":"10.1007","author":[{"given":"David","family":"Griffioen","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Frits","family":"Vaandrager","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,6,18]]},"reference":[{"issue":"2","key":"31_CR1","doi-asserted-by":"publisher","first-page":"253","DOI":"10.1016\/0304-3975(91)90224-P","volume":"82","author":"M. Abadi","year":"1991","unstructured":"M. Abadi and L. Lamport. The existence of refinement mappings. Theoretical Computer Science, 82(2):253\u2013284, 1991.","journal-title":"Theoretical Computer Science"},{"key":"31_CR2","doi-asserted-by":"crossref","unstructured":"S. Bensalem, Y. Lakhnech, and H. Saidi. Powerful techniques for the automatic generation of invariants. In Proc. CAV'96, LNCS 1102, pp 323\u2013335. Springer, 1996.","DOI":"10.1007\/3-540-61474-5_80"},{"issue":"12","key":"31_CR3","doi-asserted-by":"publisher","first-page":"115","DOI":"10.1016\/0304-3975(88)90098-9","volume":"59","author":"M. Browne","year":"1988","unstructured":"M. Browne, E. Clarke, and O. Gr\u00fcmberg. Characterizing finite Kripke structures in propositional temporal logic. Theoretical Comp. Sci., 59(1,2):115\u2013131, 1988.","journal-title":"Theoretical Comp. Sci."},{"issue":"2","key":"31_CR4","doi-asserted-by":"publisher","first-page":"458","DOI":"10.1145\/201019.201032","volume":"42","author":"R. Nicola De","year":"1995","unstructured":"R. De Nicola and F. Vaandrager. Three logics for branching bisimulation. Journal of the ACM, 42(2):458\u2013487, 1995.","journal-title":"Journal of the ACM"},{"key":"31_CR5","doi-asserted-by":"crossref","unstructured":"M. Devillers, W. Griffioen, and O. M\u00fcller. Possibly infinite sequences: A comparative case study. In Proc. TPHOLs'97, LNCS 1275, pp 89\u2013104. Springer, 1997.","DOI":"10.1007\/BFb0028388"},{"key":"31_CR6","unstructured":"M. Devillers, W. Griffioen, J. Romijn, and F. Vaandrager. Verification of a leader election protocol \u2014 formal methods applied to IEEE 1394. Technical Report CSI-R9728, University of Nijmegen, 1997."},{"key":"31_CR7","unstructured":"S. Garland, N. Lynch, and M. Vaziri. IOA: A language for specifiying, programming, and validating distributed systems, September 1997. Available through http:\/\/larch.lcs.mit.edu:8001\/~garland\/ioaLanguage.html."},{"key":"31_CR8","doi-asserted-by":"crossref","unstructured":"R. Gawlick, R. Segala, J. S\u00f8gaard-Andersen, and N. Lynch. Liveness in timed and untimed systems. In Proc. 21 th ICALP, LNCS 820. Springer, 1994. A full version appears as MIT Technical Report MIT\/LCS\/TR-587.","DOI":"10.1007\/3-540-58201-0_66"},{"issue":"3","key":"31_CR9","doi-asserted-by":"publisher","first-page":"555","DOI":"10.1145\/233551.233556","volume":"43","author":"R. Glabbeek van","year":"1996","unstructured":"R. van Glabbeek and W. Weijland. Branching time and abstraction in bisimulation semantics. Journal of the ACM, 43(3):555\u2013600, 1996.","journal-title":"Journal of the ACM"},{"key":"31_CR10","unstructured":"J. Groote and J. Springintveld. Focus points and convergent process operators \u2014 a proof strategy for protocol verification. Report CS-119566, CWI, 1995."},{"key":"31_CR11","doi-asserted-by":"crossref","unstructured":"L. Helmink, M. Sellink, and F. Vaandrager. Proof-checking a data link protocol. In Proc. TYPES'93, LNCS 806, pp 127\u2013165. Springer, 1994.","DOI":"10.1007\/3-540-58085-9_75"},{"key":"31_CR12","unstructured":"IEEE Computer Society. IEEE Standard for a High Performance Serial Bus. Std 1394-1995, August 1996."},{"issue":"2","key":"31_CR13","doi-asserted-by":"publisher","first-page":"214","DOI":"10.1006\/inco.1995.1134","volume":"121","author":"N. Lynch","year":"1995","unstructured":"N. Lynch and F. Vaandrager. Forward and backward simulations, I: Untimed systems. Information and Computation, 121(2):214\u2013233, 1995.","journal-title":"Information and Computation"},{"key":"31_CR14","doi-asserted-by":"crossref","unstructured":"K. Namjoshi. A simple characterization of stuttering bisimulation. In Proc. FST & TCS'97, LNCS 1346, pp 284\u2013296. Springer, 1997.","DOI":"10.1007\/BFb0058037"},{"key":"31_CR15","doi-asserted-by":"crossref","unstructured":"T. Nipkow and K. Slind. I\/O automata in Isabelle\/HOL. In Types for Proofs and Programs, LNCS 996, pp 101\u2013119. Springer, 1995.","DOI":"10.1007\/3-540-60579-7_6"},{"issue":"2","key":"31_CR16","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1109\/32.345827","volume":"21","author":"S. Owre","year":"1995","unstructured":"S. Owre, J. Rushby, N. Shankar, and F. von Henke. Formal verification for fault-tolerant architectures: Prolegomena to the design of PVS. IEEE Transactions on Software Engineering, 21(2):107\u2013125, 1995.","journal-title":"IEEE Transactions on Software Engineering"},{"issue":"1","key":"31_CR17","doi-asserted-by":"publisher","first-page":"45","DOI":"10.1016\/0020-0190(91)90061-L","volume":"39","author":"A. Sistla","year":"1991","unstructured":"A. Sistla. Proving correctness with respect to nondeterministic safety specifications. Information Processing Letters, 39(1):45\u201349, 1991.","journal-title":"Information Processing Letters"},{"key":"31_CR18","doi-asserted-by":"crossref","unstructured":"J. S\u00f8gaard-Andersen, S. Garland, J. Guttag, N. Lynch, and A. Pogosyants. Computer-assisted simulation proofs. In Proc. CAV'93, LNCS 697, pp 305\u2013319. Springer, 1993.","DOI":"10.1007\/3-540-56922-7_25"},{"key":"31_CR19","series-title":"Report MIT\/LCS\/TR-589","volume-title":"Correctness of communication protocols \u2014 a case study","author":"J. S\u00f8gaard-Andersen","year":"1993","unstructured":"J. S\u00f8gaard-Andersen, N. Lynch, and B. Lampson. Correctness of communication protocols \u2014 a case study. Report MIT\/LCS\/TR-589, MIT, Cambridge, MA, 1993."}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BFb0028756","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,11]],"date-time":"2020-04-11T08:23:40Z","timestamp":1586593420000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0028756"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1998]]},"ISBN":["9783540646082","9783540693390"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/bfb0028756","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1998]]}}}