{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T02:49:16Z","timestamp":1725504556823},"publisher-location":"Berlin, Heidelberg","reference-count":31,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540781622"},{"type":"electronic","value":"9783540781639"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-78163-9_24","type":"book-chapter","created":{"date-parts":[[2008,2,29]],"date-time":"2008-02-29T10:30:06Z","timestamp":1204281006000},"page":"279-293","source":"Crossref","is-referenced-by-count":17,"title":["From LTL to Symbolically Represented Deterministic Automata"],"prefix":"10.1007","author":[{"given":"Andreas","family":"Morgenstern","sequence":"first","affiliation":[]},{"given":"Klaus","family":"Schneider","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"24_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"83","DOI":"10.1007\/3-540-45089-0_9","volume-title":"Implementation and Application of Automata","author":"C. Allauzen","year":"2003","unstructured":"Allauzen, C., Mohri, M.: An efficient pre-determinization algorithm. In: H. Ibarra, O., Dang, Z. (eds.) CIAA 2003. LNCS, vol.\u00a02759, pp. 83\u201395. Springer, Heidelberg (2003)"},{"key":"24_CR2","doi-asserted-by":"publisher","first-page":"877","DOI":"10.1109\/ICCAD.2005.1560185","volume-title":"Conference on Computer Aided Design (ICCAD)","author":"R. Armoni","year":"2005","unstructured":"Armoni, R., et al.: Efficient LTL compilation for SAT-based model checking. In: Conference on Computer Aided Design (ICCAD), pp. 877\u2013884. IEEE Computer Society, Los Alamitos (2005)"},{"key":"24_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"208","DOI":"10.1007\/11812128_20","volume-title":"Implementation and Application of Automata","author":"R. Bloem","year":"2006","unstructured":"Bloem, R., et al.: Symbolic implementation of alternating automata. In: H. Ibarra, O., Yen, H.-C. (eds.) CIAA 2006. LNCS, vol.\u00a04094, pp. 208\u2013218. Springer, Heidelberg (2006)"},{"key":"24_CR4","first-page":"1","volume-title":"Logic in Computer Science (LICS)","author":"J. Burch","year":"1990","unstructured":"Burch, J., et al.: Symbolic model checking: 1020 states and beyond. In: Logic in Computer Science (LICS), Washington, DC, USA, 1990, pp. 1\u201333. IEEE Computer Society, Los Alamitos (1990)"},{"issue":"1-3","key":"24_CR5","doi-asserted-by":"publisher","first-page":"37","DOI":"10.1016\/S0304-3975(02)00618-7","volume":"297","author":"O. Carton","year":"2003","unstructured":"Carton, O., Michel, M.: Unambiguous B\u00fcchi automata. Theoretical Computer Science\u00a0297(1-3), 37\u201381 (2003)","journal-title":"Theoretical Computer Science"},{"issue":"1","key":"24_CR6","doi-asserted-by":"publisher","first-page":"47","DOI":"10.1023\/A:1008615614281","volume":"10","author":"E. Clarke","year":"1997","unstructured":"Clarke, E., Grumberg, O., Hamaguchi, K.: Another look at LTL model checking. Formal Methods in System Design (FMSD)\u00a010(1), 47\u201371 (1997)","journal-title":"Formal Methods in System Design (FMSD)"},{"key":"24_CR7","first-page":"995","volume-title":"Handbook of Theoretical Computer Science. Formal Models and Semantics, ch.16","author":"E. Emerson","year":"1990","unstructured":"Emerson, E.: Temporal and modal logic. In: van Leeuwen, J. (ed.) Handbook of Theoretical Computer Science. Formal Models and Semantics, ch.16, vol.\u00a0B, pp. 995\u20131072. Elsevier, Amsterdam (1990)"},{"key":"24_CR8","doi-asserted-by":"crossref","unstructured":"Emerson, E., Sistla, A.: Deciding branching time logic. In: Symposium on Theory of Computing (STOC), pp. 14\u201324 (1984)","DOI":"10.1145\/800057.808661"},{"key":"24_CR9","series-title":"Lecture Notes in Computer Science","volume-title":"Computer Aided Verification","author":"P. Gastin","year":"2001","unstructured":"Gastin, P., Oddoux, D.: Fast LTL to B\u00fcchi Automata Translation. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol.\u00a02102, Springer, Heidelberg (2001)"},{"key":"24_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"96","DOI":"10.1007\/978-3-540-39724-3_10","volume-title":"Correct Hardware Design and Verification Methods","author":"S. Gurumurthy","year":"2003","unstructured":"Gurumurthy, S., et al.: On Complementing Nondeterministic B\u00fcchi Automata. In: Geist, D., Tronci, E. (eds.) CHARME 2003. LNCS, vol.\u00a02860, pp. 96\u2013110. Springer, Heidelberg (2003)"},{"key":"24_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"394","DOI":"10.1007\/11874683_26","volume-title":"Computer Science Logic","author":"T. Henzinger","year":"2006","unstructured":"Henzinger, T., Piterman, N.: Solving games without determinization. In: \u00c9sik, Z. (ed.) CSL 2006. LNCS, vol.\u00a04207, pp. 394\u2013409. Springer, Heidelberg (2006)"},{"key":"24_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0055036","volume-title":"Automata, Languages and Programming","author":"Y. Kesten","year":"1998","unstructured":"Kesten, Y., Pnueli, A., Raviv, L.: Algorithmic Verification of Linear Temporal Logic Specifications. In: Larsen, K.G., Skyum, S., Winskel, G. (eds.) ICALP 1998. LNCS, vol.\u00a01443, Springer, Heidelberg (1998)"},{"issue":"2","key":"24_CR13","doi-asserted-by":"publisher","first-page":"182","DOI":"10.1016\/j.tcs.2006.07.022","volume":"363","author":"J. Klein","year":"2006","unstructured":"Klein, J., Baier, C.: Experiments with deterministic \u03c9-automata for formulas of temporal logic. Theoretical Computer Science\u00a0363(2), 182\u2013195 (2006)","journal-title":"Theoretical Computer Science"},{"key":"24_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"31","DOI":"10.1007\/11817963_6","volume-title":"Computer Aided Verification","author":"O. Kupferman","year":"2006","unstructured":"Kupferman, O., Piterman, N., Vardi, M.: Safraless Compositional Synthesis. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol.\u00a04144, pp. 31\u201344. Springer, Heidelberg (2006)"},{"key":"24_CR15","first-page":"531","volume-title":"Symposium on Foundations of Computer Science","author":"O. Kupferman","year":"2005","unstructured":"Kupferman, O., Vardi, M.: Safraless decision procedures. In: Symposium on Foundations of Computer Science, pp. 531\u2013540. IEEE Computer Society, Los Alamitos (2005)"},{"key":"24_CR16","volume-title":"Counter-free Automata","author":"R. McNaughton","year":"1971","unstructured":"McNaughton, R., Papert, S.: Counter-free Automata. MIT Press, Cambridge (1971)"},{"key":"24_CR17","unstructured":"Merz, S., Sezgin, A.: Emptiness of linear weak alternating automata. Technical report, LORIA (2003)"},{"key":"24_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"275","DOI":"10.1007\/3-540-16761-7_77","volume-title":"Automata, Languages and Programming","author":"D. Muller","year":"1986","unstructured":"Muller, D., Saoudi, A., Schupp, P.: Alternating automata, the weak monadic theory of the tree, and its complexity. In: Kott, L. (ed.) ICALP 1986. LNCS, vol.\u00a0226, pp. 275\u2013283. Springer, Heidelberg (1986)"},{"key":"24_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"238","DOI":"10.1007\/11605157_20","volume-title":"Implementation and Application of Automata","author":"R. Pel\u00e1nek","year":"2006","unstructured":"Pel\u00e1nek, R., Strejcek, J.: Deeper connections between LTL and alternating automata. In: Farr\u00e9, J., Litovsky, I., Schmitz, S. (eds.) CIAA 2005. LNCS, vol.\u00a03845, pp. 238\u2013249. Springer, Heidelberg (2006)"},{"key":"24_CR20","volume-title":"Symp. on Logic in Computer Science","author":"N. Piterman","year":"2006","unstructured":"Piterman, N.: From nondeterministic B\u00fcchi and Streett automata to deterministic parity automata. In: Symp. on Logic in Computer Science, IEEE Comp. Soc, Los Alamitos (2006)"},{"key":"24_CR21","first-page":"46","volume-title":"Foundations of Computer Science (FOCS)","author":"A. Pnueli","year":"1977","unstructured":"Pnueli, A.: The temporal logic of programs. In: Foundations of Computer Science (FOCS), Providence, RI, USA, 1977, pp. 46\u201357. IEEE Computer Society, Los Alamitos (1977)"},{"key":"24_CR22","first-page":"179","volume-title":"Symposium on Principles of Programming Languages","author":"A. Pnueli","year":"1989","unstructured":"Pnueli, A., Rosner, R.: On the synthesis of a reactive module. In: Symposium on Principles of Programming Languages, Austin, Texas, pp. 179\u2013190. ACM, New York (1989)"},{"key":"24_CR23","doi-asserted-by":"crossref","unstructured":"Safra, S.: On the complexity of \u03c9-automata. In: Symposium on Foundations of Computer Science (FOCS), pp. 319\u2013327 (1988)","DOI":"10.1109\/SFCS.1988.21948"},{"key":"24_CR24","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"39","DOI":"10.1007\/3-540-45653-8_3","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"K. Schneider","year":"2001","unstructured":"Schneider, K.: Improving automata generation for linear temporal logic by considering the automata hierarchy. In: Nieuwenhuis, R., Voronkov, A. (eds.) LPAR 2001. LNCS (LNAI), vol.\u00a02250, pp. 39\u201354. Springer, Heidelberg (2001)"},{"key":"24_CR25","series-title":"EATCS Series","volume-title":"Texts in Theoretical Computer Science","author":"K. Schneider","year":"2003","unstructured":"Schneider, K.: Verification of Reactive Systems \u2013 Formal Methods and Algorithms. In: Texts in Theoretical Computer Science. EATCS Series, Springer, Heidelberg (2003)"},{"key":"24_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"262","DOI":"10.1007\/11605157_22","volume-title":"Implementation and Application of Automata","author":"C. Schulte Althoff","year":"2006","unstructured":"Schulte Althoff, C., Thomas, W., Wallmeier, N.: Observations on determinization of B\u00fcchi automata. In: Farr\u00e9, J., Litovsky, I., Schmitz, S. (eds.) CIAA 2005. LNCS, vol.\u00a03845, pp. 262\u2013272. Springer, Heidelberg (2006)"},{"key":"24_CR27","first-page":"133","volume-title":"Handbook of Theoretical Computer Science. Formal Models and Semantics, ch. 4","author":"W. Thomas","year":"1990","unstructured":"Thomas, W.: Automata on infinite objects. In: van Leeuwen, J. (ed.) Handbook of Theoretical Computer Science. Formal Models and Semantics, ch. 4, vol.\u00a0B, pp. 133\u2013191. Elsevier, Amsterdam (1990)"},{"key":"24_CR28","unstructured":"Tuerk, T., Schneider, K.: Relationship between alternating omega-automata and symbolically represented nondeterministic omega-automata. Technical Report 340, Dep. of Computer Science, University of Kaiserslautern, Germany (2005)"},{"key":"24_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"238","DOI":"10.1007\/3-540-60915-6_6","volume-title":"Logics for Concurrency","author":"M. Vardi","year":"1996","unstructured":"Vardi, M.: An automata-theoretic approach to linear temporal logic. In: Moller, F., Birtwistle, G. (eds.) Logics for Concurrency. LNCS, vol.\u00a01043, pp. 238\u2013266. Springer, Heidelberg (1996)"},{"key":"24_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"265","DOI":"10.1007\/3-540-48778-6_16","volume-title":"Formal Methods for Real-Time and Probabilistic Systems","author":"M. Vardi","year":"1999","unstructured":"Vardi, M.: Probabilistic linear-time model checking: An overview of the automata-theoretic approach. In: Katoen, J.-P. (ed.) AMAST-ARTS 1999, ARTS 1999, and AMAST-WS 1999. LNCS, vol.\u00a01601, pp. 265\u2013276. Springer, Heidelberg (1999)"},{"key":"24_CR31","first-page":"332","volume-title":"Symposium on Logic in Computer Science (LICS)","author":"M. Vardi","year":"1986","unstructured":"Vardi, M., Wolper, P.: An automata-theoretic approach to automatic program verification. In: Symposium on Logic in Computer Science (LICS), pp. 332\u2013344. IEEE Computer Society, Los Alamitos (1986)"}],"container-title":["Lecture Notes in Computer Science","Verification, Model Checking, and Abstract Interpretation"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-78163-9_24.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T11:00:36Z","timestamp":1619521236000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-78163-9_24"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540781622","9783540781639"],"references-count":31,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-78163-9_24","relation":{},"subject":[]}}