A Formal Approach to Identify Structural Patterns in RNA

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–structure 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–structure patterns over RNA secondary structures, including pseudoknots. We present a model-checking algorithm for LiRNA that reduces sequence–structure 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.