{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T13:28:41Z","timestamp":1725542921359},"publisher-location":"Berlin, Heidelberg","reference-count":35,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540373766"},{"type":"electronic","value":"9783540373773"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2006]]},"DOI":"10.1007\/11817949_33","type":"book-chapter","created":{"date-parts":[[2006,8,2]],"date-time":"2006-08-02T19:59:29Z","timestamp":1154548769000},"page":"492-508","source":"Crossref","is-referenced-by-count":9,"title":["Finding Shortest Witnesses to the Nonemptiness of Automata on Infinite Words"],"prefix":"10.1007","author":[{"given":"Orna","family":"Kupferman","sequence":"first","affiliation":[]},{"given":"Sarai","family":"Sheinvald-Faragy","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"33_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"163","DOI":"10.1007\/BFb0055622","volume-title":"CONCUR \u201998 Concurrency Theory","author":"R. Alur","year":"1998","unstructured":"Alur, R., Henzinger, T.A., Kupferman, O., Vardi, M.Y.: Alternating refinement relations. In: Sangiorgi, D., de Simone, R. (eds.) CONCUR 1998. LNCS, vol.\u00a01466, pp. 163\u2013178. Springer, Heidelberg (1998)"},{"key":"33_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"197","DOI":"10.1007\/BFb0023733","volume-title":"Computer-Aided Verification","author":"A. Bouajjani","year":"1991","unstructured":"Bouajjani, A., Fernandez, J.-C., Halbwachs, N.: Minimal model genration. In: Clarke, E., Kurshan, R.P. (eds.) CAV 1990. LNCS, vol.\u00a0531, pp. 197\u2013203. Springer, Heidelberg (1991)"},{"issue":"3","key":"33_CR3","doi-asserted-by":"publisher","first-page":"237","DOI":"10.1007\/BF01371727","volume":"26","author":"J.C. Birget","year":"1993","unstructured":"Birget, J.C.: State-complexity of finite-state devices, state compressibility and incompressibility. Mathematical Systems Theory\u00a026(3), 237\u2013269 (1993)","journal-title":"Mathematical Systems Theory"},{"key":"33_CR4","doi-asserted-by":"publisher","first-page":"19","DOI":"10.1016\/0304-3975(80)90069-9","volume":"10","author":"J.A. Brzozowski","year":"1980","unstructured":"Brzozowski, J.A., Leiss, E.: Finite automata and sequential networks. TCS\u00a010, 19\u201335 (1980)","journal-title":"TCS"},{"key":"33_CR5","first-page":"1","volume-title":"Proc. International Congress on Logic, Method, and Philosophy of Science, 1960","author":"J.R. B\u00fcchi","year":"1962","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, pp. 1\u201312. Stanford University Press, Stanford (1962)"},{"key":"33_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"52","DOI":"10.1007\/BFb0025774","volume-title":"Logics of Programs","author":"E.M. Clarke","year":"1982","unstructured":"Clarke, E.M., Emerson, E.A.: Design and synthesis of synchronization skeletons using branching time temporal logic. In: Kozen, D. (ed.) Logic of Programs 1981. LNCS, vol.\u00a0131, pp. 52\u201371. Springer, Heidelberg (1982)"},{"issue":"5","key":"33_CR7","doi-asserted-by":"publisher","first-page":"752","DOI":"10.1145\/876638.876643","volume":"50","author":"E.M. Clarke","year":"2003","unstructured":"Clarke, E.M., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement for symbolic model checking. J. ACM\u00a050(5), 752\u2013794 (2003)","journal-title":"J. ACM"},{"key":"33_CR8","first-page":"427","volume-title":"Proc. 32nd DAC","author":"E.M. Clarke","year":"1995","unstructured":"Clarke, E.M., Grumberg, O., McMillan, K.L., Zhao, X.: Efficient generation of counterexamples and witnesses in symbolic model checking. In: Proc. 32nd DAC, pp. 427\u2013432. IEEE Computer Society, Los Alamitos (1995)"},{"issue":"1","key":"33_CR9","doi-asserted-by":"publisher","first-page":"114","DOI":"10.1145\/322234.322243","volume":"28","author":"A.K. Chandra","year":"1981","unstructured":"Chandra, A.K., Kozen, D.C., Stockmeyer, L.J.: Alternation. J. ACM\u00a028(1), 114\u2013133 (1981)","journal-title":"J. ACM"},{"issue":"3","key":"33_CR10","doi-asserted-by":"publisher","first-page":"517","DOI":"10.1145\/176584.176587","volume":"41","author":"D. Drusinsky","year":"1994","unstructured":"Drusinsky, D., Harel, D.: On the power of bounded concurrency I: Finite automata. J. ACM\u00a041(3), 517\u2013539 (1994)","journal-title":"J. ACM"},{"key":"33_CR11","doi-asserted-by":"crossref","unstructured":"Emerson, E.A., Jutla, C.: Tree automata, \u03bc-calculus and determinacy. In: Proc. 32nd FOCS, pp. 368\u2013377 (1991)","DOI":"10.1109\/SFCS.1991.185392"},{"key":"33_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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., Kupferman, O., Somenzi, F., Vardi, M.Y.: On Complementing Nondeterministic B\u00fcchi Automata. In: Geist, D., Tronci, E. (eds.) CHARME 2003. LNCS, vol.\u00a02860, pp. 96\u2013110. Springer, Heidelberg (2003)"},{"issue":"3","key":"33_CR13","doi-asserted-by":"publisher","first-page":"843","DOI":"10.1145\/177492.177725","volume":"16","author":"O. Grumberg","year":"1994","unstructured":"Grumberg, O., Long, D.E.: Model checking and modular verification. ACM TOPLAS\u00a016(3), 843\u2013871 (1994)","journal-title":"ACM TOPLAS"},{"key":"33_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"92","DOI":"10.1007\/978-3-540-24732-6_7","volume-title":"Model Checking Software","author":"P. Gastin","year":"2004","unstructured":"Gastin, P., Moro, P., Zeitoun, M.: Minimization of counterexamples in spin. In: Graf, S., Mounier, L. (eds.) SPIN 2004. LNCS, vol.\u00a02989, pp. 92\u2013108. Springer, Heidelberg (2004)"},{"key":"33_CR15","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)"},{"issue":"3","key":"33_CR16","first-page":"183","volume":"56","author":"H. Galperin","year":"1983","unstructured":"Galperin, H., Wigderson, A.: Succinct representations of graphs. I& C\u00a056(3), 183\u2013198 (1983)","journal-title":"I& C"},{"key":"33_CR17","doi-asserted-by":"publisher","first-page":"231","DOI":"10.1016\/0167-6423(87)90035-9","volume":"8","author":"D. Harel","year":"1987","unstructured":"Harel, D.: Statecharts: A visual formalism for complex systems. Sci. Computer Prog.\u00a08, 231\u2013274 (1987)","journal-title":"Sci. Computer Prog."},{"key":"33_CR18","first-page":"1","volume":"173","author":"D. Harel","year":"2002","unstructured":"Harel, D., Kupferman, O., Vardi, M.Y.: On the complexity of verifying concurrent transition systems. I & C\u00a0173, 1\u201319 (2002)","journal-title":"I & C"},{"key":"33_CR19","doi-asserted-by":"crossref","unstructured":"Harel, D., Rosner, R., Vardi, M.Y.: On the power of bounded concurrency iii: Reasoning about programs. In: Proc. 5th LICS, pp. 478\u2013488 (1990)","DOI":"10.1109\/LICS.1990.113770"},{"key":"33_CR20","series-title":"Undergraduate Mathematics Series","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4471-0613-5","volume-title":"Elementary Number Theory","author":"G.A. Jones","year":"1998","unstructured":"Jones, G.A., Jones, J.M., Tyrer-Jones, J.M.: Elementary Number Theory. Undergraduate Mathematics Series. Springer, Berlin (1998)"},{"key":"33_CR21","doi-asserted-by":"crossref","unstructured":"Kozen, D.: Lower bounds for natural proof systems. In: Proc. 18th FOCS, pp. 254\u2013266 (1977)","DOI":"10.1109\/SFCS.1977.16"},{"key":"33_CR22","unstructured":"Kupferman, O., Vardi, M.Y.: Verification of fair transition systems. CJTCS 1998(2) (1998)"},{"issue":"2","key":"33_CR23","doi-asserted-by":"publisher","first-page":"408","DOI":"10.1145\/377978.377993","volume":"2","author":"O. Kupferman","year":"2001","unstructured":"Kupferman, O., Vardi, M.Y.: Weak alternating automata are not that weak. ACM TOCL\u00a02(2), 408\u2013429 (2001)","journal-title":"ACM TOCL"},{"issue":"2","key":"33_CR24","doi-asserted-by":"crossref","first-page":"224","DOI":"10.1007\/s100090100062","volume":"4","author":"O. Kupferman","year":"2003","unstructured":"Kupferman, O., Vardi, M.Y.: Vacuity detection in temporal model checking. J. STTT\u00a04(2), 224\u2013233 (2003)","journal-title":"J. STTT"},{"key":"33_CR25","doi-asserted-by":"crossref","unstructured":"Kupferman, O., Vardi, M.Y.: Safraless decision procedures. In: Proc. 46th FOCS, pp. 531\u2013540 (2005)","DOI":"10.1109\/SFCS.2005.66"},{"issue":"2","key":"33_CR26","doi-asserted-by":"publisher","first-page":"312","DOI":"10.1145\/333979.333987","volume":"47","author":"O. Kupferman","year":"2000","unstructured":"Kupferman, O., Vardi, M.Y., Wolper, P.: An automata-theoretic approach to branching-time model checking. J. ACM\u00a047(2), 312\u2013360 (2000)","journal-title":"J. ACM"},{"key":"33_CR27","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":"33_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-10235-3","volume-title":"A Calculus of Communication Systems","author":"R. Milner","year":"1980","unstructured":"Milner, R.: A Calculus of Communication Systems. LNCS, vol.\u00a092. Springer, Heidelberg (1980)"},{"key":"33_CR29","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.E. Muller","year":"1986","unstructured":"Muller, D.E., Saoudi, A., Schupp, P.E.: 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":"33_CR30","volume-title":"Computational Complexity","author":"C.H. Papadimitriou","year":"1994","unstructured":"Papadimitriou, C.H.: Computational Complexity. Addison-Wesley, Reading (1994)"},{"key":"33_CR31","doi-asserted-by":"publisher","first-page":"177","DOI":"10.1016\/S0022-0000(70)80006-X","volume":"4","author":"W.J. Savitch","year":"1970","unstructured":"Savitch, W.J.: Relationship between nondeterministic and deterministic tape complexities. Journal on Computer and System Sciences\u00a04, 177\u2013192 (1970)","journal-title":"Journal on Computer and System Sciences"},{"key":"33_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"493","DOI":"10.1007\/978-3-540-31980-1_32","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"V. Schuppan","year":"2005","unstructured":"Schuppan, V., Biere, A.: Shortest counterexamples for symbolic model checking of LTL with past. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol.\u00a03440, pp. 493\u2013509. Springer, Heidelberg (2005)"},{"key":"33_CR33","doi-asserted-by":"publisher","first-page":"217","DOI":"10.1016\/0304-3975(87)90008-9","volume":"49","author":"A.P. Sistla","year":"1987","unstructured":"Sistla, A.P., Vardi, M.Y., Wolper, P.: The complementation problem for B\u00fcchi automata with applications to temporal logic. TCS\u00a049, 217\u2013237 (1987)","journal-title":"TCS"},{"key":"33_CR34","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"471","DOI":"10.1007\/BFb0015261","volume-title":"Computer Science Today","author":"M.Y. Vardi","year":"1995","unstructured":"Vardi, M.Y.: Alternating automata and program verification. In: van Leeuwen, J. (ed.) Computer Science Today. LNCS, vol.\u00a01000, pp. 471\u2013485. Springer, Heidelberg (1995)"},{"issue":"1","key":"33_CR35","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","CONCUR 2006 \u2013 Concurrency Theory"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11817949_33.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T07:29:56Z","timestamp":1619508596000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11817949_33"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006]]},"ISBN":["9783540373766","9783540373773"],"references-count":35,"URL":"https:\/\/doi.org\/10.1007\/11817949_33","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2006]]}}}