{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T04:52:14Z","timestamp":1725511934312},"publisher-location":"Berlin, Heidelberg","reference-count":16,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540712084"},{"type":"electronic","value":"9783540712091"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-71209-1_34","type":"book-chapter","created":{"date-parts":[[2007,7,4]],"date-time":"2007-07-04T22:56:34Z","timestamp":1183589794000},"page":"451-465","source":"Crossref","is-referenced-by-count":20,"title":["Improved Algorithms for the Automata-Based Approach to Model-Checking"],"prefix":"10.1007","author":[{"given":"Laurent","family":"Doyen","sequence":"first","affiliation":[]},{"given":"Jean-Fran\u00e7ois","family":"Raskin","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"issue":"2","key":"34_CR1","doi-asserted-by":"publisher","first-page":"166","DOI":"10.2307\/2271090","volume":"34","author":"J.R. B\u00fcchi","year":"1969","unstructured":"B\u00fcchi, J.R., Landweber, L.H.: Definability in the monadic second-order theory of successor. J. Symb. Log.\u00a034(2), 166\u2013170 (1969)","journal-title":"J. Symb. Log."},{"key":"34_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"17","DOI":"10.1007\/11817963_5","volume-title":"Computer Aided Verification","author":"M. Wulf De","year":"2006","unstructured":"De Wulf, M., et al.: Antichains: A new algorithm for checking universality of finite automata. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol.\u00a04144, pp. 17\u201330. Springer, Heidelberg (2006)"},{"key":"34_CR3","unstructured":"Doyen, L., Raskin, J.-F.: Improved Algorithms for the Automata-Based Approach to Model-Checking (extended version). Tech. Rep.\u00a076, U.L.B. \u2013 Federated Center in Verification (2006), \n                    \n                      http:\/\/www.ulb.ac.be\/di\/ssd\/cfv\/publications.html"},{"issue":"5","key":"34_CR4","doi-asserted-by":"publisher","first-page":"1159","DOI":"10.1137\/S0097539703420675","volume":"34","author":"K. Etessami","year":"2005","unstructured":"Etessami, K., Wilke, T., Schuller, R.A.: Fair simulation relations, parity games, and state space reduction for b\u00fcchi automata. SIAM J. Comput.\u00a034(5), 1159\u20131175 (2005)","journal-title":"SIAM J. Comput."},{"key":"34_CR5","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":"34_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","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":"34_CR7","first-page":"147","volume-title":"Proceedings of ISTCS\u201997","author":"O. Kupferman","year":"1997","unstructured":"Kupferman, O., Vardi, M.Y.: Weak alternating automata are not that weak. In: Proceedings of ISTCS\u201997, pp. 147\u2013158. IEEE Computer Society Press, Los Alamitos (1997)"},{"key":"34_CR8","unstructured":"Miyano, S., Hayashi, T.: Alternating finite automata on omega-words. In: CAAP, pp. 195\u2013210 (1984)"},{"key":"34_CR9","unstructured":"Michel, M.: Complementation is more difficult with automata on infinite words. In: CNET, Paris (1988)"},{"key":"34_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"304","DOI":"10.1007\/978-3-540-24732-6_21","volume-title":"Model Checking Software","author":"T.C. Ruys","year":"2004","unstructured":"Ruys, T.C., Holzmann, G.J.: Advanced spin tutorial. In: Graf, S., Mounier, L. (eds.) SPIN 2004. LNCS, vol.\u00a02989, pp. 304\u2013305. Springer, Heidelberg (2004)"},{"key":"34_CR11","first-page":"319","volume-title":"Proc. of FOCS: Foundations of Computer Science","author":"S. Safra","year":"1988","unstructured":"Safra, S.: On the complexity of \u03c9-automata. In: Proc. of FOCS: Foundations of Computer Science, pp. 319\u2013327. IEEE Computer Society Press, Los Alamitos (1988)"},{"key":"34_CR12","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. Theor. Comput. Sci.\u00a049, 217\u2013237 (1987)","journal-title":"Theor. Comput. Sci."},{"key":"34_CR13","unstructured":"Tabakov, D.: Experimental evaluation of explicit and symbolic approaches to complementation of non-deterministic buechi automata. Talk at \u201cGames and Verification\u201d workshop, Newton Institute for Math. Sciences (July 2006)"},{"key":"34_CR14","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"396","DOI":"10.1007\/11591191_28","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"D. Tabakov","year":"2005","unstructured":"Tabakov, D., Vardi, M.Y.: Experimental evaluation of classical automata constructions. In: Sutcliffe, G., Voronkov, A. (eds.) LPAR 2005. LNCS (LNAI), vol.\u00a03835, pp. 396\u2013411. Springer, Heidelberg (2005)"},{"key":"34_CR15","first-page":"332","volume-title":"LICS","author":"M.Y. Vardi","year":"1986","unstructured":"Vardi, M.Y., Wolper, P.: An automata-theoretic approach to automatic program verification (prelim. report). In: LICS, pp. 332\u2013344. IEEE Computer Society Press, Los Alamitos (1986)"},{"issue":"1","key":"34_CR16","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1006\/inco.1994.1092","volume":"115","author":"M.Y. Vardi","year":"1994","unstructured":"Vardi, M.Y., Wolper, P.: Reasoning about infinite computations. Inf. Comput.\u00a0115(1), 1\u201337 (1994)","journal-title":"Inf. Comput."}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-71209-1_34.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,19]],"date-time":"2020-11-19T05:16:48Z","timestamp":1605763008000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-71209-1_34"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540712084","9783540712091"],"references-count":16,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-71209-1_34","relation":{},"subject":[]}}