{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,11]],"date-time":"2025-10-11T17:10:47Z","timestamp":1760202647688},"publisher-location":"Berlin, Heidelberg","reference-count":20,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540580430"},{"type":"electronic","value":"9783540484233"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1994]]},"DOI":"10.1007\/3-540-58043-3_22","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T15:10:08Z","timestamp":1330269008000},"page":"273-346","source":"Crossref","is-referenced-by-count":27,"title":["Temporal verification of simulation and refinement"],"prefix":"10.1007","author":[{"given":"Yonit","family":"Kesten","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Zohar","family":"Manna","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Amir","family":"Pnueli","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,6,7]]},"reference":[{"key":"7_CR1","doi-asserted-by":"crossref","unstructured":"M. Abadi and L. Lamport. The existence of refinement mappings. In Proc. 3rd IEEE Symp. Logic in Comp. Sci., pages 165\u2013175, 1988.","DOI":"10.1109\/LICS.1988.5115"},{"key":"7_CR2","doi-asserted-by":"crossref","first-page":"207","DOI":"10.1007\/BF01257083","volume":"20","author":"M. Ben-Ari","year":"1983","unstructured":"M. Ben-Ari, Z. Manna, and A. Pnueli. The temporal logic of branching time. Acta Informatica, 20:207\u2013226, 1983.","journal-title":"Acta Informatica"},{"key":"7_CR3","doi-asserted-by":"crossref","unstructured":"H. Barringer, R. Kuiper, and A. Pnueli. A really abstract concurrent model and its temporal logic. In Proc. 13th ACM Symp. Princ. of Prog. Lang., pages 173\u2013183, 1986.","DOI":"10.1145\/512644.512660"},{"key":"7_CR4","doi-asserted-by":"crossref","unstructured":"J.W. de Bakker, W.-P. de Roever, and G. Rozenberg, editors. Stepwise Refinement of Distributed Systems: Models, Formalism, Correctness. Lecture Notes in Computer Science 430. Springer-Verlag, 1990.","DOI":"10.1007\/3-540-52559-9"},{"key":"7_CR5","unstructured":"E. Diepstraten and R. Kuiper. Abadi, Lamport, and Stark: Towards a proof theory for stuttering, dense domains and refinmement mappings. In J.W. de Bakker, W.-P. de Roever, and G. Rozenberg, editors, Stepwise Refinement of Distributed Systems: Models, Formalism, Correctness, Lecture Notes in Computer Science 430, pages 208\u2013238. Springer-Verlag, 1990."},{"key":"7_CR6","doi-asserted-by":"crossref","unstructured":"D. Gabbay, A. Pnueli, S. Shelah, and J. Stavi. On the temporal analysis of fairness. In Proc. 7th ACM Symp. Princ. of Prog. Lang., pages 163\u2013173, 1980.","DOI":"10.1145\/567446.567462"},{"key":"7_CR7","doi-asserted-by":"crossref","first-page":"190","DOI":"10.1145\/69624.357207","volume":"5","author":"L. Lamport","year":"1983","unstructured":"L. Lamport. Specifying concurrent program modules. ACM Trans. Prog. Lang. Sys., 5:190\u2013222, 1983.","journal-title":"ACM Trans. Prog. Lang. Sys."},{"key":"7_CR8","unstructured":"L. Lamport. What good is temporal logic. In R.E.A. Mason, editor, Proc. IFIP 9th World Congress, pages 657\u2013668. North-Holland, 1983."},{"key":"7_CR9","unstructured":"L. Lamport. The temporal logic of actions. Technical Report 79, Digital Equipment Corporation, Systems Research Center, 1991. To appear in Transactions on Programming Languages and Systems."},{"key":"7_CR10","unstructured":"L. Lamport. The existence of refinement mapping. TLA Note 92-03-19, March 1992."},{"key":"7_CR11","doi-asserted-by":"crossref","unstructured":"O. Lichtenstein, A. Pnueli, and L. Zuck. The glory of the past. In Proc. Conf. Logics of Programs, volume 193 of Lect. Notes in Comp. Sci., pages 196\u2013218. Springer-Verlag, 1985.","DOI":"10.1007\/3-540-15648-8_16"},{"key":"7_CR12","doi-asserted-by":"crossref","unstructured":"Z. Manna and A. Pnueli. How to cook a temporal proof system for your pet language. In Proc. 10th ACM Symp. Princ. of Prog. Lang., pages 141\u2013154, 1983.","DOI":"10.1145\/567067.567082"},{"key":"7_CR13","doi-asserted-by":"crossref","first-page":"257","DOI":"10.1016\/0167-6423(84)90003-0","volume":"32","author":"Z. Manna","year":"1984","unstructured":"Z. Manna and A. Pnueli. Adequate proof principles for invariance and liveness properties of concurrent programs. Sci. Comp. Prog., 32:257\u2013289, 1984.","journal-title":"Sci. Comp. Prog."},{"issue":"1","key":"7_CR14","doi-asserted-by":"crossref","first-page":"97","DOI":"10.1016\/0304-3975(91)90041-Y","volume":"83","author":"Z. Manna","year":"1991","unstructured":"Z. Manna and A. Pnueli. Completing the temporal picture. Theor. Comp. Sci., 83(1):97\u2013130, 1991.","journal-title":"Theor. Comp. Sci."},{"key":"7_CR15","volume-title":"The Temporal Logic of Reactive and Concurrent Systems: Specification","author":"Z. Manna","year":"1991","unstructured":"Z. Manna and A. Pnueli. The Temporal Logic of Reactive and Concurrent Systems: Specification. Springer-Verlag, New York, 1991."},{"key":"7_CR16","volume-title":"Temporal Verification of Reactive Systems","author":"Z. Manna","year":"1994","unstructured":"Z. Manna and A. Pnueli. Temporal Verification of Reactive Systems. Springer-Verlag, New York, 1994. To appear."},{"key":"7_CR17","doi-asserted-by":"crossref","unstructured":"A. Pnueli. System specification and refinement in temporal logic. In R.K. Shyamasundar, editor, Foundations of Software Technology and Theoretical Computer Science, volume 652 of Lect. Notes in Comp. Sci., pages 1\u201338. Springer-Verlag, 1992.","DOI":"10.1007\/3-540-56287-7_92"},{"key":"7_CR18","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/0304-3975(81)90110-9","volume":"13","author":"A. Pnueli","year":"81","unstructured":"A. Pnueli. The temporal semantics of concurrent programs. Theoretical Computer Science, 13:1\u201320, 81.","journal-title":"Theoretical Computer Science"},{"key":"7_CR19","unstructured":"E.W. Stark. Foundations of a Theory of Specifications for Distributed Systems. PhD thesis, M.I.T, 1984."},{"key":"7_CR20","doi-asserted-by":"crossref","first-page":"135","DOI":"10.1016\/0304-3975(86)90007-1","volume":"56","author":"E.W. Stark","year":"1988","unstructured":"E.W. Stark. Proving entailments between conceptual state specifications. Theor. Comp. Sci., 56:135\u2013154, 1988.","journal-title":"Theor. Comp. Sci."}],"container-title":["Lecture Notes in Computer Science","A Decade of Concurrency Reflections and Perspectives"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-58043-3_22.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,28]],"date-time":"2021-04-28T01:10:43Z","timestamp":1619572243000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-58043-3_22"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1994]]},"ISBN":["9783540580430","9783540484233"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/3-540-58043-3_22","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1994]]}}}