{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T14:04:27Z","timestamp":1725545067337},"publisher-location":"Berlin, Heidelberg","reference-count":32,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540310235"},{"type":"electronic","value":"9783540330974"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2006]]},"DOI":"10.1007\/11605157_17","type":"book-chapter","created":{"date-parts":[[2006,3,1]],"date-time":"2006-03-01T15:07:40Z","timestamp":1141225660000},"page":"199-212","source":"Crossref","is-referenced-by-count":4,"title":["Experiments with Deterministic \u03c9-Automata for Formulas of Linear Temporal Logic"],"prefix":"10.1007","author":[{"given":"Joachim","family":"Klein","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Christel","family":"Baier","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"17_CR1","doi-asserted-by":"publisher","first-page":"389","DOI":"10.1007\/978-3-642-59126-6_7","volume":"3","author":"W. Thomas","year":"1997","unstructured":"Thomas, W.: Languages, automata, and logic. Handbook of formal languages\u00a03, 389\u2013455 (1997)","journal-title":"Handbook of formal languages"},{"key":"17_CR2","series-title":"Lecture Notes in Computer Science","volume-title":"Automata Logics, and Infinite Games: A Guide to Current Research","year":"2002","unstructured":"Gr\u00e4del, E., Thomas, W., Wilke, T. (eds.): Automata, Logics, and Infinite Games. LNCS, vol.\u00a02500. Springer, Heidelberg (2002)"},{"key":"17_CR3","unstructured":"de Alfaro, L.: Formal Verification of Probabilistic Systems. PhD thesis, Stanford University, Department of Computer Science (1997)"},{"key":"17_CR4","doi-asserted-by":"publisher","first-page":"125","DOI":"10.1007\/s004460050046","volume":"11","author":"C. Baier","year":"1998","unstructured":"Baier, C., Kwiatkowska, M.: Model checking for a probabilistic branching time logic with fairness. Distributed Computing\u00a011, 125\u2013155 (1998)","journal-title":"Distributed Computing"},{"key":"17_CR5","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":"17_CR6","first-page":"319","volume-title":"Proc. 29th Annual Symposium on Foundations of Computer Science (FOCS)","author":"S. Safra","year":"1988","unstructured":"Safra, S.: On the complexity of \u03c9-automata. In: Proc. 29th Annual Symposium on Foundations of Computer Science (FOCS), pp. 319\u2013327. IEEE Computer Society Press, Los Alamitos (1988)"},{"key":"17_CR7","unstructured":"Safra, S.: Complexity of Automata on Infinite Objects. PhD thesis, The Weizmann Institue of Science, Rehovot, Israel (1989)"},{"key":"17_CR8","unstructured":"Michel, M.: Complementation is more difficult with automata on infinite words. Technical report, CNET Paris (1988)"},{"key":"17_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"97","DOI":"10.1007\/3-540-46691-6_8","volume-title":"Foundations of Software Technology and Theoretical Computer Science","author":"C. L\u00f6ding","year":"1999","unstructured":"L\u00f6ding, C.: Optimal bounds for the transformation of omega-automata. In: Pandu Rangan, C., Raman, V., Ramanujam, R. (eds.) FST TCS 1999. LNCS, vol.\u00a01738, pp. 97\u2013109. Springer, Heidelberg (1999)"},{"key":"17_CR10","doi-asserted-by":"crossref","unstructured":"Kupferman, O., Vardi, M.Y.: Freedom, weakness, and determinism: From linear-time to branching-time. In: Proc. 13th IEEE Symposium on Logic in Computer Science, pp. 81\u201392 (1998)","DOI":"10.1109\/LICS.1998.705645"},{"key":"17_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"153","DOI":"10.1007\/3-540-44618-4_13","volume-title":"CONCUR 2000 - Concurrency Theory","author":"K. Etessami","year":"2000","unstructured":"Etessami, K., Holzmann, G.J.: Optimizing B\u00fcchi automata. In: Palamidessi, C. (ed.) CONCUR 2000. LNCS, vol.\u00a01877, pp. 153\u2013167. Springer, Heidelberg (2000)"},{"key":"17_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"248","DOI":"10.1007\/10722167_21","volume-title":"Computer Aided Verification","author":"F. Somenzi","year":"2000","unstructured":"Somenzi, F., Bloem, R.: Efficient B\u00fcchi automata from LTL formulae. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol.\u00a01855, pp. 248\u2013263. Springer, Heidelberg (2000)"},{"key":"17_CR13","doi-asserted-by":"crossref","unstructured":"Dwyer, M.B., Avrunin, G.S., Corbett, J.C.: Patterns in property specifications for finite-state verification. In: ICSE, pp. 411\u2013420 (1999)","DOI":"10.1145\/302405.302672"},{"key":"17_CR14","first-page":"995","volume-title":"Handbook of Theoretical Computer Science, vol. B: Formal Models and Semantics","author":"E.A. Emerson","year":"1990","unstructured":"Emerson, E.A.: Temporal and modal logic. In: van Leeuwen, J. (ed.) Handbook of Theoretical Computer Science, vol. B: Formal Models and Semantics, pp. 995\u20131072. Elsevier Science Publishers, Amsterdam (1990)"},{"key":"17_CR15","volume-title":"Model Checking","author":"E. Clarke","year":"2000","unstructured":"Clarke, E., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge (2000)"},{"key":"17_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"694","DOI":"10.1007\/3-540-48224-5_57","volume-title":"Automata, Languages and Programming","author":"K. Etessami","year":"2001","unstructured":"Etessami, K., Wilke, T., Schuller, R.A.: Fair simulation relations, parity games, and state space reduction for B\u00fcchi automata. In: Orejas, F., Spirakis, P.G., van Leeuwen, J. (eds.) ICALP 2001. LNCS, vol.\u00a02076, pp. 694\u2013707. Springer, Heidelberg (2001)"},{"key":"17_CR17","unstructured":"Klein, J.: Linear time logic and deterministic omega-automata. Diploma thesis, Universit\u00e4t Bonn, Institut f\u00fcr Informatik (2005)"},{"key":"17_CR18","doi-asserted-by":"publisher","first-page":"973","DOI":"10.1137\/0216062","volume":"16","author":"R. Paige","year":"1987","unstructured":"Paige, R., Tarjan, R.E.: Three partition refinement algorithms. SIAM Journal on Computing\u00a016, 973\u2013989 (1987)","journal-title":"SIAM Journal on Computing"},{"key":"17_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-48683-6_17","volume-title":"Computer Aided Verification","author":"O. Kupferman","year":"1999","unstructured":"Kupferman, O., Vardi, M.Y.: Model checking of safety properties. In: Halbwachs, N., Peled, D.A. (eds.) CAV 1999. LNCS, vol.\u00a01633, Springer, Heidelberg (1999)"},{"key":"17_CR20","unstructured":"Latvala, T.: On model checking safety properties. Research Report A76, Helsinki University of Technology, Laboratory for Theoretical Computer Science, Espoo, Finland (2002)"},{"key":"17_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"261","DOI":"10.1007\/3-540-60385-9_16","volume-title":"Correct Hardware Design and Verification Methods","author":"S. Tasiran","year":"1995","unstructured":"Tasiran, S., Hojati, R., Brayton, R.K.: Language containment of non-deterministic \u03c9-automata. In: Camurati, P.E., Eveking, H. (eds.) CHARME 1995. LNCS, vol.\u00a0987, pp. 261\u2013277. Springer, Heidelberg (1995)"},{"key":"17_CR22","unstructured":"Tauriainen, H.: Automated testing of B\u00fcchi automata translators for linear temporal logic. Research report, Helsinki University of Technology, Laboratory for Theoretical Computer Science (2000)"},{"key":"17_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"126","DOI":"10.1007\/978-3-540-39724-3_12","volume-title":"Correct Hardware Design and Verification Methods","author":"R. Sebastiani","year":"2003","unstructured":"Sebastiani, R., Tonetta, S.: More Deterministic vs. \u201dSmaller\u201d B\u00fcchi Automata for Efficient LTL Model Checking. In: Geist, D., Tronci, E. (eds.) CHARME 2003. LNCS, vol.\u00a02860, pp. 126\u2013140. Springer, Heidelberg (2003)"},{"key":"17_CR24","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1109\/32.588521","volume":"23","author":"G.J. Holzmann","year":"1997","unstructured":"Holzmann, G.J.: The Model Checker Spin. IEEE Trans. on Software Engineering\u00a023, 279\u2013295 (1997), Special issue on Formal Methods in Software Practice","journal-title":"IEEE Trans. on Software Engineering"},{"key":"17_CR25","series-title":"IFIP Conference Proceedings","first-page":"3","volume-title":"Proc. PSTV 1995","author":"R. Gerth","year":"1995","unstructured":"Gerth, R., Peled, D., Vardi, M.Y., Wolper, P.: Simple on-the-fly automatic verification of linear temporal logic. In: Proc. PSTV 1995. IFIP Conference Proceedings, vol.\u00a038, pp. 3\u201318. Chapman and Hall, Boca Raton (1995)"},{"key":"17_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"35","DOI":"10.1007\/3-540-45089-0_5","volume-title":"Implementation and Application of Automata","author":"C. Fritz","year":"2003","unstructured":"Fritz, C.: Constructing B\u00fcchi automata from linear temporal logic using simulation relations for alternating B\u00fcchi automata. In: H. Ibarra, O., Dang, Z. (eds.) CIAA 2003. LNCS, vol.\u00a02759, pp. 35\u201348. Springer, Heidelberg (2003)"},{"key":"17_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"53","DOI":"10.1007\/3-540-44585-4_6","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, pp. 53\u201365. Springer, Heidelberg (2001)"},{"key":"17_CR28","doi-asserted-by":"publisher","first-page":"69","DOI":"10.1016\/0304-3975(94)00214-4","volume":"141","author":"D.E. Muller","year":"1995","unstructured":"Muller, D.E., Schupp, P.E.: Simulating alternating tree automata by nondeterministic automata: New results and new proofs of the theorems of Rabin, McNaughton and Safra. Theoretical Computer Science\u00a0141, 69\u2013107 (1995)","journal-title":"Theoretical Computer Science"},{"key":"17_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/11605157_22","volume-title":"Implementation and Application of Automata","author":"C.S. Althoff","year":"2006","unstructured":"Althoff, C.S., 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, Springer, Heidelberg (2006)"},{"key":"17_CR30","first-page":"14","volume-title":"STOC 1984","author":"E.A. Emerson","year":"1984","unstructured":"Emerson, E.A., Sistla, A.P.: Deciding branching time logic. In: STOC 1984, pp. 14\u201324. ACM Press, New York (1984)"},{"key":"17_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"378","DOI":"10.1007\/3-540-58325-4_202","volume-title":"Algorithms and Computation","author":"S.C. Krishnan","year":"1994","unstructured":"Krishnan, S.C., Puri, A., Brayton, R.K.: Deterministic \u03c9 Automata vis-a-vis Deterministic Buchi Automata. In: Du, D.-Z., Zhang, X.-S. (eds.) ISAAC 1994. LNCS, vol.\u00a0834, pp. 378\u2013386. Springer, Heidelberg (1994)"},{"key":"17_CR32","doi-asserted-by":"publisher","first-page":"105","DOI":"10.1016\/S0020-0190(00)00183-6","volume":"79","author":"C. L\u00f6ding","year":"2001","unstructured":"L\u00f6ding, C.: Efficient minimization of deterministic weak omega-automata. Information Processing Letters\u00a079, 105\u2013109 (2001)","journal-title":"Information Processing Letters"}],"container-title":["Lecture Notes in Computer Science","Implementation and Application of Automata"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11605157_17.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T07:05:15Z","timestamp":1619507115000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11605157_17"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006]]},"ISBN":["9783540310235","9783540330974"],"references-count":32,"URL":"https:\/\/doi.org\/10.1007\/11605157_17","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2006]]}}}