{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,19]],"date-time":"2024-09-19T15:25:39Z","timestamp":1726759539736},"publisher-location":"Berlin, Heidelberg","reference-count":29,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540564966"},{"type":"electronic","value":"9783540475729"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1993]]},"DOI":"10.1007\/3-540-56496-9_21","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T11:12:51Z","timestamp":1330254771000},"page":"260-273","source":"Crossref","is-referenced-by-count":36,"title":["Property preserving simulations"],"prefix":"10.1007","author":[{"given":"S.","family":"Bensalem","sequence":"first","affiliation":[]},{"given":"A.","family":"Bouajjani","sequence":"additional","affiliation":[]},{"given":"C.","family":"Loiseaux","sequence":"additional","affiliation":[]},{"given":"J.","family":"Sifakis","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,5,30]]},"reference":[{"key":"21_CR1","unstructured":"M. Abadi and L. Lamport. The existence of Refinement Mappings. SRC 29, Digital Equipment Corpoiation, Systems Research Center, August 1988."},{"key":"21_CR2","doi-asserted-by":"crossref","unstructured":"A. Bouajjani, J.C. Fernandez, S. Graf, C. Rodriguez, and J. Sifakis. Safety for branching time semantics. In J.L. Albert, B. Monein, and M.R. Artalejo, editors, 18th ICALP, pages 76\u201392, LNCS 510, Springer-Verlag, October 1991.","DOI":"10.1007\/3-540-54233-7_126"},{"key":"21_CR3","volume-title":"RTC 15","author":"A. Bouajjani","year":"1989","unstructured":"A. Bouajjani. From Linear-Time Propositional Temporal Logics to a Branching-Time \u03bc-calculus. RTC 15, LGI-IMAG, Grenoble, 1989."},{"key":"21_CR4","volume-title":"RC 7206 30923","author":"D. Brand","year":"1978","unstructured":"D. Brand. Algebraic simulation between parallel programs. RC 7206 30923, IBM, Yorktown Heights, 1978."},{"key":"21_CR5","unstructured":"J.R. B\u00fcchi. On a decision method in restricted second order arithmetic. In Intern. Cong. Logic, Method and Philos. Sci., Stantford Univ. Press, 1962."},{"key":"21_CR6","doi-asserted-by":"crossref","unstructured":"P. Cousot and R. Cousot. Systematic design of program analysis framework. In Proc. 6th ACM Symp. on Principle of Programming Languages, 1979.","DOI":"10.1145\/567752.567778"},{"key":"21_CR7","unstructured":"P. Cousot and R. Cousot. Comparing the Galois Connection and Widening\/Narrowing Approaches to Abstract Interpretation. Technical Report, LIX, Ecole Polytechnique, May 1990."},{"issue":"2","key":"21_CR8","doi-asserted-by":"crossref","first-page":"244","DOI":"10.1145\/5397.5399","volume":"8","author":"E. M. Clarke","year":"1986","unstructured":"E. M. Clarke, E. A. Emerson, and E. Sistla. Automatic Verification of Finite State Concurrent Systems using Temporal Logic Specifications: A Practical Approach. In 10th Symposium on Principles of Programming Languages (POPL 83), ACM, 1983. Complete version published in ACM TOPLAS, 8(2):244\u2013263, April 1986.","journal-title":"ACM TOPLAS"},{"key":"21_CR9","doi-asserted-by":"crossref","unstructured":"E.M. Clarke, O. Grumberg, and D.E. Long. Model checking and abstraction. In Symposium on Principles of Programming Languages (POPL 92), ACM, October 1992.","DOI":"10.1145\/143165.143235"},{"key":"21_CR10","doi-asserted-by":"crossref","unstructured":"E.A. Emerson and J. Y. Halpern, 'sometimes\u2019 and\u2019 not never\u2019 revisited: on branching versus linear time logic. In 10th. Annual Symp. on Principles of Programming Languages, 1983.","DOI":"10.1145\/567067.567081"},{"key":"21_CR11","doi-asserted-by":"crossref","unstructured":"S. Graf and J. Sifakis. A logic for the specification and proof of regular controllable processes of CCS. Acta Informatica, 23, 1986.","DOI":"10.1007\/BF00288467"},{"key":"21_CR12","doi-asserted-by":"crossref","unstructured":"S. Graf and J. Sifakis. A modal characterization of observational congruence on finite terms of CCS. Information and Control, 68, 1986.","DOI":"10.1016\/S0019-9958(86)80031-6"},{"key":"21_CR13","doi-asserted-by":"crossref","first-page":"137","DOI":"10.1145\/2455.2460","volume":"32","author":"M. Hennessy","year":"1985","unstructured":"M. Hennessy and R. Milner. Algebraic laws for nondeterminism and concurrency. Journal of the Association for Computing Machinery, 32:137\u2013161, 1985.","journal-title":"Journal of the Association for Computing Machinery"},{"key":"21_CR14","volume-title":"RC 7796 33742","author":"T. Kasai","year":"1979","unstructured":"T. Kasai and R.E. Miller. Homomorphisms between models of parallel computation. RC 7796 33742, IBM, Yorktown Heights, 1979."},{"key":"21_CR15","doi-asserted-by":"crossref","unstructured":"D. Kozen. Results on the propositional \u03bc-calculus. In Theoretical Computer Science, North-Holland, 1983.","DOI":"10.1016\/0304-3975(82)90125-6"},{"key":"21_CR16","unstructured":"R.P. Kurshan. Analysis of Discrete Event Coordination. LNCS 430, Springer-Verlag, May 1989."},{"issue":"2","key":"21_CR17","doi-asserted-by":"crossref","first-page":"125","DOI":"10.1109\/TSE.1977.229904","volume":"SE-3","author":"L. Lamport","year":"1977","unstructured":"L. Lamport. Proving the correctness of multiprocess programs. IEEE Transactions on Software Engineering, SE-3(2):125\u2013143, 1977.","journal-title":"IEEE Transactions on Software Engineering"},{"key":"21_CR18","doi-asserted-by":"crossref","unstructured":"O. Lichtenstein, A. Pnueli, and L. Zuck. The glory of the past. In Conference on Logics of Programs, LNCS 194, Springer Verlag, 1985.","DOI":"10.1007\/3-540-15648-8_16"},{"key":"21_CR19","volume-title":"MIT\/LCS\/TM 373","author":"N. A. Lynch","year":"1988","unstructured":"N.A. Lynch and M.R. Tuttle. An introduction to Input\/Ouput Automata. MIT\/LCS\/TM 373, MIT, Cambridge, Massachussetts, November 1988."},{"key":"21_CR20","unstructured":"R. Milner. An algebraic definition of simulation between programs. In Proc. Second Int. Joint Conf. on Artificial Intelligence, pages 481\u2013489, BCS, 1971."},{"key":"21_CR21","doi-asserted-by":"crossref","unstructured":"Z. Manna and A. Pnueli. A hierarchy of temporal properties. In Proc. 9th ACM Symp. on Princ. of Dist. Comp., 1990.","DOI":"10.1145\/93385.93442"},{"key":"21_CR22","doi-asserted-by":"crossref","unstructured":"R. De Nicola and F. Vaandrager. Three logics for branching bisimulation. In Proc. of Fifth Symp. on Logic in Computer Science, Computer Society Press, 1990.","DOI":"10.1109\/LICS.1990.113739"},{"key":"21_CR23","doi-asserted-by":"crossref","first-page":"493","DOI":"10.1090\/S0002-9947-1944-0010555-7","volume":"55","author":"O. Ore","year":"1944","unstructured":"O. Ore. Galois connexions. Trans. Amer. Math. Soc, 55:493\u2013513, February 1944.","journal-title":"Trans. Amer. Math. Soc"},{"key":"21_CR24","doi-asserted-by":"crossref","first-page":"45","DOI":"10.1016\/0304-3975(81)90110-9","volume":"13","author":"A. Pnueli","year":"1981","unstructured":"A. Pnueli. The Temporal Logic of Programs. In 18th Symposium on Foundations of Computer Science (FOCS 77), IEEE, 1977. Revised version published in Theoretical Computer Science, 13:45\u201360, 1981.","journal-title":"Theoretical Computer Science"},{"issue":"nomber4","key":"21_CR25","first-page":"339","volume":"11","author":"Luis E. E. Sanchis","year":"1977","unstructured":"Luis E. Sanchis. Data types as lattices: retractions, projection and projection. In RAIRO Theorical computer science, vol 11, nomber 4, pages 339\u2013344, 1977.","journal-title":"RAIRO Theorical computer science"},{"key":"21_CR26","unstructured":"J. Sifakis. Property preserving homomorphisms and a notion of simulation of transition systems. RR IMAG 332, IMAG, November 1982."},{"key":"21_CR27","doi-asserted-by":"crossref","unstructured":"J. Sifakis. A unified approach for studying the properties of transition systems. Theorical Computer Science, 18, 1982.","DOI":"10.1016\/0304-3975(82)90067-6"},{"key":"21_CR28","doi-asserted-by":"crossref","unstructured":"J. Sifakis. Property preserving homomorphisms of transition systems. In E. Clarke and D. Kozen, editors, Workshop on logics of programs, LNCS 164, Springer-Verlag, 1983.","DOI":"10.1007\/3-540-12896-4_381"},{"key":"21_CR29","doi-asserted-by":"crossref","unstructured":"P. Wolper. Temporal logic can be more expreessive. Inform. Contr., 56, 1983.","DOI":"10.1016\/S0019-9958(83)80051-5"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-56496-9_21.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T21:04:01Z","timestamp":1605647041000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-56496-9_21"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1993]]},"ISBN":["9783540564966","9783540475729"],"references-count":29,"URL":"https:\/\/doi.org\/10.1007\/3-540-56496-9_21","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1993]]}}}