{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,5]],"date-time":"2026-02-05T09:19:32Z","timestamp":1770283172750,"version":"3.49.0"},"publisher-location":"Berlin, Heidelberg","reference-count":31,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540405610","type":"print"},{"value":"9783540450894","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2003]]},"DOI":"10.1007\/3-540-45089-0_5","type":"book-chapter","created":{"date-parts":[[2007,10,27]],"date-time":"2007-10-27T07:27:35Z","timestamp":1193470055000},"page":"35-48","source":"Crossref","is-referenced-by-count":49,"title":["Constructing B\u00fcchi Automata from Linear Temporal Logic Using Simulation Relations for Alternating B\u00fcchi Automata"],"prefix":"10.1007","author":[{"given":"Carsten","family":"Fritz","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2003,6,24]]},"reference":[{"key":"5_CR1","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"163","DOI":"10.1007\/BFb0055622","volume-title":"9th Int. Conf. on Concurrency Theory (CONCUR\u2019 98)","author":"R. Alur","year":"1998","unstructured":"R. Alur, Th.A. Henzinger, O. Kupferman, and M.Y. Vardi. Alternating refinement relations. In D. Sangiorgi and R. de Simone, eds., 9th Int. Conf. on Concurrency Theory (CONCUR\u2019 98), vol. 1466 of LNCS, pp. 163\u2013178, 1998."},{"key":"5_CR2","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"70","DOI":"10.1007\/3-540-36576-1_5","volume-title":"6th Int. Conf. on Foundations of Software Science and Computational Structures (FOSSACS\u2019 03)","author":"A. Arnold","year":"2003","unstructured":"A. Arnold and L. Santocanale. Ambigious classes in the games \u03bc-calculus hierarchy. In A. D. Gordon, ed., 6th Int. Conf. on Foundations of Software Science and Computational Structures (FOSSACS\u2019 03), vol. 2620 of LNCS, pp. 70\u201386, 2003."},{"key":"5_CR3","unstructured":"AT & T Labs-Research. Graphviz. http:\/\/www.research.att.com\/sw\/tools\/graphviz\/ ."},{"key":"5_CR4","unstructured":"R. Bloem. Wring: an LTL to Buechi translator. URL: http:\/\/vlsi.colorado.edu\/~rbloem\/wring.html ."},{"key":"5_CR5","series-title":"Lect Notes Comput Sci","first-page":"255","volume-title":"Computer Aided Verification, 3rd Int. Workshop, CAV\u2019 91","author":"D. L. Dill","year":"1991","unstructured":"D. L. Dill, A. J. Hu, and H. Wong-Toi. Checking for language inclusion using simulation preorders. In Kim Guldstrand Larsen and Arne Skou, eds., Computer Aided Verification, 3rd Int. Workshop, CAV\u2019 91, vol. 575 of LNCS, pp. 255\u2013265, 1991."},{"key":"5_CR6","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"153","DOI":"10.1007\/3-540-44618-4_13","volume-title":"11th Int. Conf. on Concurrency Theory (CONCUR 2000)","author":"K. Etessami","year":"2000","unstructured":"K. Etessami and G. Holzmann. Optimizing B\u00fcchi automata. In C. Palamidessi, ed., 11th Int. Conf. on Concurrency Theory (CONCUR 2000), vol. 1877 of LNCS, pp. 153\u2013167, 2000."},{"key":"5_CR7","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"694","DOI":"10.1007\/3-540-48224-5_57","volume-title":"ICALP","author":"K. Etessami","year":"2001","unstructured":"K. Etessami, R. Schuller, and Th. Wilke. Fair simulation relations, parity games, and state space reduction for B\u00fcchi automata. In F. Orejas, P.G. Spirakis, and J. van Leeuwen, eds., ICALP, volume 2076 of LNCS, pp. 694\u2013707. Springer-Verlag, 2001."},{"key":"5_CR8","unstructured":"K. Etessami. Temporal massage parlor. http:\/\/www1.bell-labs.com\/project\/TMP\/ ."},{"key":"5_CR9","unstructured":"C. Fritz. Home page. http:\/\/www.ti.informatik.uni-kiel.de\/~fritz\/ ."},{"key":"5_CR10","unstructured":"C. Fritz and B. Teegen. LTL \u2192 BA. http:\/\/www.ti.informatik.uni-kiel.de\/~teegen\/ABA-Simulation\/ltl.cgi ."},{"key":"5_CR11","unstructured":"C. Fritz and Th. Wilke. Simulation relations for alternating B\u00fcchi automata. Tech. Rep. 2019, Institut f\u00fcr Informatik, Kiel University, July 2002. Extended version. Available at http:\/\/www.ti.informatik.uni-kiel.de\/~fritz\/TechRep2019ext.ps ."},{"key":"5_CR12","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"157","DOI":"10.1007\/3-540-36206-1_15","volume-title":"22nd Conf. on Foundations of Software Technology and Theoretical Computer Science","author":"C. Fritz","year":"2002","unstructured":"C. Fritz and Th. Wilke. State space reductions for alternating B\u00fcchi automata: Quotienting by simulation equivalences. In M. Agrawal and A. Seth, eds., 22nd Conf. on Foundations of Software Technology and Theoretical Computer Science, vol. 2556 of LNCS, pp. 157\u2013168, 2002."},{"key":"5_CR13","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"610","DOI":"10.1007\/3-540-45657-0_51","volume-title":"Computer Aided Verification. 14th International Conference, CAV 2002","author":"S. Gurumurthy","year":"2002","unstructured":"S. Gurumurthy, R. Bloem, and F. Somenzi. Fair simulation minimization. In E. Brinksma and K. Guldstrand Larsen, eds., Computer Aided Verification. 14th International Conference, CAV 2002, vol. 2404 of LNCS, pp. 610\u2013623, 2002."},{"key":"5_CR14","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":"5_CR15","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"53","DOI":"10.1007\/3-540-44585-4_6","volume-title":"Computer Aided Verification. 13th International Conference, CAV 2001","author":"P. Gastin","year":"2001","unstructured":"P. Gastin and D. Oddoux. Fast LTL to B\u00fcchi automata translation. In G. Berry, H. Comon, and A. Finkel, eds., Computer Aided Verification. 13th International Conference, CAV 2001, vol. 2102 of LNCS, pp. 53\u201365. Springer-Verlag, 2001."},{"key":"5_CR16","doi-asserted-by":"crossref","unstructured":"R. Gerth, D. Peled, M.Y. Vardi, and P. Wolper. Simple on-the-fly automatic verification of linear temporal logic. In Proc. of the 15th Workshop on Protocol Specification, Testing, and Verification, pp. 3\u201318, Warsaw, Poland, June 1995. Chapman Hall.","DOI":"10.1007\/978-0-387-34892-6_1"},{"key":"5_CR17","doi-asserted-by":"crossref","unstructured":"M. Henzinger Rauch, Th.A. Henzinger, and P.W. Kopke. Computing simulations on finite and infinite graphs. In 36th Ann. Symp. on Foundations of Computer Science (FOCS\u2019 95), pp. 453\u2013462, 1995.","DOI":"10.1109\/SFCS.1995.492576"},{"key":"5_CR18","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"273","DOI":"10.1007\/3-540-63141-0_19","volume-title":"CONCUR\u2019 97","author":"Th.A. Henzinger","year":"1997","unstructured":"Th.A. Henzinger, O. Kupferman, and S.K. Rajamani. Fair simulation. In CONCUR\u2019 97, vol. 1243 of LNCS, pp. 273\u2013287, 1997."},{"key":"5_CR19","unstructured":"G. J. Holzmann. The SPIN homepage. http:\/\/netlib.bell-labs.com\/netlib\/spin\/whatispin.html ."},{"key":"5_CR20","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"299","DOI":"10.1007\/3-540-46419-0_21","volume-title":"TACAS\u2019 00: Tools and Algorithms for the Construction and Analysis of Systems","author":"Th.A. Henzinger","year":"2000","unstructured":"Th.A. Henzinger and S.K. Rajamani. Fair bisimulation. In S. Graf and M. Schwartzbach, eds., TACAS\u2019 00: Tools and Algorithms for the Construction and Analysis of Systems, vol. 1785 of LNCS, pp. 299\u2013314. Springer-Verlag, 2000."},{"key":"5_CR21","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"290","DOI":"10.1007\/3-540-46541-3_24","volume-title":"STACS 2000, 17th Ann. Symp. on Theoretical Aspects of Computer Science","author":"M. Jurdzimski","year":"2000","unstructured":"M. Jurdzi\u2019mski. Small progress measures for solving parity games. In H. Reichel and S. Tison, eds., STACS 2000, 17th Ann. Symp. on Theoretical Aspects of Computer Science, vol. 1770 of LNCS, pp. 290\u2013301, 2000. Springer-Verlag."},{"key":"5_CR22","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":"5_CR23","unstructured":"R. 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. ISBN 0-934613-34-6."},{"key":"5_CR24","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, vol. 92 of LNCS. Springer-Verlag, 1980."},{"key":"5_CR25","doi-asserted-by":"crossref","unstructured":"Z. Manna and A. Pnueli. The Temporal Logic of Reactive and Concurrent Systems. Springer-Verlag, 1992.","DOI":"10.1007\/978-1-4612-0931-7"},{"key":"5_CR26","series-title":"Lect Notes Comput Sci","volume-title":"Proc. 13th Int. Coll. on Automata, Languages, and Programming (ICALP\u2019 86)","author":"D.E. Muller","year":"1986","unstructured":"D.E. Muller, A. Saoudi, and P.E. Schupp. Alternating automata, the weak monadic theory of the tree and its complexity. In Proc. 13th Int. Coll. on Automata, Languages, and Programming (ICALP\u2019 86), vol. 226 of LNCS, 1986."},{"key":"5_CR27","unstructured":"D. Oddoux. LTL2BA. http:\/\/verif.liafa.jussieu.fr\/cgi-bin\/binbin\/ltl2ba.shtml ."},{"key":"5_CR28","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"167","DOI":"10.1007\/BFb0017309","volume-title":"5th GI Conference","author":"D. M. R. Park","year":"1981","unstructured":"D. M. R. Park. Concurrency and automata on infinite sequences. In P. Deussen, ed., 5th GI Conference, vol. 104 of LNCS, pp. 167\u2013183, 1981."},{"key":"5_CR29","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"248","DOI":"10.1007\/10722167_21","volume-title":"Computer Aided Verification, 12th International Conference (CAV 2000)","author":"F. Somenzi","year":"2000","unstructured":"F. Somenzi and R. Bloem. Efficient B\u00fcchi automata from LTL formulae. In E. Allen Emerson and A. Prasad Sistla, eds., Computer Aided Verification, 12th International Conference (CAV 2000), vol. 1855 of LNCS, pp. 248\u2013263, 2000."},{"issue":"1","key":"5_CR30","doi-asserted-by":"publisher","first-page":"57","DOI":"10.1007\/s100090200070","volume":"4","author":"H. Tauriainen","year":"2002","unstructured":"H. Tauriainen and K. Heljanko. Testing LTL formula translation into B\u00fcchi automata. Int. Journal on Software Tools for Technology Transfer, 4(1):57\u201370, 2002.","journal-title":"Int. Journal on Software Tools for Technology Transfer"},{"key":"5_CR31","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"238","DOI":"10.1007\/3-540-60915-6_6","volume-title":"Logics for Concurrency: Structure versus Automata","author":"M.Y. Vardi","year":"1996","unstructured":"M.Y. Vardi. An automata-theoretic approach to linear temporal logic. In Logics for Concurrency: Structure versus Automata, vol. 1043 of LNCS, pp. 238\u2013266, 1996."}],"container-title":["Lecture Notes in Computer Science","Implementation and Application of Automata"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-45089-0_5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,21]],"date-time":"2025-01-21T23:24:16Z","timestamp":1737501856000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45089-0_5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003]]},"ISBN":["9783540405610","9783540450894"],"references-count":31,"URL":"https:\/\/doi.org\/10.1007\/3-540-45089-0_5","relation":{},"ISSN":["0302-9743"],"issn-type":[{"value":"0302-9743","type":"print"}],"subject":[],"published":{"date-parts":[[2003]]}}}