{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,27]],"date-time":"2025-10-27T20:35:30Z","timestamp":1761597330396},"publisher-location":"Berlin, Heidelberg","reference-count":28,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540631415"},{"type":"electronic","value":"9783540691884"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1997]]},"DOI":"10.1007\/3-540-63141-0_19","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T23:09:10Z","timestamp":1330297750000},"page":"273-287","source":"Crossref","is-referenced-by-count":34,"title":["Fair simulation"],"prefix":"10.1007","author":[{"given":"Thomas A.","family":"Henzinger","sequence":"first","affiliation":[]},{"given":"Orna","family":"Kupferman","sequence":"additional","affiliation":[]},{"given":"Sriram K.","family":"Rajamani","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,6,7]]},"reference":[{"key":"19_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:253\u2013284, 1991.","journal-title":"Theoretical Computer Science"},{"key":"19_CR2","doi-asserted-by":"crossref","unstructured":"A. Aziz, V. Singhal, F. Balarin, R.K. Brayton, and A.L. Sangiovanni-Vincentelli. Equivalences for fair Kripke structures. In Proc. 21st ICALP, Springer LNCS 820, pp. 364\u2013375, 1994.","DOI":"10.1007\/3-540-58201-0_82"},{"key":"19_CR3","doi-asserted-by":"crossref","unstructured":"S. Bensalem, A. Bouajjani, C. Loiseaux, and J. Sifakis. Property-preserving simulations. In Proc. 4th CAV, Springer LNCS 663, pp. 260\u2013273, 1992.","DOI":"10.1007\/3-540-56496-9_21"},{"key":"19_CR4","unstructured":"J.A. Bergstra, J.W. Klop, and E.R. Olderog. Failures without chaos: a new process semantics for fair abstraction. In Proc. 3rd IFIP FDPC, Elsevier, pp. 77\u2013103, 1987."},{"key":"19_CR5","doi-asserted-by":"crossref","first-page":"189","DOI":"10.1016\/0167-6423(95)00003-B","volume":"24","author":"B. Bloom","year":"1996","unstructured":"B. Bloom and R. Paige. Transformational design and implementation of a new efficient solution to the ready simulation problem. Science of Computer Programming, 24:189\u2013220, 1996.","journal-title":"Science of Computer Programming"},{"key":"19_CR6","doi-asserted-by":"crossref","unstructured":"E. Brinksma, A. Rensink, and W. Vogler. Fair testing. In Proc. 6th CONCUR, Springer LNCS 962, pp. 313\u2013327, 1995.","DOI":"10.1007\/3-540-60218-6_23"},{"key":"19_CR7","doi-asserted-by":"crossref","unstructured":"O. Bernholtz, M.Y. Vardi, and P. Wolper. An automata-theoretic approach to branching-time model checking. In Proc. 6th CAV, Springer LNCS 818, pp. 142\u2013155, 1994.","DOI":"10.1007\/3-540-58179-0_50"},{"key":"19_CR8","doi-asserted-by":"publisher","first-page":"244","DOI":"10.1145\/5397.5399","volume":"8","author":"E.M. Clarke","year":"1986","unstructured":"E.M. Clarke, E.A. Emerson, and A.P. Sistla. Automatic verification of finite-state concurrent systems using temporal-logic specifications. ACM Transactions on Programming Languages and Systems, 8:244\u2013263, 1986.","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"19_CR9","doi-asserted-by":"crossref","first-page":"36","DOI":"10.1145\/151646.151648","volume":"15","author":"R.J. Cleaveland","year":"1993","unstructured":"R.J. Cleaveland, J. Parrow, and B. Steffen. The Concurrency Workbench: a semantics-based tool for the verification of finite-state systems. ACM Transactions on Programming Languages and Systems, 15:36\u201372, 1993.","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"19_CR10","doi-asserted-by":"crossref","unstructured":"D. Dill, A.J. Hu, and H. Wong-Toi. Checking for language inclusion using simulation relations. In Proc. 3rd CAV, Springer LNCS 575, pp. 255\u2013265, 1991.","DOI":"10.1007\/3-540-55179-4_25"},{"key":"19_CR11","doi-asserted-by":"crossref","unstructured":"E.A. Emerson and C. Jutla. The complexity of tree automata and logics of programs. In Proc. 29th FOCS, IEEE Computer Society, pp. 368\u2013377, 1988.","DOI":"10.1109\/SFCS.1988.21949"},{"key":"19_CR12","doi-asserted-by":"crossref","first-page":"843","DOI":"10.1145\/177492.177725","volume":"16","author":"O. Grumberg","year":"1994","unstructured":"O. Grumberg and D.E. Long. Model checking and modular verification. ACM Transactions on Programming Languages and Systems, 16:843\u2013871, 1994.","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"19_CR13","doi-asserted-by":"crossref","first-page":"121","DOI":"10.1016\/0304-3975(87)90004-1","volume":"49","author":"M.C.B. Hennessy","year":"1987","unstructured":"M.C.B. Hennessy. An algebraic theory of fair asynchronous communicating processes. Theoretical Computer Science, 49:121\u2013143, 1987.","journal-title":"Theoretical Computer Science"},{"key":"19_CR14","doi-asserted-by":"crossref","unstructured":"M.R. Henzinger, T.A. Henzinger, and P.W. Kopke. Computing simulations on finite and infinite graphs. In Proc. S6th FOCS, IEEE Computer Society, pp. 453\u2013462, 1995.","DOI":"10.1109\/SFCS.1995.492576"},{"key":"19_CR15","volume-title":"PhD thesis","author":"R. Hojati","year":"1996","unstructured":"R. Hojati. A BDD-based Environment for Formal Verification of Hardware Systems. PhD thesis, EECS Department, University of California, Berkeley, 1996."},{"key":"19_CR16","doi-asserted-by":"crossref","unstructured":"O. Kupferman and M.Y. Vardi. Verification of fair transition systems. In Proc. 8th CAV, Springer LNCS 1102, pp. 372\u2013382, 1996.","DOI":"10.1007\/3-540-61474-5_84"},{"key":"19_CR17","doi-asserted-by":"publisher","first-page":"190","DOI":"10.1145\/69624.357207","volume":"5","author":"L. Lamport","year":"1983","unstructured":"L. Lamport. Specifying concurrent program modules. ACM Transactions on Programming Languages and Systems, 5:190\u2013222, 1983.","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"19_CR18","unstructured":"N.A. Lynch and R. Segala. A comparison of simulation techniques and algebraic techniques for verifying concurrent systems. Technical Report MIT\/LCS\/TM-499, Laboratory for Computer Science, MIT, 1993."},{"key":"19_CR19","doi-asserted-by":"crossref","unstructured":"N.A. Lynch and M.R. Tuttle. Hierarchical correctness proofs for distributed algorithms. In Proc. 6th PODC, ACM, pp. 137\u2013151, 1987.","DOI":"10.1145\/41840.41852"},{"key":"19_CR20","unstructured":"N.A. Lynch. Distributed Algorithms. Morgan-Kaufmann, 1996."},{"key":"19_CR21","unstructured":"R. Milner. An algebraic definition of simulation between programs. In Proc. 2nd IJCAI, British Computer Society, pp. 481\u2013489, 1971."},{"key":"19_CR22","doi-asserted-by":"crossref","unstructured":"V. Natarajan and R.J. Cleaveland. Divergence and fair testing. In Proc. 22nd ICALP, Springer LNCS 944, pp. 648\u2013659, 1995.","DOI":"10.1007\/3-540-60084-1_112"},{"key":"19_CR23","doi-asserted-by":"crossref","unstructured":"A. Pnueli. Linear and branching structures in the semantics and logics of reactive systems. In Proc. 12th ICALP, Springer LNCS 194, pp. 15\u201332, 1985.","DOI":"10.1007\/BFb0015727"},{"key":"19_CR24","doi-asserted-by":"crossref","unstructured":"A. Pnueli and R. Rosner. On the synthesis of a reactive module. In Proc. 16th POPL, ACM, pp. 179\u2013190, 1989.","DOI":"10.1145\/75277.75293"},{"key":"19_CR25","doi-asserted-by":"crossref","unstructured":"M.O. Rabin. Weakly definable relations and special automata. In Proc. Mathematical Logic and Foundations of Set Theory, Elsevier, pp. 1\u201323, 1970.","DOI":"10.1016\/S0049-237X(08)71929-3"},{"key":"19_CR26","doi-asserted-by":"crossref","unstructured":"S. Safra. On the complexity of \u03c9-automata. In Proc. 29th FOCS, IEEE Computer Society, pp. 319\u2013327, 1988.","DOI":"10.1109\/SFCS.1988.21948"},{"key":"19_CR27","doi-asserted-by":"crossref","unstructured":"L.J. Stockmeyer and A.R. Meyer. Word problems requiring exponential time. In Proc. 5th STOC, ACM, pp. 1\u20139, 1973.","DOI":"10.1145\/800125.804029"},{"key":"19_CR28","doi-asserted-by":"publisher","first-page":"217","DOI":"10.1016\/0304-3975(87)90008-9","volume":"49","author":"A.P. Sistla","year":"1987","unstructured":"A.P. Sistla, M.Y. Vardi, and P. Wolper. The complementation problem for Buchi automata with applications to temporal logic. Theoretical Computer Science, 49:217\u2013237, 1987.","journal-title":"Theoretical Computer Science"}],"container-title":["Lecture Notes in Computer Science","CONCUR '97: Concurrency Theory"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-63141-0_19.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T21:16:07Z","timestamp":1605647767000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-63141-0_19"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1997]]},"ISBN":["9783540631415","9783540691884"],"references-count":28,"URL":"https:\/\/doi.org\/10.1007\/3-540-63141-0_19","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1997]]}}}