乐胖代购免代理版

{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,10]],"date-time":"2024-09-10T19:40:33Z","timestamp":1725997233427},"publisher-location":"Cham","reference-count":23,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030025076"},{"type":"electronic","value":"9783030025083"}],"license":[{"start":{"date-parts":[[2018,1,1]],"date-time":"2018-01-01T00:00:00Z","timestamp":1514764800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2018,1,1]],"date-time":"2018-01-01T00:00:00Z","timestamp":1514764800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2018]]},"DOI":"10.1007\/978-3-030-02508-3_2","type":"book-chapter","created":{"date-parts":[[2018,10,13]],"date-time":"2018-10-13T18:22:47Z","timestamp":1539454967000},"page":"11-34","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["LTL Semantic Tableaux and Alternating $$\\omega $$ \u03c9 -automata via Linear Factors"],"prefix":"10.1007","author":[{"ORCID":"http:\/\/orcid.org\/0000-0002-8165-3403","authenticated-orcid":false,"given":"Martin","family":"Sulzmann","sequence":"first","affiliation":[]},{"ORCID":"http:\/\/orcid.org\/0000-0002-9000-1239","authenticated-orcid":false,"given":"Peter","family":"Thiemann","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2018,10,15]]},"reference":[{"issue":"2","key":"2_CR1","doi-asserted-by":"publisher","first-page":"291","DOI":"10.1016\/0304-3975(95)00182-4","volume":"155","author":"VM Antimirov","year":"1996","unstructured":"Antimirov, V.M.: Partial derivatives of regular expressions and finite automaton constructions. Theor. Comput. Sci. 155(2), 291\u2013319 (1996). \n https:\/\/doi.org\/10.1016\/0304-3975(95)00182-4","journal-title":"Theor. Comput. Sci."},{"key":"2_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"95","DOI":"10.1007\/978-3-642-28756-5_8","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"T Babiak","year":"2012","unstructured":"Babiak, T., K\u0159et\u00ednsk\u00fd, M., \u0158eh\u00e1k, V., Strej\u010dek, J.: LTL to B\u00fcchi automata translation: fast and more deterministic. In: Flanagan, C., K\u00f6nig, B. (eds.) TACAS 2012. LNCS, vol. 7214, pp. 95\u2013109. Springer, Heidelberg (2012). \n https:\/\/doi.org\/10.1007\/978-3-642-28756-5_8"},{"key":"2_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"21","DOI":"10.1007\/978-3-319-19225-3_2","volume-title":"Descriptional Complexity of Formal Systems","author":"S Broda","year":"2015","unstructured":"Broda, S., Machiavelo, A., Moreira, N., Reis, R.: Partial derivative automaton for regular expressions with shuffle. In: Shallit, J., Okhotin, A. (eds.) DCFS 2015. LNCS, vol. 9118, pp. 21\u201332. Springer, Cham (2015). \n https:\/\/doi.org\/10.1007\/978-3-319-19225-3_2"},{"key":"2_CR4","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 1999 \u2014 Formal Methods","author":"J-M Couvreur","year":"1999","unstructured":"Couvreur, J.-M.: On-the-fly verification of linear temporal logic. In: Wing, J.M., Woodcock, J., Davies, J. (eds.) FM 1999. LNCS, vol. 1708, pp. 253\u2013271. Springer, Heidelberg (1999). \n https:\/\/doi.org\/10.1007\/3-540-48119-2_16"},{"issue":"3","key":"2_CR5","doi-asserted-by":"publisher","first-page":"219","DOI":"10.1007\/s10703-016-0259-2","volume":"49","author":"J Esparza","year":"2016","unstructured":"Esparza, J., K\u0159et\u00ednsk\u00fd, J., Sickert, S.: From LTL to deterministic automata: a safraless compositional approach. Form. Methods Syst. Des. 49(3), 219\u2013271 (2016). \n https:\/\/doi.org\/10.1007\/s10703-016-0259-2","journal-title":"Form. Methods Syst. Des."},{"issue":"2","key":"2_CR6","doi-asserted-by":"publisher","first-page":"101","DOI":"10.1023\/b:form.0000017718.28096.48","volume":"24","author":"B Finkbeiner","year":"2004","unstructured":"Finkbeiner, B., Sipma, H.: Checking finite traces using alternating automata. Form. Methods Syst. Des. 24(2), 101\u2013127 (2004). \n https:\/\/doi.org\/10.1023\/b:form.0000017718.28096.48","journal-title":"Form. Methods Syst. Des."},{"key":"2_CR7","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. 2102, pp. 53\u201365. Springer, Heidelberg (2001). \n https:\/\/doi.org\/10.1007\/3-540-44585-4_6"},{"issue":"1","key":"2_CR8","doi-asserted-by":"publisher","first-page":"60","DOI":"10.1016\/j.tcs.2005.07.004","volume":"345","author":"J Geldenhuys","year":"2005","unstructured":"Geldenhuys, J., Valmari, A.: More efficient on-the-fly LTL verification with Tarjan\u2019s algorithm. Theor. Comput. Sci. 345(1), 60\u201382 (2005). \n https:\/\/doi.org\/10.1016\/j.tcs.2005.07.004","journal-title":"Theor. Comput. Sci."},{"key":"2_CR9","series-title":"IFIP Advances in Information and Communication Technology","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/978-0-387-34892-6_1","volume-title":"Protocol Specification Testing and Verification XV","author":"R Gerth","year":"1996","unstructured":"Gerth, R., Peled, D., Vardi, M.Y., Wolper, P.: Simple on-the-fly automatic verification of linear temporal logic. In: Dembinski, P., Sredniawa, M. (eds.) PSTV 1995. IFIPAICT, pp. 3\u201318. Springer, Boston (1996). \n https:\/\/doi.org\/10.1007\/978-0-387-34892-6_1"},{"key":"2_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"521","DOI":"10.1007\/3-540-44929-9_36","volume-title":"Theoretical Computer Science: Exploring New Frontiers of Theoretical Informatics","author":"C Loding","year":"2000","unstructured":"Loding, C., Thomas, W.: Alternating automata and logics over infinite words. In: van Leeuwen, J., Watanabe, O., Hagiya, M., Mosses, P.D., Ito, T. (eds.) TCS 2000. LNCS, vol. 1872, pp. 521\u2013535. Springer, Heidelberg (2000). \n https:\/\/doi.org\/10.1007\/3-540-44929-9_36"},{"key":"2_CR11","doi-asserted-by":"publisher","unstructured":"Muller, D.E., Saoudi, A., Schupp, P.E.: Weak alternating automata give a simple explanation of why most temporal and dynamic logics are decidable in exponential time. In: Proceedings of 3rd Annual Symposium on Logic in Computer Science, LICS 1999, Edinburgh, July 1988, pp. 422\u2013427. IEEE CS Press (1988). \n https:\/\/doi.org\/10.1109\/lics.1988.5139","DOI":"10.1109\/lics.1988.5139"},{"key":"2_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"238","DOI":"10.1007\/11605157_20","volume-title":"Implementation and Application of Automata","author":"R Pel\u00e1nek","year":"2006","unstructured":"Pel\u00e1nek, R., Strej\u010dek, J.: Deeper connections between LTL and alternating automata. In: Farr\u00e9, J., Litovsky, I., Schmitz, S. (eds.) CIAA 2005. LNCS, vol. 3845, pp. 238\u2013249. Springer, Heidelberg (2006). \n https:\/\/doi.org\/10.1007\/11605157_20"},{"key":"2_CR13","doi-asserted-by":"publisher","unstructured":"Pnueli, A.: The temporal logic of programs. In: Proceedings of 18th Annual Symposium on Foundations of Computer Science, FOCS 1977, Providence, RI, October\u2013November 1977, pp. 46\u201357. IEEE CS Press (1977). \n https:\/\/doi.org\/10.1109\/sfcs.1977.32","DOI":"10.1109\/sfcs.1977.32"},{"key":"2_CR14","doi-asserted-by":"publisher","first-page":"287","DOI":"10.4204\/EPTCS.226.20","volume":"226","author":"Mark Reynolds","year":"2016","unstructured":"Reynolds, M.: A new rule for LTL tableaux. In: Cantone, D., Delzanno, G. (eds.) Proceedings of 7th International Symposium on Games, Automata, Logics and Formal Verification, GandALF 2016 (Catania, September 2016). Electronic Proceedings in Theoretical Computer Science, vol. 226, pp. 287\u2013301. Open Public Association, Sydney (2016). \n https:\/\/doi.org\/10.4204\/eptcs.226.20","journal-title":"Electronic Proceedings in Theoretical Computer Science"},{"key":"2_CR15","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"277","DOI":"10.1007\/3-540-69778-0_28","volume-title":"Automated Reasoning with Analytic Tableaux and Related Methods","author":"S Schwendimann","year":"1998","unstructured":"Schwendimann, S.: A new one-pass tableau calculus for PLTL. In: de Swart, H. (ed.) TABLEAUX 1998. LNCS (LNAI), vol. 1397, pp. 277\u2013291. Springer, Heidelberg (1998). \n https:\/\/doi.org\/10.1007\/3-540-69778-0_28"},{"key":"2_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"287","DOI":"10.1007\/978-3-319-15579-1_22","volume-title":"Language and Automata Theory and Applications","author":"P Thiemann","year":"2015","unstructured":"Thiemann, P., Sulzmann, M.: From \n \n \n \n $$\\omega $$\n \n \n \u03c9\n \n \n -regular expressions to B\u00fcchi automata via partial derivatives. In: Dediu, A.-H., Formenti, E., Mart\u00edn-Vide, C., Truthe, B. (eds.) LATA 2015. LNCS, vol. 8977, pp. 287\u2013298. Springer, Cham (2015). \n https:\/\/doi.org\/10.1007\/978-3-319-15579-1_22"},{"key":"2_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"575","DOI":"10.1007\/3-540-57887-0_116","volume-title":"Theoretical Aspects of Computer Software","author":"MY Vardi","year":"1994","unstructured":"Vardi, M.Y.: Nontraditional applications of automata theory. In: Hagiya, M., Mitchell, J.C. (eds.) TACS 1994. LNCS, vol. 789, pp. 575\u2013597. Springer, Heidelberg (1994). \n https:\/\/doi.org\/10.1007\/3-540-57887-0_116"},{"key":"2_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"191","DOI":"10.1007\/3-540-63104-6_19","volume-title":"Automated Deduction\u2014CADE-14","author":"MY Vardi","year":"1997","unstructured":"Vardi, M.Y.: Alternating automata: unifying truth and validity checking for temporal logics. In: McCune, W. (ed.) CADE 1997. LNCS, vol. 1249, pp. 191\u2013206. Springer, Heidelberg (1997). \n https:\/\/doi.org\/10.1007\/3-540-63104-6_19"},{"key":"2_CR19","unstructured":"Vardi, M.Y., Wolper, P.: An automata-theoretic approach to automatic program verification (preliminary report). In: Proceedings of 1st Symposium on Logic in Computer Science, LICS 1986, Cambridge, MA, June 1986, pp. 332\u2013344. IEEE CS Press (1986)"},{"issue":"1","key":"2_CR20","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1006\/inco.1994.1092","volume":"115","author":"MY Vardi","year":"1994","unstructured":"Vardi, M.Y., Wolper, P.: Reasoning about infinite computations. Inf. Comput. 115(1), 1\u201337 (1994). \n https:\/\/doi.org\/10.1006\/inco.1994.1092","journal-title":"Inf. Comput."},{"issue":"1\/2","key":"2_CR21","doi-asserted-by":"publisher","first-page":"72","DOI":"10.1016\/s0019-9958(83)80051-5","volume":"56","author":"P Wolper","year":"1983","unstructured":"Wolper, P.: Temporal logic can be more expressive. Inf. Control 56(1\/2), 72\u201399 (1983). \n https:\/\/doi.org\/10.1016\/s0019-9958(83)80051-5","journal-title":"Inf. Control"},{"issue":"110\u2013111","key":"2_CR22","first-page":"119","volume":"28","author":"P Wolper","year":"1985","unstructured":"Wolper, P.: The tableau method for temporal logic: an overview. Log. Anal. 28(110\u2013111), 119\u2013136 (1985). \n https:\/\/www.jstor.org\/stable\/44084125","journal-title":"Log. Anal."},{"key":"2_CR23","doi-asserted-by":"publisher","unstructured":"Wolper, P., Vardi, M.Y., Sistla, A.P.: Reasoning about infinite computation paths (extended abstract). In: Proceedings of 24th Annual Symposium on Foundations of Computer Science, FOCS 1983, Tucson, AZ, November 1983, pp. 185\u2013194. IEEE CS Press (1983). \n https:\/\/doi.org\/10.1109\/sfcs.1983.51","DOI":"10.1109\/sfcs.1983.51"}],"container-title":["Lecture Notes in Computer Science","Theoretical Aspects of Computing \u2013 ICTAC 2018"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-02508-3_2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,3,3]],"date-time":"2020-03-03T07:49:36Z","timestamp":1583221776000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-02508-3_2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018]]},"ISBN":["9783030025076","9783030025083"],"references-count":23,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-02508-3_2","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2018]]},"assertion":[{"value":"15 October 2018","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"ICTAC","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Colloquium on Theoretical Aspects of Computing","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Stellenbosch","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"South Africa","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2018","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"16 October 2018","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"19 October 2018","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"15","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"ictac2018","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.ictac.org.za\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}