{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,18]],"date-time":"2026-01-18T01:31:39Z","timestamp":1768699899082,"version":"3.49.0"},"publisher-location":"Berlin, Heidelberg","reference-count":20,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642198342","type":"print"},{"value":"9783642198359","type":"electronic"}],"license":[{"start":{"date-parts":[[2011,1,1]],"date-time":"2011-01-01T00:00:00Z","timestamp":1293840000000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2011]]},"DOI":"10.1007\/978-3-642-19835-9_23","type":"book-chapter","created":{"date-parts":[[2011,3,14]],"date-time":"2011-03-14T11:03:16Z","timestamp":1300100596000},"page":"262-266","source":"Crossref","is-referenced-by-count":8,"title":["B\u00fcchi Store: An Open Repository of B\u00fcchi Automata"],"prefix":"10.1007","author":[{"given":"Yih-Kuen","family":"Tsay","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ming-Hsien","family":"Tsai","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jinn-Shu","family":"Chang","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Yi-Wen","family":"Chang","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"23_CR1","unstructured":"B\u00fcchi, J.R.: On a decision method in restricted second-order arithmetic. In: Int\u2019l Congress on Logic, Methodology and Philosophy of Science, pp. 1\u201311 (1962)"},{"key":"23_CR2","unstructured":"CodeIgniter, \n                    \n                      http:\/\/codeigniter.com\/"},{"key":"23_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"253","DOI":"10.1007\/3-540-48119-2_16","volume-title":"FM\u201999 - Formal Methods","author":"J.M. Couvreur","year":"1999","unstructured":"Couvreur, J.M.: On-the-fly verification of linear temporal logic. In: Woodcock, J.C.P., Davies, J. (eds.) FM 1999. LNCS, vol.\u00a01708, pp. 253\u2013271. Springer, Heidelberg (1999)"},{"key":"23_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"249","DOI":"10.1007\/3-540-48683-6_23","volume-title":"Computer Aided Verification","author":"M. Daniele","year":"1999","unstructured":"Daniele, M., Giunchiglia, F., Vardi, M.Y.: Improved automata generation for linear temporal logic. In: Halbwachs, N., Peled, D.A. (eds.) CAV 1999. LNCS, vol.\u00a01633, pp. 249\u2013260. Springer, Heidelberg (1999)"},{"key":"23_CR5","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":"23_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"308","DOI":"10.1007\/3-540-36135-9_20","volume-title":"Formal Techniques for Networked and Distributed Systems - FORTE 2002","author":"D. Giannakopoulou","year":"2002","unstructured":"Giannakopoulou, D., Lerda, F.: From states to transitions: Improving translation of LTL formulae to B\u00fcchi automata. In: Peled, D.A., Vardi, M.Y. (eds.) FORTE 2002. LNCS, vol.\u00a02529, pp. 308\u2013326. Springer, Heidelberg (2002)"},{"key":"23_CR7","volume-title":"The SPIN Model Checker: Primer and Reference Manual","author":"G.J. Holzmann","year":"2003","unstructured":"Holzmann, G.J.: The SPIN Model Checker: Primer and Reference Manual. Addison-Wesley, Reading (2003)"},{"key":"23_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"724","DOI":"10.1007\/978-3-540-70575-8_59","volume-title":"Automata, Languages and Programming","author":"D. K\u00e4hler","year":"2008","unstructured":"K\u00e4hler, D., Wilke, T.: Complementation, disambiguation, and determinization of B\u00fcchi automata unified. In: Aceto, L., Damg\u00e5rd, I., Goldberg, L.A., Halld\u00f3rsson, M.M., Ing\u00f3lfsd\u00f3ttir, A., Walukiewicz, I. (eds.) ICALP 2008, Part I. LNCS, vol.\u00a05125, pp. 724\u2013735. Springer, Heidelberg (2008)"},{"issue":"3","key":"23_CR9","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 Transactions on Computational Logic\u00a02(3), 408\u2013429 (2001)","journal-title":"ACM Transactions on Computational Logic"},{"key":"23_CR10","doi-asserted-by":"publisher","first-page":"377","DOI":"10.1145\/93385.93442","volume-title":"PODC","author":"Z. Manna","year":"1990","unstructured":"Manna, Z., Pnueli, A.: A hierarchy of temporal properties. In: PODC, pp. 377\u2013408. ACM, New York (1990)"},{"key":"23_CR11","unstructured":"Michel, M.: Complementation is more difficult with automata on infinite words. In: CNET, Paris (1988)"},{"key":"23_CR12","first-page":"255","volume-title":"LICS","author":"N. Piterman","year":"2006","unstructured":"Piterman, N.: From nondeterministic B\u00fcchi and Streett automata to deterministic parity automata. In: LICS, pp. 255\u2013264. IEEE, Los Alamitos (2006)"},{"key":"23_CR13","first-page":"319","volume-title":"FOCS","author":"S. Safra","year":"1988","unstructured":"Safra, S.: On the complexity of \u03c9-automta. In: FOCS, pp. 319\u2013327. IEEE, Los Alamitos (1988)"},{"key":"23_CR14","unstructured":"Schewe, S.: B\u00fcchi complementation made tight. In: STACS, pp. 661\u2013672 (2009)"},{"key":"23_CR15","unstructured":"Sistla, A.P.: Theoretical Issues in the Design and Verification of Distributed Systems. PhD thesis, Harvard (1983)"},{"key":"23_CR16","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":"23_CR17","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":"23_CR18","unstructured":"The Spec Patterns repository, \n                    \n                      http:\/\/patterns.projects.cis.ksu.edu\/"},{"key":"23_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"346","DOI":"10.1007\/978-3-540-78800-3_26","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"Y.-K. Tsay","year":"2008","unstructured":"Tsay, Y.-K., Chen, Y.-F., Tsai, M.-H., Chan, W.-C., Luo, C.-J.: GOAL extended: Towards a research tool for omega automata and temporal logic. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol.\u00a04963, pp. 346\u2013350. Springer, Heidelberg (2008)"},{"key":"23_CR20","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. In: LICS, pp. 332\u2013344. IEEE, Los Alamitos (1986)"}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-19835-9_23","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,21]],"date-time":"2019-05-21T06:48:24Z","timestamp":1558421304000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-19835-9_23"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011]]},"ISBN":["9783642198342","9783642198359"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-19835-9_23","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2011]]}}}