{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T22:38:01Z","timestamp":1725489481404},"publisher-location":"Berlin, Heidelberg","reference-count":38,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540414131"},{"type":"electronic","value":"9783540444503"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2000]]},"DOI":"10.1007\/3-540-44450-5_12","type":"book-chapter","created":{"date-parts":[[2007,8,16]],"date-time":"2007-08-16T04:26:08Z","timestamp":1187238368000},"page":"151-163","source":"Crossref","is-referenced-by-count":2,"title":["Fair Equivalence Relations"],"prefix":"10.1007","author":[{"given":"Orna","family":"Kupferman","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Nir","family":"Piterman","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Moshe Y.","family":"Vardi","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2000,11,24]]},"reference":[{"issue":"2","key":"12_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. TCS, 82(2):253\u2013284, 1991.","journal-title":"TCS"},{"key":"12_CR2","doi-asserted-by":"crossref","unstructured":"A. Aziz, V._Singhal, F. Balarin, R. Brayton, and A.L. Sangiovanni-Vincentelli. Equivalences for fair kripke structures. In Proc. 21st ICALP, Jerusalem, Israel, July 1994.","DOI":"10.1007\/3-540-58201-0_82"},{"key":"12_CR3","doi-asserted-by":"publisher","first-page":"115","DOI":"10.1016\/0304-3975(88)90098-9","volume":"59","author":"M.C. Browne","year":"1988","unstructured":"M.C. Browne, E.M. Clarke, and O. Grumberg. Characterizing finite Kripke structures in propositional temporal logic. TCS, 59:115\u2013131, 1988.","journal-title":"TCS"},{"key":"12_CR4","doi-asserted-by":"crossref","unstructured":"D. Bustan and O. Grumberg. Simulation based minimization. In Proc. 17th ICAD, Pittsburgh, PA, June 2000.","DOI":"10.1007\/10721959_20"},{"issue":"6","key":"12_CR5","doi-asserted-by":"publisher","first-page":"638","DOI":"10.1007\/BF03180566","volume":"4","author":"J. Balcazar","year":"1992","unstructured":"J. Balcazar, J. Gabarro, and M. Santha. Deciding bisimilarity is P-complete. Formal Aspects of Computing, 4(6):638\u2013648, 1992.","journal-title":"Formal Aspects of Computing"},{"issue":"2","key":"12_CR6","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(2):244\u2013263, January 1986.","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"12_CR7","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","DOI":"10.1007\/BFb0028174","volume-title":"Exploiting symmetry in temporal logic model checking","author":"E.M. Clarke","year":"1993","unstructured":"E.M. Clarke, T. Filkorn, and S. Jha. Exploiting symmetry in temporal logic model checking. In Proc. 5th CAV, LNCS 697, 1993."},{"key":"12_CR8","doi-asserted-by":"publisher","first-page":"36","DOI":"10.1145\/151646.151648","volume":"15","author":"R. Cleaveland","year":"1993","unstructured":"R. Cleaveland, J. Parrow, and B. Steffen. The concurrency workbench: A semanticsbased tool for the verification of concurrent systems. ACM Trans. on Programming Languages and Systems, 15:36\u201372, 1993.","journal-title":"ACM Trans. on Programming Languages and Systems"},{"key":"12_CR9","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"255","DOI":"10.1007\/3-540-55179-4_25","volume-title":"Checking for language inclusion using simulation relations","author":"D.L. Dill","year":"1992","unstructured":"D.L. Dill, A.J. Hu, and H. Wong-Toi. Checking for language inclusion using simulation relations. In Proc. 3rd CAV, LNCS 575, pp. 255\u2013265, 1991."},{"key":"12_CR10","doi-asserted-by":"crossref","unstructured":"S. Dziembowski, M. Jurdzinski, and I. Walukiewicz. How much memory is needed to win infinite games. In Proc. 12th LICS, pp. 99\u2013110, 1997.","DOI":"10.1109\/LICS.1997.614939"},{"key":"12_CR11","doi-asserted-by":"crossref","unstructured":"E.A. Emerson and C. Jutla. Tree automata, \u03bc-calculus and determinacy. In Proc. 32nd FOCS, pp. 368\u2013377, 1991.","DOI":"10.1109\/SFCS.1991.185392"},{"key":"12_CR12","doi-asserted-by":"crossref","unstructured":"N. Francez. Fairness. Texts and Monographs in Computer Science. Springer-Verlag, 1986.","DOI":"10.1007\/978-1-4612-4886-6"},{"issue":"3","key":"12_CR13","doi-asserted-by":"publisher","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 Trans. on Programming Languages and Systems, 16(3):843\u2013871, 1994.","journal-title":"ACM Trans. on Programming Languages and Systems"},{"key":"12_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. 36th FOCS, pp. 453\u2013462, 1995.","DOI":"10.1109\/SFCS.1995.492576"},{"key":"12_CR15","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"273","DOI":"10.1007\/3-540-63141-0_19","volume-title":"Fair simulation","author":"T.A. Henzinger","year":"1997","unstructured":"T.A. Henzinger, O. Kupferman, and S. Rajamani. Fair simulation. In Proc. 8th Conference on Concurrency Theory, LNCS 1243, pp. 273\u2013287, 1997."},{"key":"12_CR16","unstructured":"R. Hojati. A BDD-based Environment for Formal Verification of Hardware Systems. PhD thesis, University of California at Berkeley, 1996."},{"key":"12_CR17","series-title":"Lect Notes Comput Sci","volume-title":"Fair bisimulation","author":"T. Henzinger","year":"2000","unstructured":"T. Henzinger and S. Rajamani. Fair bisimulation. In Proc. 4th TACAS, LNCS 1785, pp. 299\u2013314, 2000."},{"key":"12_CR18","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"263","DOI":"10.1007\/3-540-61604-7_60","volume-title":"On the expressive completeness of the propositional \u03bc-calculus with respect to the monadic second order logic","author":"D. Janin","year":"1996","unstructured":"D. Janin and I. Walukiewicz. On the expressive completeness of the propositional \u03bc-calculus with respect to the monadic second order logic. In Proc. 7th Conference on Concurrency Theory, LNCS 1119, pp. 263\u2013277, 1996."},{"key":"12_CR19","doi-asserted-by":"publisher","first-page":"217","DOI":"10.1016\/0304-3975(85)90043-X","volume":"36","author":"M. Kaminski","year":"1985","unstructured":"M. Kaminski. A classification of \u03c9-regular languages. TCS, 36:217\u2013229, 1985.","journal-title":"TCS"},{"key":"12_CR20","doi-asserted-by":"crossref","unstructured":"O. Kupferman, S. Safra, and M.Y. Vardi. Relating word and tree automata. In Proc. 11th LICS, pp. 322\u2013333, 1996.","DOI":"10.1109\/LICS.1996.561360"},{"key":"12_CR21","doi-asserted-by":"crossref","unstructured":"R.P. Kurshan. Computer Aided Verification of Coordinating Processes. Princeton Univ. Press, 1994.","DOI":"10.1515\/9781400864041"},{"key":"12_CR22","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"381","DOI":"10.1007\/3-540-49213-5_14","volume-title":"Modular model checking","author":"O. Kupferman","year":"1998","unstructured":"O. Kupferman and M.Y. Vardi. Modular model checking. In Proc. Compositionality Workshop, LNCS 1536, pp. 381\u2013401, 1998."},{"key":"12_CR23","unstructured":"O. Kupferman and M.Y. Vardi. Verification of fair transition systems. Chicago Journal of TCS, 1998(2)."},{"key":"12_CR24","doi-asserted-by":"crossref","unstructured":"O. Kupferman and M.Y. Vardi. Weak alternating automata and tree automata emptiness. In Proc. 30th STOC, pp. 224\u2013233, 1998.","DOI":"10.1145\/276698.276748"},{"key":"12_CR25","doi-asserted-by":"crossref","unstructured":"N. A. Lynch and M.R. Tuttle. Hierarchical correctness proofs for distributed algorithms. In Proc. 6th PODC, pp. 137\u2013151, 1987.","DOI":"10.1145\/41840.41852"},{"key":"12_CR26","doi-asserted-by":"crossref","unstructured":"K.L. McMillan. Symbolic Model Checking. Kluwer Academic Publishers, 1993.","DOI":"10.1007\/978-1-4615-3190-6"},{"key":"12_CR27","unstructured":"R. Milner. An algebraic definition of simulation between programs. In Proc. 2nd International Joint Conference on Artificial Intelligence, pp. 481\u2013489, 1971."},{"key":"12_CR28","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-10235-3","volume-title":"A Calculus of Communicating Systems","author":"R. Milner","year":"1980","unstructured":"R. Milner. A Calculus of Communicating Systems, LNCS 92, 1980."},{"key":"12_CR29","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4612-0931-7","volume-title":"The Temporal Logic of Reactive and Concurrent Systems: Specification","author":"Z. Manna","year":"1992","unstructured":"Z. Manna and A. Pnueli. The Temporal Logic of Reactive and Concurrent Systems: Specification. Springer-Verlag, Berlin, January 1992."},{"key":"12_CR30","doi-asserted-by":"crossref","unstructured":"A.R. Meyer and L.J. Stockmeyer. The equivalence problem for regular expressions with squaring requires exponential time. In Proc. 13th SWAT, pp. 125\u2013129, 1972.","DOI":"10.1109\/SWAT.1972.29"},{"issue":"1-2","key":"12_CR31","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/S0304-3975(97)00039-X","volume":"189","author":"D. Niwi\u0144ski","year":"1997","unstructured":"D. Niwi\u0144ski. Fixed point characterization of infinite behavior of finite-state systems. TCS, 189(1-2):1\u201369, December 1997.","journal-title":"TCS"},{"key":"12_CR32","series-title":"Lect Notes Comput Sci","volume-title":"Relating hierarchies of word and tree automata","author":"D. Niwinski","year":"1998","unstructured":"D. Niwinski and I. Walukiewicz. Relating hierarchies of word and tree automata. In Symposium on Theoretical Aspects in Computer Science, LNCS 1373, 1998."},{"key":"12_CR33","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"15","DOI":"10.1007\/BFb0015727","volume-title":"Linear and branching structures in the semantics and logics of reactive systems","author":"A. Pnueli","year":"1985","unstructured":"A. Pnueli. Linear and branching structures in the semantics and logics of reactive systems. In Proc. 12th ICALP, LNCS 194 pp. 15\u201332, 1985."},{"key":"12_CR34","doi-asserted-by":"publisher","first-page":"1","DOI":"10.2307\/1995086","volume":"141","author":"M.O. Rabin","year":"1969","unstructured":"M.O. Rabin. Decidability of second order theories and automata on infinite trees. Transaction of the AMS, 141:1\u201335, 1969.","journal-title":"Transaction of the AMS"},{"key":"12_CR35","doi-asserted-by":"crossref","unstructured":"M.O. Rabin. Weakly definable relations and special automata. In Proc. Symp. Math. Logic and Foundations of Set Theory, pp. 1\u201323. North Holland, 1970.","DOI":"10.1016\/S0049-237X(08)71929-3"},{"key":"12_CR36","doi-asserted-by":"crossref","unstructured":"S. Safra and M.Y. Vardi. On \u03c9-automata and temporal logic. In Proc. 21st STOC, pp. 127\u2013137, 1989.","DOI":"10.1145\/73007.73019"},{"key":"12_CR37","doi-asserted-by":"crossref","unstructured":"W. Thomas. Automata on infinite objects. Handbook of Theoretical Computer Science, pp. 165\u2013191, 1990.","DOI":"10.1016\/B978-0-444-88074-1.50009-3"},{"key":"12_CR38","doi-asserted-by":"publisher","first-page":"123","DOI":"10.1016\/S0019-9958(79)90653-3","volume":"43","author":"K. Wagner","year":"1979","unstructured":"K. Wagner. On \u03c9-regular sets. Information and Control, 43:123\u2013177, 1979.","journal-title":"Information and Control"}],"container-title":["Lecture Notes in Computer Science","FST TCS 2000: Foundations of Software Technology and Theoretical Computer Science"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-44450-5_12","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,2]],"date-time":"2019-05-02T00:16:52Z","timestamp":1556756212000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-44450-5_12"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2000]]},"ISBN":["9783540414131","9783540444503"],"references-count":38,"URL":"https:\/\/doi.org\/10.1007\/3-540-44450-5_12","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2000]]}}}