{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,9]],"date-time":"2024-09-09T14:24:04Z","timestamp":1725891844453},"publisher-location":"Berlin, Heidelberg","reference-count":26,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540472377"},{"type":"electronic","value":"9783540472384"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2006]]},"DOI":"10.1007\/11901914_12","type":"book-chapter","created":{"date-parts":[[2006,10,10]],"date-time":"2006-10-10T05:21:43Z","timestamp":1160457703000},"page":"125-140","source":"Crossref","is-referenced-by-count":1,"title":["On the Succinctness of Nondeterminism"],"prefix":"10.1007","author":[{"given":"Benjamin","family":"Aminof","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Orna","family":"Kupferman","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"12_CR1","doi-asserted-by":"publisher","first-page":"181","DOI":"10.1016\/0020-0190(85)90056-0","volume":"21","author":"B. Alpern","year":"1985","unstructured":"Alpern, B., Schneider, F.B.: Defining liveness. IPL\u00a021, 181\u2013185 (1985)","journal-title":"IPL"},{"key":"12_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"211","DOI":"10.1007\/3-540-46002-0_21","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"R. Armoni","year":"2002","unstructured":"Armoni, R., Fix, L., Flaisher, A., Gerth, R., Ginsburg, B., Kanza, T., Landver, A., Mador-Haim, S., Singerman, E., Tiemeyer, A., Vardi, M.Y., Zbar, Y.: The ForSpec temporal logic: A new temporal property-specification logic. In: Katoen, J.-P., Stevens, P. (eds.) ETAPS 2002 and TACAS 2002. LNCS, vol.\u00a02280, pp. 211\u2013296. Springer, Heidelberg (2002)"},{"key":"12_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"363","DOI":"10.1007\/3-540-44585-4_33","volume-title":"Computer Aided Verification","author":"I. Beer","year":"2001","unstructured":"Beer, I., Ben-David, S., Eisner, C., Fisman, D., Gringauze, A., Rodeh, Y.: The temporal logic Sugar. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol.\u00a02102, pp. 363\u2013367. Springer, Heidelberg (2001)"},{"key":"12_CR4","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"611","DOI":"10.1007\/3-540-45744-5_50","volume-title":"Automated Reasoning","author":"B. Boigelot","year":"2001","unstructured":"Boigelot, B., Jodogne, S., Wolper, P.: On the use of weak automata for deciding linear arithmetic with integer and real variables. In: Gor\u00e9, R.P., Leitsch, A., Nipkow, T. (eds.) IJCAR 2001. LNCS (LNAI), vol.\u00a02083, pp. 611\u2013625. Springer, Heidelberg (2001)"},{"key":"12_CR5","unstructured":"B\u00fcchi, J.R.: On a decision method in restricted second order arithmetic. In: Proc. International Congress on Logic, Method, and Philosophy of Science. 1960, Stanford, pp. 1\u201312 (1962)"},{"issue":"1","key":"12_CR6","doi-asserted-by":"publisher","first-page":"7","DOI":"10.1023\/A:1011276507260","volume":"19","author":"E.M. Clarke","year":"2001","unstructured":"Clarke, E.M., Bierea, A., Raimi, R., Zhu, Y.: Bounded model checking using satisfiability solving. Formal Methods in System Design\u00a019(1), 7\u201334 (2001)","journal-title":"Formal Methods in System Design"},{"key":"12_CR7","unstructured":"Accellera\u00a0Organization Inc, http:\/\/www.accellera.org"},{"key":"12_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","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 B\u00fcchi automata. In: Du, D.-Z., Zhang, X.-S. (eds.) ISAAC 1994. LNCS, vol.\u00a0834, pp. 378\u2013386. Springer, Heidelberg (1994)"},{"key":"12_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"324","DOI":"10.1007\/978-3-540-30476-0_27","volume-title":"Automated Technology for Verification and Analysis","author":"O. Kupferman","year":"2004","unstructured":"Kupferman, O., Morgenstern, G., Murano, A.: Typeness for \u03c9-regular automata. In: Wang, F. (ed.) ATVA 2004. LNCS, vol.\u00a03299, pp. 324\u2013338. Springer, Heidelberg (2004)"},{"key":"12_CR10","doi-asserted-by":"crossref","unstructured":"Kupferman, O., Safra, S., Vardi, M.Y.: Relating word and tree automata. In: Proc. 11th LICS, DIMACS, pp. 322\u2013333 (June 1996)","DOI":"10.1109\/LICS.1996.561360"},{"key":"12_CR11","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"24","DOI":"10.1007\/3-540-45653-8_2","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"O. Kupferman","year":"2001","unstructured":"Kupferman, O., Vardi, M.Y.: On bounded specifications. In: Nieuwenhuis, R., Voronkov, A. (eds.) LPAR 2001. LNCS (LNAI), vol.\u00a02250, pp. 24\u201338. Springer, Heidelberg (2001)"},{"issue":"2","key":"12_CR12","doi-asserted-by":"publisher","first-page":"273","DOI":"10.1145\/1055686.1055689","volume":"6","author":"O. Kupferman","year":"2005","unstructured":"Kupferman, O., Vardi, M.Y.: From linear time to branching time. ACM TOCL\u00a06(2), 273\u2013294 (2005)","journal-title":"ACM TOCL"},{"key":"12_CR13","volume-title":"Computer Aided Verification of Coordinating Processes","author":"R.P. Kurshan","year":"1994","unstructured":"Kurshan, R.P.: Computer Aided Verification of Coordinating Processes. Princeton University Press, Princeton (1994)"},{"key":"12_CR14","doi-asserted-by":"publisher","first-page":"376","DOI":"10.1007\/BF01691063","volume":"3","author":"L.H. Landweber","year":"1969","unstructured":"Landweber, L.H.: Decision problems for \u03c9\u2013automata. Mathematical Systems Theory\u00a03, 376\u2013384 (1969)","journal-title":"Mathematical Systems Theory"},{"key":"12_CR15","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)"},{"issue":"3","key":"12_CR16","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. IPL\u00a079(3), 105\u2013109 (2001)","journal-title":"IPL"},{"key":"12_CR17","first-page":"521","volume":"9","author":"R. McNaughton","year":"1966","unstructured":"McNaughton, R.: Testing and generating infinite sequences by a finite automation. I& C\u00a09, 521\u2013530 (1966)","journal-title":"I& C"},{"key":"12_CR18","doi-asserted-by":"crossref","unstructured":"Meyer, A.R., Fischer, M.J.: Economy of description by automata, grammars, and formal systems. In: Proc. 12th SSAT, pp. 188\u2013191 (1971)","DOI":"10.1109\/SWAT.1971.11"},{"key":"12_CR19","unstructured":"Michel, M.: Complementation is more difficult with automata on infinite words. CNET, Paris (1988)"},{"key":"12_CR20","doi-asserted-by":"publisher","first-page":"321","DOI":"10.1016\/0304-3975(84)90049-5","volume":"32","author":"S. Miyano","year":"1984","unstructured":"Miyano, S., Hayashi, T.: Alternating finite automata on \u03c9-words. TCS\u00a032, 321\u2013330 (1984)","journal-title":"TCS"},{"key":"12_CR21","doi-asserted-by":"publisher","first-page":"1","DOI":"10.2307\/1995086","volume":"141","author":"M.O. Rabin","year":"1969","unstructured":"Rabin, M.O.: Decidability of second order theories and automata on infinite trees. Transaction of the AMS\u00a0141, 1\u201335 (1969)","journal-title":"Transaction of the AMS"},{"key":"12_CR22","doi-asserted-by":"crossref","unstructured":"Safra, S.: On the complexity of \u03c9-automata. In: Proc. 29th FOCS, pp. 319\u2013327 (1988)","DOI":"10.1109\/SFCS.1988.21948"},{"key":"12_CR23","doi-asserted-by":"crossref","unstructured":"Safra, S., Vardi, M.Y.: On \u03c9-automata and temporal logic. In: Proc. 21st ACM STOC, pp. 127\u2013137 (1989)","DOI":"10.1145\/73007.73019"},{"key":"12_CR24","doi-asserted-by":"publisher","first-page":"495","DOI":"10.1007\/BF01211865","volume":"6","author":"A.P. Sistla","year":"1994","unstructured":"Sistla, A.P.: Safety, liveness and fairness in temporal logic. Formal Aspects of Computing\u00a06, 495\u2013511 (1994)","journal-title":"Formal Aspects of Computing"},{"key":"12_CR25","doi-asserted-by":"crossref","unstructured":"Thomas, W.: Automata on infinite objects. In: Handbook of Theoretical Computer Science, pp. 133\u2013191 (1990)","DOI":"10.1016\/B978-0-444-88074-1.50009-3"},{"issue":"1","key":"12_CR26","first-page":"1","volume":"115","author":"M.Y. Vardi","year":"1994","unstructured":"Vardi, M.Y., Wolper, P.: Reasoning about infinite computations. I& C\u00a0115(1), 1\u201337 (1994)","journal-title":"I& C"}],"container-title":["Lecture Notes in Computer Science","Automated Technology for Verification and Analysis"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11901914_12.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T19:56:10Z","timestamp":1605642970000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11901914_12"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006]]},"ISBN":["9783540472377","9783540472384"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/11901914_12","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2006]]}}}