{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,29]],"date-time":"2025-03-29T16:47:56Z","timestamp":1743266876481,"version":"3.37.3"},"reference-count":35,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2022,4,5]],"date-time":"2022-04-05T00:00:00Z","timestamp":1649116800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2022,4,5]],"date-time":"2022-04-05T00:00:00Z","timestamp":1649116800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Int J Softw Tools Technol Transfer"],"published-print":{"date-parts":[[2022,6]]},"DOI":"10.1007\/s10009-022-00656-0","type":"journal-article","created":{"date-parts":[[2022,4,5]],"date-time":"2022-04-05T07:02:29Z","timestamp":1649142149000},"page":"473-492","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":5,"title":["Temporal-logic query checking over finite data streams"],"prefix":"10.1007","volume":"24","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-7209-550X","authenticated-orcid":false,"given":"Samuel","family":"Huang","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4952-5380","authenticated-orcid":false,"given":"Rance","family":"Cleaveland","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2022,4,5]]},"reference":[{"key":"656_CR1","first-page":"1","volume-title":"Runtime Verification","author":"C Ackermann","year":"2010","unstructured":"Ackermann, C., Cleaveland, R., Huang, S., Ray, A., Shelton, C., Latronico, E.: Automatic requirement extraction from test cases. In: Barringer, H., et al. (eds.) Runtime Verification, pp. 1\u201315. Springer, Berlin, Heidelberg (2010)"},{"key":"656_CR2","unstructured":"Agrawal, R., Srikant, R.: Mining sequential patterns. In: Proceedings of the Eleventh International Conference on Data Engineering. pp. 3\u201314. IEEE Computer Society, Washington, DC, USA (1995)"},{"issue":"8","key":"656_CR3","doi-asserted-by":"publisher","first-page":"677","DOI":"10.1006\/eujc.1996.0059","volume":"17","author":"R Ahlswede","year":"1996","unstructured":"Ahlswede, R., Cai, N.: Incomparability and intersection properties of boolean interval lattices and chain posets. Eur. J. Comb. 17(8), 677\u2013687 (1996). https:\/\/doi.org\/10.1006\/eujc.1996.0059","journal-title":"Eur. J. Comb."},{"issue":"1","key":"656_CR4","doi-asserted-by":"publisher","first-page":"116","DOI":"10.1145\/227595.227602","volume":"43","author":"R Alur","year":"1996","unstructured":"Alur, R., Feder, T., Henzinger, T.A.: The benefits of relaxing punctuality. J. ACM (JACM) 43(1), 116\u2013146 (1996)","journal-title":"J. ACM (JACM)"},{"key":"656_CR5","volume-title":"Principles of Model Checking","author":"C Baier","year":"2008","unstructured":"Baier, C., Katoen, J.P.: Principles of Model Checking. MIT Press, Cambridge (2008)"},{"issue":"1","key":"656_CR6","doi-asserted-by":"publisher","first-page":"115","DOI":"10.1016\/0304-3975(88)90098-9","volume":"59","author":"M Browne","year":"1988","unstructured":"Browne, M., Clarke, E., Grumberg, O.: Characterizing finite Kripke structures in propositional temporal logic. Theoret. Comput. Sci. 59(1), 115\u2013131 (1988). https:\/\/doi.org\/10.1016\/0304-3975(88)90098-9","journal-title":"Theoret. Comput. Sci."},{"key":"656_CR7","doi-asserted-by":"publisher","unstructured":"Bruns, G., Godefroid, P.: Temporal logic query checking. In: Proceedings 16th Annual IEEE Symposium on Logic in Computer Science. pp. 409\u2013417 (2001). https:\/\/doi.org\/10.1109\/LICS.2001.932516","DOI":"10.1109\/LICS.2001.932516"},{"key":"656_CR8","unstructured":"Causality workbench team: PROMO: Simple causal effects in time series (2008), https:\/\/data.world\/data-society\/causal-effects-in-time-series"},{"key":"656_CR9","doi-asserted-by":"publisher","first-page":"450","DOI":"10.1007\/10722167_34","volume-title":"Computer Aided Verification","author":"W Chan","year":"2000","unstructured":"Chan, W.: Temporal-logic queries. In: Emerson, E.A., Sistla, A.P. (eds.) Computer Aided Verification, pp. 450\u2013463. Springer, Berlin, Heidelberg (2000)"},{"key":"656_CR10","doi-asserted-by":"publisher","first-page":"76","DOI":"10.1007\/978-3-642-19583-9_11","volume-title":"Hardware and Software: Verification and Testing","author":"H Chockler","year":"2011","unstructured":"Chockler, H., Gurfinkel, A., Strichman, O.: Variants of LTL query checking. In: Barner, S., Harris, I., Kroening, D., Raz, O. (eds.) Hardware and Software: Verification and Testing, pp. 76\u201392. Springer, Berlin, Heidelberg (2011)"},{"key":"656_CR11","first-page":"52","volume-title":"Logics of Programs","author":"EM Clarke","year":"1981","unstructured":"Clarke, E.M., Emerson, E.A.: Design and synthesis of synchronization skeletons using branching time temporal logic. In: Kozen, D. (ed.) Logics of Programs, pp. 52\u201371. Springer, Berlin, Heidelberg (1981)"},{"key":"656_CR12","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-10575-8","volume-title":"Handbook of Model Checking","author":"EM Clarke","year":"2018","unstructured":"Clarke, E.M., Henzinger, T.A., Veith, H., Bloem, R.: Handbook of Model Checking. Springer, Berlin (2018)"},{"key":"656_CR13","doi-asserted-by":"crossref","unstructured":"De\u00a0Giacomo, G., De\u00a0Masellis, R., Montali, M.: Reasoning on LTL on finite traces: Insensitivity to infiniteness. In: Proceedings of the Twenty-Eighth AAAI Conference on Artificial Intelligence. pp. 1027-1033. AAAI\u201914, AAAI Press, Qu\u00e9bec City, Qu\u00e9bec, Canada (2014)","DOI":"10.1609\/aaai.v28i1.8872"},{"key":"656_CR14","unstructured":"De\u00a0Giacomo, G., Vardi, M.Y.: Linear temporal logic and linear dynamic logic on finite traces. In: Proceedings of the Twenty-Third International Joint Conference on Artificial Intelligence. pp. 854-860. IJCAI \u201913, AAAI Press, Beijing, China (2013)"},{"key":"656_CR15","doi-asserted-by":"publisher","unstructured":"Duret-Lutz, A., Lewkowicz, A., Fauchille, A., Michaud, T., Renault, E., Xu, L.: Spot 2.0: A framework for LTL and $$\\omega $$-automata manipulation. In: Proceedings of the 14th International Symposium on Automated Technology for Verification and Analysis (ATVA\u201916). Lecture Notes in Computer Science, vol.\u00a09938, pp. 122\u2013129. Springer (2016). https:\/\/doi.org\/10.1007\/978-3-319-46520-3_8","DOI":"10.1007\/978-3-319-46520-3_8"},{"key":"656_CR16","doi-asserted-by":"publisher","unstructured":"Eisner, C., Fisman, D.: Functional Specification of Hardware via Temporal Logic, pp. 795\u2013829. Springer International Publishing, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-10575-8_24","DOI":"10.1007\/978-3-319-10575-8_24"},{"key":"656_CR17","doi-asserted-by":"crossref","unstructured":"Fionda, V., Greco, G.: The complexity of LTL on finite traces: Hard and easy fragments. In: Proceedings of the Thirtieth AAAI Conference on Artificial Intelligence. pp. 971\u2013977. AAAI\u201916, AAAI Press, Phoenix, Arizona (2016)","DOI":"10.1609\/aaai.v30i1.10104"},{"issue":"3","key":"656_CR18","doi-asserted-by":"publisher","first-page":"731","DOI":"10.1007\/s10115-014-0817-0","volume":"45","author":"D Fradkin","year":"2015","unstructured":"Fradkin, D., M\u00f6rchen, F.: Mining sequential patterns for classification. Knowl. Inf. Syst. 45(3), 731\u2013749 (2015). https:\/\/doi.org\/10.1007\/s10115-014-0817-0","journal-title":"Knowl. Inf. Syst."},{"key":"656_CR19","doi-asserted-by":"publisher","unstructured":"Georgala, K., Sherif, M.A., Ngomo, A.C.N.: An efficient approach for the generation of Allen relations. In: Proceedings of the Twenty-Second European Conference on Artificial Intelligence. p. 948-956. ECAI\u201916, IOS Press, The Hague, The Netherlands (2016). https:\/\/doi.org\/10.3233\/978-1-61499-672-9-948","DOI":"10.3233\/978-1-61499-672-9-948"},{"issue":"10","key":"656_CR20","doi-asserted-by":"publisher","first-page":"898","DOI":"10.1109\/TSE.2003.1237171","volume":"29","author":"A Gurfinkel","year":"2003","unstructured":"Gurfinkel, A., Chechik, M., Devereux, B.: Temporal logic query checking: A tool for model exploration. IEEE Trans. Software Eng. 29(10), 898\u2013914 (2003). https:\/\/doi.org\/10.1109\/TSE.2003.1237171","journal-title":"IEEE Trans. Software Eng."},{"key":"656_CR21","unstructured":"Holzmann, G.J.: The SPIN model checker: Primer and reference manual, vol.\u00a01003. Addison-Wesley, Reading (2004)"},{"key":"656_CR22","doi-asserted-by":"publisher","unstructured":"Hopcroft, J.: An n log n algorithm for minimizing states in a finite automaton. In: Kohavi, Z., Paz, A. (eds.) Theory of Machines and Computations, pp. 189 \u2013 196. Academic Press (1971). https:\/\/doi.org\/10.1016\/B978-0-12-417750-5.50022-1, http:\/\/www.sciencedirect.com\/science\/article\/pii\/B9780124177505500221","DOI":"10.1016\/B978-0-12-417750-5.50022-1"},{"key":"656_CR23","doi-asserted-by":"publisher","first-page":"34","DOI":"10.1007\/978-3-319-67113-0_3","volume-title":"Critical Systems: Formal Methods and Automated Verification","author":"S Huang","year":"2017","unstructured":"Huang, S., Cleaveland, R.: Query checking for linear temporal logic. In: Petrucci, L., Seceleanu, C., Cavalcanti, A. (eds.) Critical Systems: Formal Methods and Automated Verification, pp. 34\u201348. Springer International Publishing, Cham (2017)"},{"key":"656_CR24","unstructured":"Huang, S., Cleaveland, R.: A tableau construction for finite linear-time temporal logic. arXiv preprint arXiv:1910.09339 (2019), submitted for publication"},{"key":"656_CR25","doi-asserted-by":"crossref","unstructured":"Huang, S., Cleaveland, R.: Temporal-logic query checking over finite data streams. In: International Conference on Formal Methods for Industrial Critical Systems. pp. 252\u2013271. Springer (2020)","DOI":"10.1007\/978-3-030-58298-2_11"},{"issue":"3","key":"656_CR26","doi-asserted-by":"publisher","first-page":"333","DOI":"10.1016\/0304-3975(82)90125-6","volume":"27","author":"D Kozen","year":"1983","unstructured":"Kozen, D.: Results on the propositional $$\\mu $$-calculus. Theoret. Comput. Sci. 27(3), 333\u2013354 (1983)","journal-title":"Theoret. Comput. Sci."},{"key":"656_CR27","doi-asserted-by":"publisher","unstructured":"Kupferman, O.: Automata Theory and Model Checking, pp. 107\u2013151. Springer International Publishing, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-10575-8_4","DOI":"10.1007\/978-3-319-10575-8_4"},{"key":"656_CR28","doi-asserted-by":"publisher","unstructured":"Leucker, M.: Runtime Verification for Linear-Time Temporal Logic, pp. 151\u2013194. Springer International Publishing, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-56841-6_5","DOI":"10.1007\/978-3-319-56841-6_5"},{"key":"656_CR29","doi-asserted-by":"publisher","DOI":"10.7717\/peerj-cs.103","author":"A Meurer","year":"2017","unstructured":"Meurer, A., Smith, C.P., et al.: SymPy: Symbolic computing in Python. PeerJ Comput. Sci. (2017). https:\/\/doi.org\/10.7717\/peerj-cs.103","journal-title":"PeerJ Comput. Sci."},{"key":"656_CR30","doi-asserted-by":"publisher","unstructured":"Pnueli, A.: The temporal logic of programs. In: 18th Annual Symposium on Foundations of Computer Science. pp. 46\u201357 (1977). https:\/\/doi.org\/10.1109\/SFCS.1977.32","DOI":"10.1109\/SFCS.1977.32"},{"key":"656_CR31","doi-asserted-by":"publisher","first-page":"333","DOI":"10.1007\/978-3-319-46982-9_21","volume-title":"Runtime Verification","author":"G Ro\u015fu","year":"2016","unstructured":"Ro\u015fu, G.: Finite-trace linear temporal logic: Coinductive completeness. In: Falcone, Y., S\u00e1nchez, C. (eds.) Runtime Verification, pp. 333\u2013350. Springer International Publishing, Cham (2016)"},{"key":"656_CR32","doi-asserted-by":"crossref","unstructured":"Ro\u015fu, G., Bensalem, S.: Allen linear (interval) temporal logic\u2013translation to LTL and monitor synthesis. In: International Conference on Computer Aided Verification. pp. 263\u2013277. Springer (2006)","DOI":"10.1007\/11817963_25"},{"issue":"3","key":"656_CR33","doi-asserted-by":"publisher","first-page":"733","DOI":"10.1145\/3828.3837","volume":"32","author":"AP Sistla","year":"1985","unstructured":"Sistla, A.P., Clarke, E.M.: The complexity of propositional linear temporal logics. J. ACM (JACM) 32(3), 733\u2013749 (1985)","journal-title":"J. ACM (JACM)"},{"key":"656_CR34","unstructured":"Vardi, M.Y., Wolper, P.: An automata-theoretic approach to automatic program verification. In: Proceedings of the First Symposium on Logic in Computer Science. pp. 322\u2013331. IEEE Computer Society (1986)"},{"issue":"110\u2013111","key":"656_CR35","first-page":"119","volume":"28","author":"P Wolper","year":"1985","unstructured":"Wolper, P.: The tableau method for temporal logic: An overview. Logique et Anal. (N.S.) 28(110\u2013111), 119\u2013136 (1985)","journal-title":"Logique et Anal. (N.S.)"}],"container-title":["International Journal on Software Tools for Technology Transfer"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-022-00656-0.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10009-022-00656-0\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-022-00656-0.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,1,31]],"date-time":"2023-01-31T16:16:57Z","timestamp":1675181817000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10009-022-00656-0"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,4,5]]},"references-count":35,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2022,6]]}},"alternative-id":["656"],"URL":"https:\/\/doi.org\/10.1007\/s10009-022-00656-0","relation":{},"ISSN":["1433-2779","1433-2787"],"issn-type":[{"type":"print","value":"1433-2779"},{"type":"electronic","value":"1433-2787"}],"subject":[],"published":{"date-parts":[[2022,4,5]]},"assertion":[{"value":"8 March 2022","order":1,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"5 April 2022","order":2,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}