{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,27]],"date-time":"2026-05-27T17:21:48Z","timestamp":1779902508903,"version":"3.53.1"},"publisher-location":"Cham","reference-count":32,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783032014351","type":"print"},{"value":"9783032014368","type":"electronic"}],"license":[{"start":{"date-parts":[[2025,8,19]],"date-time":"2025-08-19T00:00:00Z","timestamp":1755561600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2025,8,19]],"date-time":"2025-08-19T00:00:00Z","timestamp":1755561600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2026]]},"abstract":"<jats:title>Abstract<\/jats:title>\n                  <jats:p>RNA molecules fold into complex structures that are crucial to their biological function. Secondary structure is an RNA abstraction with biological relevance and computational tractability. Structural motifs within these configurations are essential for understanding and classifying RNA functionality and are often implicated in disease mechanisms. Existing pattern-matching approaches can identify sequence motifs, structural motifs, and sequence\u2013structure motifs. However, they often lack the expressiveness needed to capture complex patterns, particularly pseudoknots. This paper introduces Linear RNA Diagram Logic (LiRNA), a novel logic inspired by classical temporal logics. We show that LiRNA is expressive enough to specify sequence, structural, and sequence\u2013structure patterns over RNA secondary structures, including pseudoknots. We present a model-checking algorithm for LiRNA that reduces sequence\u2013structure pattern matching to the satisfaction of logical formulas. The algorithm is proven correct, and its worst-case complexity is shown to be proportional to the product of the formula size and the input structure length raised to the power of one plus the number of existential quantifiers in the formula.<\/jats:p>","DOI":"10.1007\/978-3-032-01436-8_11","type":"book-chapter","created":{"date-parts":[[2025,8,18]],"date-time":"2025-08-18T03:25:12Z","timestamp":1755487512000},"page":"195-217","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["A Formal Approach to\u00a0Identify Structural Patterns in\u00a0RNA"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-3061-863X","authenticated-orcid":false,"given":"Michele","family":"Loreti","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0539-0290","authenticated-orcid":false,"given":"Michela","family":"Quadrini","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0008-2639-1683","authenticated-orcid":false,"given":"Matteo","family":"Scoccia","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-7536-8796","authenticated-orcid":false,"given":"Luca","family":"Tesei","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2025,8,19]]},"reference":[{"key":"11_CR1","series-title":"Lecture Notes in Business Information Processing","doi-asserted-by":"publisher","first-page":"169","DOI":"10.1007\/978-3-642-28108-2_19","volume-title":"Business Process Management Workshops","author":"W van der Aalst","year":"2012","unstructured":"van der Aalst, W., et al.: Process mining manifesto. In: Daniel, F., Barkaoui, K., Dustdar, S. (eds.) BPM 2011. LNBIP, vol. 99, pp. 169\u2013194. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-28108-2_19"},{"issue":"5","key":"11_CR2","doi-asserted-by":"publisher","first-page":"531","DOI":"10.1093\/logcom\/4.5.531","volume":"4","author":"JF Allen","year":"1994","unstructured":"Allen, J.F., Ferguson, G.: Actions and events in interval temporal logic. J. Log. Comput. 4(5), 531\u2013579 (1994). https:\/\/doi.org\/10.1093\/logcom\/4.5.531","journal-title":"J. Log. Comput."},{"key":"11_CR3","volume-title":"Principles of Model Checking","author":"C Baier","year":"2008","unstructured":"Baier, C., Katoen, J.P.: Principles of Model Checking. MIT Press, Cambridge, MA, USA (2008)"},{"key":"11_CR4","doi-asserted-by":"publisher","first-page":"59","DOI":"10.1016\/j.tcs.2015.05.016","volume":"592","author":"R Beal","year":"2015","unstructured":"Beal, R., Adjeroh, D.: Efficient pattern matching for RNA secondary structures. Theoret. Comput. Sci. 592, 59\u201371 (2015). https:\/\/doi.org\/10.1016\/j.tcs.2015.05.016","journal-title":"Theoret. Comput. Sci."},{"issue":"1","key":"11_CR5","doi-asserted-by":"publisher","first-page":"235","DOI":"10.1093\/nar\/28.1.235","volume":"28","author":"H Berman","year":"2000","unstructured":"Berman, H., et al.: The protein data bank. Nucleic Acids Res. 28(1), 235\u2013242 (2000). https:\/\/doi.org\/10.1093\/nar\/28.1.235","journal-title":"Nucleic Acids Res."},{"issue":"4","key":"11_CR6","doi-asserted-by":"publisher","first-page":"900","DOI":"10.1016\/j.jmb.2008.04.033","volume":"379","author":"M Bon","year":"2008","unstructured":"Bon, M., Vernizzi, G., Orland, H., Zee, A.: Topological classification of RNA structures. J. Mol. Biol. 379(4), 900\u2013911 (2008). https:\/\/doi.org\/10.1016\/j.jmb.2008.04.033","journal-title":"J. Mol. Biol."},{"key":"11_CR7","doi-asserted-by":"publisher","unstructured":"Bormann, J., Lohse, J., Payer, M., Venzl, G.: Model checking in industrial hardware design. In: Proceedings of the 32nd Annual ACM\/IEEE Design Automation Conference, pp. 298\u2013303 (1995). https:\/\/doi.org\/10.1145\/217474.217545","DOI":"10.1145\/217474.217545"},{"key":"11_CR8","doi-asserted-by":"publisher","first-page":"598","DOI":"10.1038\/nrmicro1704","volume":"5","author":"I Brierley","year":"2007","unstructured":"Brierley, I., Pennell, S., Gilbert, R.J.C.: Viral RNA pseudoknots: versatile motifs in gene expression and replication. Nat. Rev. Microbiol. 5, 598\u2013610 (2007). https:\/\/doi.org\/10.1038\/nrmicro1704","journal-title":"Nat. Rev. Microbiol."},{"issue":"15","key":"11_CR9","doi-asserted-by":"publisher","first-page":"1974","DOI":"10.1093\/bioinformatics\/btp250","volume":"25","author":"K Darty","year":"2009","unstructured":"Darty, K., Denise, A., Ponty, Y.: VARNA: interactive drawing and editing of the RNA secondary structure. Bioinformatics 25(15), 1974\u20131975 (2009). https:\/\/doi.org\/10.1093\/bioinformatics\/btp250","journal-title":"Bioinformatics"},{"key":"11_CR10","doi-asserted-by":"publisher","unstructured":"De\u00a0Giacomo, G., Felli, P., Montali, M., Perelli, G.: Hyperldl_f: a logic for checking properties of finite traces in process logs. In: Proceedings of the 30th International Joint Conference on Artificial Intelligence (IJCAI 2021), pp. 1859\u20131865 (2021). https:\/\/doi.org\/10.24963\/ijcai.2021\/256","DOI":"10.24963\/ijcai.2021\/256"},{"key":"11_CR11","unstructured":"Evans, P.A.: Algorithms and complexity for annotated sequence analysis, Ph.D. thesis, University of Victoria (1999)"},{"issue":"4","key":"11_CR12","doi-asserted-by":"publisher","first-page":"935","DOI":"10.1145\/115234.115351","volume":"38","author":"JY Halpern","year":"1991","unstructured":"Halpern, J.Y., Shoham, Y.: A propositional modal logic of time intervals. J. ACM 38(4), 935\u2013962 (1991). https:\/\/doi.org\/10.1145\/115234.115351","journal-title":"J. ACM"},{"key":"11_CR13","doi-asserted-by":"publisher","first-page":"57","DOI":"10.1016\/j.mbs.2015.10.004","volume":"270","author":"FW Huang","year":"2015","unstructured":"Huang, F.W., Reidys, C.M.: Shapes of topological RNA structures. Math. Biosci. 270, 57\u201365 (2015). https:\/\/doi.org\/10.1016\/j.mbs.2015.10.004","journal-title":"Math. Biosci."},{"issue":"4","key":"11_CR14","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/1592434.1592438","volume":"41","author":"R Jhala","year":"2009","unstructured":"Jhala, R., Majumdar, R.: Software model checking. ACM Comput. Surv. 41(4), 1\u201354 (2009). https:\/\/doi.org\/10.1145\/1592434.1592438","journal-title":"ACM Comput. Surv."},{"key":"11_CR15","doi-asserted-by":"publisher","first-page":"1354","DOI":"10.1038\/nm.3981","volume":"9","author":"MC Jiang","year":"2019","unstructured":"Jiang, M.C., Ni, J.J., Cui, W.Y., Wang, B.Y., Zhuo, W.: Emerging roles of lncRNA in cancer and therapeutic opportunities. Am. J. Cancer Res. 9, 1354\u20131366 (2019). https:\/\/doi.org\/10.1038\/nm.3981","journal-title":"Am. J. Cancer Res."},{"key":"11_CR16","doi-asserted-by":"publisher","first-page":"574485","DOI":"10.3389\/fgene.2020.574485","volume":"11","author":"B Li","year":"2020","unstructured":"Li, B., Cao, Y., Westhof, E., Miao, Z.: Advances in RNA 3D structure modeling using experimental data. Front. Genet. 11, 574485 (2020). https:\/\/doi.org\/10.3389\/fgene.2020.574485","journal-title":"Front. Genet."},{"key":"11_CR17","doi-asserted-by":"publisher","first-page":"51","DOI":"10.1007\/s00285-007-0109-3","volume":"56","author":"ME Lladser","year":"2008","unstructured":"Lladser, M.E., Betterton, M.D., Knight, R.: Multiple pattern matching: a Markov chain approach. J. Math. Biol. 56, 51\u201392 (2008). https:\/\/doi.org\/10.1007\/s00285-007-0109-3","journal-title":"J. Math. Biol."},{"key":"11_CR18","volume-title":"Molecular Cell Biology","author":"H Lodish","year":"2000","unstructured":"Lodish, H., Berk, A., Zipursky, S.L., Matsudaira, P., Baltimore, D., Darnell, J.: Molecular Cell Biology, 4th edn. W. H. Freeman and Company, New York, NY (2000)","edition":"4"},{"issue":"14","key":"11_CR19","doi-asserted-by":"publisher","first-page":"6917","DOI":"10.1080\/07391102.2022.2116110","volume":"41","author":"MAG Matarrese","year":"2023","unstructured":"Matarrese, M.A.G., Loppini, A., Nicoletti, M., Filippi, S., Chiodo, L.: Assessment of tools for RNA secondary structure prediction and extraction: a final-user perspective. J. Biomol. Struct. Dyn. 41(14), 6917\u20136936 (2023). https:\/\/doi.org\/10.1080\/07391102.2022.2116110","journal-title":"J. Biomol. Struct. Dyn."},{"issue":"1","key":"11_CR20","doi-asserted-by":"publisher","first-page":"29","DOI":"10.1016\/j.tcs.2004.12.015","volume":"335","author":"G Mauri","year":"2005","unstructured":"Mauri, G., Pavesi, G.: Algorithms for pattern matching and discovery in RNA secondary structure. Theoret. Comput. Sci. 335(1), 29\u201351 (2005). https:\/\/doi.org\/10.1016\/j.tcs.2004.12.015","journal-title":"Theoret. Comput. Sci."},{"issue":"1","key":"11_CR21","doi-asserted-by":"publisher","first-page":"214","DOI":"10.1186\/1471-2105-12-214","volume":"12","author":"F Meyer","year":"2011","unstructured":"Meyer, F., Kurtz, S., Backofen, R., Will, S., Beckstette, M.: Structator: fast index-based search for RNA sequence-structure patterns. BMC Bioinf. 12(1), 214 (2011). https:\/\/doi.org\/10.1186\/1471-2105-12-214","journal-title":"BMC Bioinf."},{"key":"11_CR22","unstructured":"Quadrini, M., Merelli, E., Piergallini, R.: Algebraic and topological operators for RNA structures comparison and classification, Ph.D. thesis, University of Camerino (2019)"},{"issue":"4","key":"11_CR23","doi-asserted-by":"publisher","first-page":"161","DOI":"10.1186\/s12859-019-2689-5","volume":"20","author":"M Quadrini","year":"2019","unstructured":"Quadrini, M., Tesei, L., Merelli, E.: An algebraic language for RNA pseudoknots comparison. BMC Bioinf. 20(4), 161 (2019). https:\/\/doi.org\/10.1186\/s12859-019-2689-5","journal-title":"BMC Bioinf."},{"issue":"11","key":"11_CR24","doi-asserted-by":"publisher","first-page":"3578","DOI":"10.1093\/bioinformatics\/btaa147","volume":"36","author":"M Quadrini","year":"2020","unstructured":"Quadrini, M., Tesei, L., Merelli, E.: ASPRAlign: a tool for the alignment of RNA secondary structures with arbitrary pseudoknots. Bioinformatics 36(11), 3578\u20133579 (2020). https:\/\/doi.org\/10.1093\/bioinformatics\/btaa147","journal-title":"Bioinformatics"},{"issue":"Suppl 6","key":"11_CR25","doi-asserted-by":"publisher","first-page":"575","DOI":"10.1186\/s12859-023-05362-5","volume":"23","author":"M Quadrini","year":"2022","unstructured":"Quadrini, M., Tesei, L., Merelli, E.: Automatic generation of pseudoknotted RNAs taxonomy. BMC Bioinf. 23(Suppl 6), 575 (2022). https:\/\/doi.org\/10.1186\/s12859-023-05362-5","journal-title":"BMC Bioinf."},{"key":"11_CR26","unstructured":"RCSB Protein Data Bank: RCSB PDB: the research collaboratory for structural bioinformatics protein data bank (2025). https:\/\/www.rcsb.org\/"},{"issue":"W1","key":"11_CR27","doi-asserted-by":"publisher","first-page":"W507","DOI":"10.1093\/nar\/gkv435","volume":"43","author":"M Retwitzer","year":"2015","unstructured":"Retwitzer, M., Polishchuk, M., Churkin, E., Kifer, I., Yakhini, Z., Barash, D.: RNAPattMatch: a web server for RNA sequence\/structure motif detection based on pattern matching with flexible gaps. Nucleic Acids Res. 43(W1), W507\u2013W512 (2015). https:\/\/doi.org\/10.1093\/nar\/gkv435","journal-title":"Nucleic Acids Res."},{"issue":"6","key":"11_CR28","doi-asserted-by":"publisher","first-page":"e213","DOI":"10.1371\/journal.pbio.0030213","volume":"3","author":"DW Staple","year":"2005","unstructured":"Staple, D.W., Butcher, S.E.: Pseudoknots: RNA structures with diverse functions. PLoS Biol. 3(6), e213 (2005). https:\/\/doi.org\/10.1371\/journal.pbio.0030213","journal-title":"PLoS Biol."},{"issue":"1","key":"11_CR29","doi-asserted-by":"publisher","first-page":"180","DOI":"10.1109\/TCBBIO.2024.3509982","volume":"22","author":"A Tripathi","year":"2025","unstructured":"Tripathi, A., Dhanuka, R., Singh, J.P.: A review of RNA structure prediction: exploring the potential of computational approaches. IEEE Trans. Comput. Biol. Bioinf. 22(1), 180\u2013191 (2025). https:\/\/doi.org\/10.1109\/TCBBIO.2024.3509982","journal-title":"IEEE Trans. Comput. Biol. Bioinf."},{"key":"11_CR30","doi-asserted-by":"publisher","unstructured":"Vardi, M.Y.: An automata-theoretic approach to linear temporal logic. In: Moller, F., Birtwistle, G. (eds.) Logics for Concurrency. LNCS, vol. 1043, pp. 238\u2013266. Springer, Heidelberg (1996). https:\/\/doi.org\/10.1007\/3-540-60915-6_6","DOI":"10.1007\/3-540-60915-6_6"},{"issue":"3\u20134","key":"11_CR31","doi-asserted-by":"publisher","first-page":"257","DOI":"10.1016\/0025-5564(78)90099-8","volume":"42","author":"MS Waterman","year":"1978","unstructured":"Waterman, M.S., Smith, T.F.: RNA secondary structure: a complete mathematical analysis. Math. Biosci. 42(3\u20134), 257\u2013266 (1978). https:\/\/doi.org\/10.1016\/0025-5564(78)90099-8","journal-title":"Math. Biosci."},{"key":"11_CR32","doi-asserted-by":"publisher","first-page":"51","DOI":"10.1016\/j.jacc.2018.08.2161","volume":"248","author":"T Zhou","year":"2016","unstructured":"Zhou, T., Ding, J.W., Wang, X.A., Zheng, X.X.: Long noncoding RNAs and atherosclerosis. Atherosclerosis 248, 51\u201361 (2016). https:\/\/doi.org\/10.1016\/j.jacc.2018.08.2161","journal-title":"Atherosclerosis"}],"updated-by":[{"DOI":"10.1007\/978-3-032-01436-8_22","type":"correction","label":"Correction","source":"publisher","updated":{"date-parts":[[2025,8,19]],"date-time":"2025-08-19T00:00:00Z","timestamp":1755561600000}}],"container-title":["Lecture Notes in Computer Science","Computational Methods in Systems Biology"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-032-01436-8_11","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,5,22]],"date-time":"2026-05-22T13:16:40Z","timestamp":1779455800000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-032-01436-8_11"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,8,19]]},"ISBN":["9783032014351","9783032014368"],"references-count":32,"URL":"https:\/\/doi.org\/10.1007\/978-3-032-01436-8_11","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,8,19]]},"assertion":[{"value":"19 August 2025","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"19 August 2025","order":2,"name":"change_date","label":"Change Date","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"Correction","order":3,"name":"change_type","label":"Change Type","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"A correction has been published.","order":4,"name":"change_details","label":"Change Details","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"The authors declare no conflict of interest.","order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Disclosure of Interests"}},{"value":"CMSB","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Computational Methods in Systems Biology","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Lyon","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"France","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2025","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"10 September 2025","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"12 September 2025","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"23","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cmsb2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/cmsb2025.sciencesconf.org\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}