{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,4,5]],"date-time":"2022-04-05T01:42:36Z","timestamp":1649122956093},"reference-count":17,"publisher":"Springer Science and Business Media LLC","issue":"1-2","license":[{"start":{"date-parts":[[1993,8,1]],"date-time":"1993-08-01T00:00:00Z","timestamp":744163200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Form Method Syst Des"],"published-print":{"date-parts":[[1993,8]]},"DOI":"10.1007\/bf01383986","type":"journal-article","created":{"date-parts":[[2005,4,1]],"date-time":"2005-04-01T21:08:55Z","timestamp":1112389735000},"page":"117-149","source":"Crossref","is-referenced-by-count":3,"title":["A formal theory of simulations between infinite automata"],"prefix":"10.1007","volume":"3","author":[{"given":"Paul","family":"Loewenstein","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"CR1","doi-asserted-by":"crossref","unstructured":"Mike Gordon. HOL: A proof generating system for higher-order logic. InVLSI specification, Verification and Synthesis G. Birtwistle and P.A. Subrahmanyam (eds.), Kluwer Academic Publisers, 1988.","DOI":"10.1007\/978-1-4613-2007-4_3"},{"key":"CR2","unstructured":"Robert S. Boyer and J. Strother Moore.A Computational Logic. Academic Press, 1979."},{"key":"CR3","unstructured":"J.R. B\u00fcchi. On a decision method in rescricted second-order arithmetic. InProceedings International Congress on Logic, Methodology and Philosophy of Science, 1960, Stanford University Press, 1962, 1?12."},{"key":"CR4","first-page":"1","volume":"141","author":"M.O. Rabin","year":"1969","unstructured":"M.O. Rabin. Decidability of second-order theories and automata on infinite trees.Transactions American Mathematical Society, 141:1?35, 1969.","journal-title":"Transactions American Mathematical Society"},{"key":"CR5","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1109\/SWCT.1963.8","volume-title":"Switching Circuit Theory and Logical Design: Proceedings Fourth Annual Symposium","author":"D.E. Muller","year":"1963","unstructured":"D.E. Muller. Infinite sequences and finite machines. InSwitching Circuit Theory and Logical Design: Proceedings Fourth Annual Symposium, New York, 1963. Institute of Electrical and Electronic Engineers, 3?16"},{"key":"CR6","doi-asserted-by":"crossref","unstructured":"Paul Loewenstein. The formal verification of state-machines using higher-order logic. InIEEE International Conference on Computer Design, 1989.","DOI":"10.1109\/ICCD.1989.63356"},{"key":"CR7","doi-asserted-by":"crossref","unstructured":"Paul Loewenstein and David Dill. Formal verification of cache systems using refinement relations. InIEEE International Conference on Computer Design, 228?233, 1990.","DOI":"10.1109\/ICCD.1990.130211"},{"key":"CR8","doi-asserted-by":"crossref","first-page":"355","DOI":"10.1007\/BF00709156","volume":"1","author":"Paul Loewenstein","year":"1992","unstructured":"Paul Loewenstein and David L. Dill. Verification of a multiprocessor cache protocol using simulation relations and higher-order logic.Formal Methods in Systems Design, 1:355?383, 1992.","journal-title":"Formal Methods in Systems Design"},{"key":"CR9","unstructured":"R. Milner. An algebraic definition of simulation between programs. InProceedings 2nd International Joint Conference on Artificial Intelligence, 1971."},{"issue":"2","key":"CR10","doi-asserted-by":"crossref","first-page":"253","DOI":"10.1016\/0304-3975(91)90224-P","volume":"82","author":"Mart\u00edn Abadi","year":"1991","unstructured":"Mart\u00edn Abadi and Leslie Lamport. The existence of refinement mappings.Theoretical Computer Science, 82(2):253?284, May 1991.","journal-title":"Theoretical Computer Science"},{"key":"CR11","unstructured":"Nils Klarlund and Fred B. Schneider. Verifying safety properties using non-deterministic infinitestate automata. Technical Report TR 89-1037, Cornell University Computer Science Department, 1989."},{"key":"CR12","unstructured":"Mike Gordon. HOL: A machine oriented formulation of higher-order logic. Technical Report 68, University of Cambridge Computer Laboratory, 1985."},{"key":"CR13","unstructured":"Mike Fourman. Avoiding use of the axiom of choice. Private communication, 1990."},{"key":"CR14","unstructured":"Bowern Alpern and Fred B. Schneider. Recognizing safety and liveness. Technical Report TR 86-727, Department of Computer Science, Cornel University, 1986."},{"key":"CR15","unstructured":"Fred B. Schneider. Decomposing properties into safety and liveness using predicate logic. Technical Report TR 87-874, Department of Computer Science, Cornell University, 1987."},{"key":"CR16","doi-asserted-by":"crossref","first-page":"114","DOI":"10.4064\/fm-8-1-114-134","volume":"8","author":"D\u00e9nes K\u00f6nig","year":"1926","unstructured":"D\u00e9nes K\u00f6nig. Sur les correspondances multivoques des ensembles.Fundamenta Mathematicae, 8:114?134, 1926.","journal-title":"Fundamenta Mathematicae"},{"key":"CR17","unstructured":"T.F. Melham. Inductive relation definitions in HOL. InInternational Workshop on the HOL Theorem Proving System and its Applications. IEEE Computer Society Press, 1991."}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF01383986.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/BF01383986\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF01383986","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,2]],"date-time":"2019-05-02T12:04:48Z","timestamp":1556798688000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BF01383986"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1993,8]]},"references-count":17,"journal-issue":{"issue":"1-2","published-print":{"date-parts":[[1993,8]]}},"alternative-id":["BF01383986"],"URL":"https:\/\/doi.org\/10.1007\/bf01383986","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"value":"0925-9856","type":"print"},{"value":"1572-8102","type":"electronic"}],"subject":[],"published":{"date-parts":[[1993,8]]}}}