{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,4,30]],"date-time":"2025-04-30T04:21:47Z","timestamp":1745986907732,"version":"3.40.4"},"reference-count":35,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2013,2,3]],"date-time":"2013-02-03T00:00:00Z","timestamp":1359849600000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Int J Softw Tools Technol Transfer"],"published-print":{"date-parts":[[2013,4]]},"DOI":"10.1007\/s10009-012-0268-4","type":"journal-article","created":{"date-parts":[[2013,2,2]],"date-time":"2013-02-02T02:57:29Z","timestamp":1359773849000},"page":"109-123","source":"Crossref","is-referenced-by-count":6,"title":["B\u00fcchi Store: an open repository of $$\\omega $$ -automata"],"prefix":"10.1007","volume":"15","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"}]},{"given":"Chi-Shiang","family":"Liu","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2013,2,3]]},"reference":[{"key":"268_CR1","doi-asserted-by":"crossref","unstructured":"Boker, U., Kupferman, O.: Co-ing B\u00fcchi made tight and useful. In: Proceedings of the 24th annual IEEE symposium on logic in computer science (LICS \u201909), pp. 245\u2013254. IEEE Computer Society (2009)","DOI":"10.1109\/LICS.2009.32"},{"key":"268_CR2","unstructured":"B\u00fcchi J.R.: On a decision method in restricted second-order arithmetic. In: Proceedings of the 1960 international congress on logic, methodology and, philosophy of science, pp. 1\u201311 (1962)"},{"key":"268_CR3","doi-asserted-by":"crossref","unstructured":"Chatterjee, K., Henzinger, T.A., Jobstmann, B., Singh, R.: QUASY: Quantitative synthesis tool. In: Proceedings of the 17th international conference on tools and algorithms for the construction and analysis of systems (TACAS \u201911), LNCS 6605, pp. 267\u2013271. Springer, Heidelberg (2011)","DOI":"10.1007\/978-3-642-19835-9_24"},{"key":"268_CR4","doi-asserted-by":"crossref","unstructured":"Cicho\u0144 J., Czubak A., Jasi\u0144ski A.: Minimal B\u00fcchi automata for certain classes of LTL formulas. In: Proceedings of the fourth international conference on dependability of computer systems, pp. 17\u201324. IEEE (2009)","DOI":"10.1109\/DepCoS-RELCOMEX.2009.31"},{"key":"268_CR5","unstructured":"CodeIgniter. http:\/\/codeigniter.com\/"},{"key":"268_CR6","doi-asserted-by":"crossref","unstructured":"Couvreur, J.M.: On-the-fly verification of linear temporal logic. In: World Congress on formal methods in the development of computing systems (FM \u201999), LNCS 1708, pp. 253\u2013271. Springer, Heidelberg (1999)","DOI":"10.1007\/3-540-48119-2_16"},{"key":"268_CR7","doi-asserted-by":"crossref","unstructured":"Daniele, M., Giunchiglia, F., Vardi, M.Y.: Improved automata generation for linear temporal logic. In: Proceedings of the 11th international conference on computer-aided verification (CAV \u201999), LNCS 1633, pp. 249\u2013260. Springer, Heidelberg (1999)","DOI":"10.1007\/3-540-48683-6_23"},{"key":"268_CR8","doi-asserted-by":"crossref","unstructured":"Dwyer, M.B., Avrunin, G.S., Corbett, J.C.: Patterns in property specifications for finite-state verification. In: Proceedings of the 21st international conference on software engineering (ICSE \u201999), pp. 411\u2013420 (1999)","DOI":"10.1145\/302405.302672"},{"key":"268_CR9","doi-asserted-by":"crossref","unstructured":"Etessami K., Holzmann G.J.: Optimizing B\u00fcchi automata. In: Proceedings of the 11th international conference on concurrency theory (CONCUR \u201900), LNCS 1877, pp. 153\u2013167. Springer, Heidelberg (2000)","DOI":"10.1007\/3-540-44618-4_13"},{"key":"268_CR10","unstructured":"Gastin, P., Oddoux, D.: LTL 2 BA: fast translation from LTL formulae to B\u00fcchi automata. http:\/\/www.lsv.ens-cachan.fr\/gastin\/"},{"key":"268_CR11","doi-asserted-by":"crossref","unstructured":"Gastin P., Oddoux D.: Fast LTL to B\u00fcchi automata translation. In: Proceedings of the 13th international conference on computer-aided verification (CAV \u201901), LNCS 2102, pp. 53\u201365. Springer, Heidelberg (2001)","DOI":"10.1007\/3-540-44585-4_6"},{"key":"268_CR12","doi-asserted-by":"crossref","unstructured":"Giannakopoulou D., Lerda F.: From states to transitions: improving translation of LTL formulae to B\u00fcchi automata. In: Proceedings of the IFIP WG 6.1 international conference on formal techniques for networked and distributed sytems (FORTE \u201902), LNCS 2529, pp. 308\u2013326. Springer, Heidelberg (2002)","DOI":"10.1007\/3-540-36135-9_20"},{"key":"268_CR13","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-36387-4","volume-title":"Automata, logics, and infinite games (LNCS 2500)","author":"E Gr\u00e4del","year":"2002","unstructured":"Gr\u00e4del, E., Thomas, W., Wilke, T.: Automata, logics, and infinite games (LNCS 2500). Springer, Heidelberg (2002)"},{"key":"268_CR14","volume-title":"The SPIN model checker: primer and reference manual","author":"GJ Holzmann","year":"2003","unstructured":"Holzmann, G.J.: The SPIN model checker: primer and reference manual. Addison-Wesley, Boston (2003)"},{"key":"268_CR15","doi-asserted-by":"crossref","unstructured":"K\u00e4hler, D., Wilke, T.: Complementation, disambiguation, and determinization of B\u00fcchi automata unified. In: Proceedings of the 35th international colloqium on automata, languages, and programming (ICALP \u201908), LNCS 5125, pp. 724\u2013735. Springer, Heidelberg (2008)","DOI":"10.1007\/978-3-540-70575-8_59"},{"issue":"5","key":"268_CR16","doi-asserted-by":"crossref","first-page":"701","DOI":"10.1093\/logcom\/12.5.701","volume":"12","author":"Y Kesten","year":"2002","unstructured":"Kesten, Y., Pnueli, A.: Complete proof system for QPTL. J. Logic Comput. 12(5), 701\u2013745 (2002)","journal-title":"J. Logic Comput."},{"issue":"3","key":"268_CR17","doi-asserted-by":"crossref","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 Trans. Comput. Logic 2(3), 408\u2013429 (2001)","journal-title":"ACM Trans. Comput. Logic"},{"issue":"4","key":"268_CR18","doi-asserted-by":"crossref","first-page":"376","DOI":"10.1007\/BF01691063","volume":"3","author":"LH Landweber","year":"1969","unstructured":"Landweber, L.H.: Decision problems for $$\\omega $$ -automata. Math. Syst. Theory 3(4), 376\u2013384 (1969)","journal-title":"Math. Syst. Theory"},{"key":"268_CR19","doi-asserted-by":"crossref","unstructured":"Manna, Z., Pnueli, A.: A hierarchy of temporal properties. In: Proceedings of the 9th ACM symposium on principles of distributed computing (PODC \u201990), pp. 377\u2013408. ACM (1990)","DOI":"10.1145\/93385.93442"},{"key":"268_CR20","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4612-0931-7","volume-title":"The temporal logic of reactive and concurrent systems: specification","author":"Z Manna","year":"1992","unstructured":"Manna, Z., Pnueli, A.: The temporal logic of reactive and concurrent systems: specification. Springer, Heidelberg (1992)"},{"key":"268_CR21","unstructured":"Michel, M.: Complementation is more difficult with automata on infinite words. In: CNET, Paris (1988)"},{"key":"268_CR22","unstructured":"PHP\/Java Bridge. http:\/\/php-java-bridge.sourceforge.net\/"},{"key":"268_CR23","doi-asserted-by":"crossref","unstructured":"Piterman, N.: From nondeterministic B\u00fcchi and Streett automata to deterministic parity automata. In: Proceedings of the 21th annual IEEE symposium on logic in computer science (LICS \u201906), pp. 255\u2013264. IEEE (2006)","DOI":"10.1109\/LICS.2006.28"},{"key":"268_CR24","doi-asserted-by":"crossref","unstructured":"Safra, S.: On the complexity of $$\\omega $$ -automta. In: Proceedings of the 29th annual IEEE symposium on foundations of computer science (FOCS \u201988), pp. 319\u2013327. IEEE (1988)","DOI":"10.1109\/SFCS.1988.21948"},{"key":"268_CR25","unstructured":"Schewe, S.: B\u00fcchi complementation made tight. In: Proceedings of the 26th international symposium on theoretical aspects of computer science (STACS \u201909), LIPIcs 3 Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, pp. 661\u2013672 (2009)"},{"key":"268_CR26","unstructured":"Sistla, A.P.: Theoretical issues in the design and verification of distributed systems. PhD thesis, Harvard (1983)"},{"key":"268_CR27","doi-asserted-by":"crossref","first-page":"217","DOI":"10.1016\/0304-3975(87)90008-9","volume":"49","author":"AP Sistla","year":"1987","unstructured":"Sistla, A.P., Vardi, M.Y., Wolper, P.: The complementation problem for B\u00fcchi automata with applications to temporal logic. Theo. Comp. Sci. 49, 217\u2013237 (1987)","journal-title":"Theo. Comp. Sci."},{"key":"268_CR28","doi-asserted-by":"crossref","unstructured":"Sohail, S., Somenzi, F., Ravi, K.: A hybrid algorithm for LTL games. In Proceedings of the 9th international conference on verification, model checking, and abstract interpretation (VMCAI \u201908), LNCS 4905, pp. 309\u2013323. Springer, Heidelberg (2008)","DOI":"10.1007\/978-3-540-78163-9_26"},{"key":"268_CR29","doi-asserted-by":"crossref","unstructured":"Somenzi, F., Bloem, R.: Efficient B\u00fcchi automata from LTL formulae. In Proceedings of the 12th international conference on computer-aided verification (CAV \u201900), LNCS 1855, pp. 248\u2013263. Springer, Heidelberg (2000)","DOI":"10.1007\/10722167_21"},{"key":"268_CR30","unstructured":"The Spec Patterns Repository. http:\/\/patterns.projects.cis.ksu.edu\/"},{"key":"268_CR31","unstructured":"Tomcat. http:\/\/tomcat.apache.org\/"},{"key":"268_CR32","doi-asserted-by":"crossref","unstructured":"Tsai, M.-H., Fogarty, S., Vardi, M.Y., Tsay, Y.-K.: State of B\u00fcchi complementation. In: Proceedings of the 15th international conference on implementation and application of automata (CIAA \u201910), LNCS 6482, pp. 261\u2013271. Springer, Heidelberg (2011)","DOI":"10.1007\/978-3-642-18098-9_28"},{"key":"268_CR33","doi-asserted-by":"crossref","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: Proceedings of the 14th international conference on tools and algorithms for the construction and analysis of systems (TACAS \u201908), LNCS 4963, pp. 346\u2013350. Springer, Heidelberg (2008)","DOI":"10.1007\/978-3-540-78800-3_26"},{"key":"268_CR34","unstructured":"Tsay, Y.-K., Tsai, M.-H., Chang, J.-S., Chang, Y.-W.: B\u00fcchi Store: an open repository of B\u00fcchi automata. In: Proceedings of the 17th international conference on tools and algorithms for the construction and analysis of systems (TACAS \u201911), LNCS 6605, pp. 262\u2013266. Springer, Heidelberg, (2011)"},{"key":"268_CR35","unstructured":"Vardi, M.Y., Wolper, P.: An automata-theoretic approach to automatic program verification. In: Proceedings of the 1st annual IEEE symposium on logic in computer science (LICS \u201986), pp. 332\u2013344. IEEE (1986)"}],"container-title":["International Journal on Software Tools for Technology Transfer"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-012-0268-4.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10009-012-0268-4\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-012-0268-4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,4,29]],"date-time":"2025-04-29T19:14:07Z","timestamp":1745954047000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10009-012-0268-4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013,2,3]]},"references-count":35,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2013,4]]}},"alternative-id":["268"],"URL":"https:\/\/doi.org\/10.1007\/s10009-012-0268-4","relation":{},"ISSN":["1433-2779","1433-2787"],"issn-type":[{"type":"print","value":"1433-2779"},{"type":"electronic","value":"1433-2787"}],"subject":[],"published":{"date-parts":[[2013,2,3]]}}}