{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,5]],"date-time":"2026-02-05T10:15:23Z","timestamp":1770286523018,"version":"3.49.0"},"publisher-location":"Berlin, Heidelberg","reference-count":29,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540002253","type":"print"},{"value":"9783540362067","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2002]]},"DOI":"10.1007\/3-540-36206-1_15","type":"book-chapter","created":{"date-parts":[[2007,8,16]],"date-time":"2007-08-16T07:23:08Z","timestamp":1187248988000},"page":"157-168","source":"Crossref","is-referenced-by-count":14,"title":["State Space Reductions for Alternating B\u00fcchi Automata Quotienting by Simulation Equivalences"],"prefix":"10.1007","author":[{"given":"Carsten","family":"Fritz","sequence":"first","affiliation":[]},{"given":"Thomas","family":"Wilke","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2002,12,16]]},"reference":[{"key":"15_CR1","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"163","DOI":"10.1007\/BFb0055622","volume-title":"CONCUR 1998","author":"R. Alur","year":"1998","unstructured":"Rajeev Alur, ThomasA. Henzinger, Orna Kupferman, and MosheY. Vardi. Alternating refinement relations. In D. Sangiorgi and R. de Simone, editors, CONCUR 1998, vol. 1466 of LNCS, pp. 163\u2013178, 1998."},{"key":"15_CR2","unstructured":"Doran Bustan and Orna Grumberg. Checking for fair simulation in models with B\u00fcchi fairness constraints, Dec. 2000. Tech. Rep. TR-CS-2000-13, Technion."},{"key":"15_CR3","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"249","DOI":"10.1007\/3-540-48683-6_23","volume-title":"CAV 1999","author":"M. Daniele","year":"1999","unstructured":"Marco Daniele, Fausto Giunchiglia, and MosheY. Vardi. Improved automata generation for linear time temporal logic. In N. Halbwachs and D. Peled, editors, CAV 1999, vol. 1633 of LNCS, pp. 249\u2013260, 1999."},{"key":"15_CR4","series-title":"Lect Notes Comput Sci","first-page":"255","volume-title":"CAV 1991","author":"D. L. Dill","year":"1991","unstructured":"David L. Dill, Alan J. Hu, and Howard Wong-Toi. Checking for language inclusion using simulation preorders. In Kim G. Larsen and Arne Skou, editors, CAV 1991, vol. 575 of LNCS, pp. 255\u2013265, 1991."},{"key":"15_CR5","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"153","DOI":"10.1007\/3-540-44618-4_13","volume-title":"CONCUR 2000","author":"K. Etessami","year":"2000","unstructured":"Kousha Etessami and Gerard Holzmann. Optimizing B\u00fcchi automata. In Catuscia Palamidessi, editor, CONCUR 2000, vol. 1877 of LNCS, pp. 153\u2013167, 2000."},{"key":"15_CR6","doi-asserted-by":"crossref","unstructured":"E. Allen Emerson and Charanjit S. Jutla. The complexity of tree automata and logics of programs (extended abstract). In FoCS 1988, pp. 328\u2013337. 1988. IEEE.","DOI":"10.1109\/SFCS.1988.21949"},{"key":"15_CR7","doi-asserted-by":"crossref","unstructured":"E. Allen Emerson and Charanjit S. Jutla. Tree automata, mu-calculus and determinacy. In FoCS 1991, pp. 368\u2013377, San Juan, Puerto Rico, Oct. 1991. IEEE.","DOI":"10.1109\/SFCS.1991.185392"},{"key":"15_CR8","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"694","DOI":"10.1007\/3-540-48224-5_57","volume-title":"ICALP 2001","author":"K. Etessami","year":"2001","unstructured":"Kousha Etessami, Rebecca Schuller, and Thomas Wilke. Fair simulation relations, parity games, and state space reduction forB\u00fcchi automata. In F. Orejas, P.G. Spirakis, and J. van Leeuwen, editors, ICALP 2001, vol. 2076 of LNCS, pp. 694\u2013707, 2001."},{"key":"15_CR9","doi-asserted-by":"crossref","unstructured":"Kousha Etessami. A Hierarchy of Polynomial-Time Computable Simulations for Automata. CONCUR 2002, to appear.","DOI":"10.1007\/3-540-45694-5_10"},{"key":"15_CR10","unstructured":"Carsten Fritz and Thomas Wilke. Simulation relations for alternating B\u00fcchi automata. Extended version of tech. rep. 2019, Institut f\u00fcr Informatik, CAU Kiel, July 2002. URL: http:\/\/www.informatik.uni-kiel.de\/\u223dfritz\/ TechRep2019 ext.ps."},{"key":"15_CR11","doi-asserted-by":"crossref","unstructured":"Yuri Gurevich and Leo Harrington. Trees, automata, and games. In 14th ACM Symp. on the Theory of Computing, pp. 60\u201365, 1982.","DOI":"10.1145\/800070.802177"},{"key":"15_CR12","volume-title":"Computers and Intractability: A Guide to the Theory of NP-Completeness","author":"M. R. Garey","year":"1979","unstructured":"M. R. Garey and D. S. Johnson. Computers and Intractability: A Guide to the Theory of NP-Completeness. W.H. Freeman and Co., San Francisco, 1979."},{"key":"15_CR13","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"53","DOI":"10.1007\/3-540-44585-4_6","volume-title":"CAV 2001","author":"P. Gastin","year":"2001","unstructured":"Paul Gastin and Denis Oddoux. Fast LTL to B\u00fcchi automata translation. In G. Berry, H. Comon, and A. Finkel, editors, CAV 2001, vol. 2102 of LNCS, pp. 53\u201365, 2001."},{"key":"15_CR14","doi-asserted-by":"crossref","unstructured":"Rob Gerth, Doron Peled, Moshe Y. Vardi, and Pierre Wolper. Simple on-the-.y automatic verification of linear temporal logic. In PSTV 1995, pp. 3\u201318, Warsaw, Poland, June 1995. Chapman Hall.","DOI":"10.1007\/978-0-387-34892-6_1"},{"key":"15_CR15","doi-asserted-by":"crossref","unstructured":"Sankar Gurumurthy, Roderick Bloem, and Fabio Somenzi. Fair simulation minimization. CAV 2002, to appear.","DOI":"10.1007\/3-540-45657-0_51"},{"key":"15_CR16","doi-asserted-by":"crossref","unstructured":"Monika Henzinger Rauch, Thomas A. Henzinger, and Peter W. Kopke. Computing simulations on finite and infinite graphs. In FoCS 1995, pp. 453\u2013462, 1995.","DOI":"10.1109\/SFCS.1995.492576"},{"key":"15_CR17","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"273","DOI":"10.1007\/3-540-63141-0_19","volume-title":"CONCUR 1997","author":"T. A. Henzinger","year":"1997","unstructured":"Thomas A. Henzinger, Orna Kupferman, and Sriram K. Rajamani. Fair simulation. In CONCUR 1997, vol. 1243 of LNCS, pp. 273\u2013287, 1997."},{"key":"15_CR18","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"299","DOI":"10.1007\/3-540-46419-0_21","volume-title":"TACAS 2000","author":"T. A. Henzinger","year":"2000","unstructured":"Thomas A. Henzinger and Sriram K. Rajamani. Fair bisimulation.In S. Graf and M. Schwartzbach, editors, TACAS 2000, vol. 1785 of LNCS, pp. 299\u2013314, 2000."},{"key":"15_CR19","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"290","DOI":"10.1007\/3-540-46541-3_24","volume-title":"STACS 2000","author":"M. Jurdzi\u0144ski","year":"2000","unstructured":"Marcin Jurdzi\u0144ski. Small progress measures for solving parity games. In H. Reichel and S. Tison, editors, STACS 2000, vol. 1770 of LNCS, pp. 290\u2013301, 2000."},{"issue":"2","key":"15_CR20","doi-asserted-by":"publisher","first-page":"312","DOI":"10.1145\/333979.333987","volume":"47","author":"O. Kupferman","year":"2000","unstructured":"OrnaKupferman, MosheY. Vardi, and Pierre Wolper. An automata-theoretic approach to branching-time model checking. Journal of the ACM, 47(2):312\u2013360, 2000.","journal-title":"Journal of the ACM"},{"key":"15_CR21","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"255","DOI":"10.1007\/3-540-44585-4_24","volume-title":"CAV 2001","author":"M. Leucker","year":"2001","unstructured":"Martin Leucker and Thomas Noll. Truth\/SLC-A parallel verification platform for concurrent systems. In G. Berry, H. Comon, and A. Finkel, editors, CAV 2001, vol. 2102 of LNCS, pp. 255\u2013259, 2001."},{"key":"15_CR22","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4615-3190-6","volume-title":"Symbolic Model Checking","author":"K. L. McMillan","year":"1993","unstructured":"Kenneth L. McMillan. Symbolic Model Checking. Kluwer, Boston, 1993."},{"key":"15_CR23","doi-asserted-by":"publisher","first-page":"321","DOI":"10.1016\/0304-3975(84)90049-5","volume":"32","author":"S. Miyano","year":"1984","unstructured":"S. Miyano and T. Hayashi. Alternating finite automata on \u03c9-words. Theoretical Computer Science, 32:321\u2013330, 1984.","journal-title":"Theoretical Computer Science"},{"key":"15_CR24","unstructured":"Robin Milner. An algebraic definition of simulation between programs. In D. C. Cooper, editor, Proc. of the 2nd Int. Joint Conf. on Artificial Intelligence, pp. 481\u2013489, London, UK, September 1971.William Kaufmann."},{"key":"15_CR25","doi-asserted-by":"crossref","unstructured":"David E. Muller, Ahmed Saoudi, and Paul E. Schupp. Weak alternating automata give a simple explanation of why most temporal and dynamic logics are decidable in exponential time. In LICS 1988, pp. 422\u2013427, IEEE Computer Society, 1988.","DOI":"10.1109\/LICS.1988.5139"},{"key":"15_CR26","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"248","DOI":"10.1007\/10722167_21","volume-title":"CAV 2000","author":"F. Somenzi","year":"2000","unstructured":"Fabio Somenzi and Roderick Bloem. Efficient B\u00fcchi automata from LTL formulae. In E. Allen Emerson and A. Prasad Sistla, editors, CAV 2000, vol. 1855 of LNCS, pp. 248\u2013263, 2000."},{"key":"15_CR27","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"575","DOI":"10.1007\/3-540-57887-0_116","volume-title":"Theoretical Aspects of Computer Software","author":"M. Y. Vardi","year":"1994","unstructured":"Moshe Y. Vardi. Nontraditional applications of automata theory. In Theoretical Aspects of Computer Software, vol. 789 of LNCS, pp. 575\u2013597, 1994."},{"key":"15_CR28","first-page":"332","volume-title":"LICS 1986","author":"M. Y. Vardi","year":"1986","unstructured":"Moshe Y. Vardi and Pierre Wolper. An automata-theoretic approach to automatic program verification. In Dexter Kozen, editor, LICS 1986, pp. 332\u2013344, Cambridge, Mass., 16-18 June 1986."},{"issue":"1","key":"15_CR29","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1006\/inco.1994.1092","volume":"115","author":"MosheY. Vardi","year":"1994","unstructured":"MosheY. Vardi and Pierre Wolper. Reasoning about infinite computations. Information and Computation, 115(1):1\u201337, 1994.","journal-title":"Information and Computation"}],"container-title":["Lecture Notes in Computer Science","FST TCS 2002: Foundations of Software Technology and Theoretical Computer Science"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-36206-1_15","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,20]],"date-time":"2025-01-20T11:23:22Z","timestamp":1737372202000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-36206-1_15"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002]]},"ISBN":["9783540002253","9783540362067"],"references-count":29,"URL":"https:\/\/doi.org\/10.1007\/3-540-36206-1_15","relation":{},"ISSN":["0302-9743"],"issn-type":[{"value":"0302-9743","type":"print"}],"subject":[],"published":{"date-parts":[[2002]]}}}