Multi-matching nested relations

Multi-matching nested relation consists of a sequence of linearly ordered positions, call, internal, and return, augmented with one-to-one, one-to-n or n-to-one matching nested edges from call to return. For clarity, inner-call and inner-return are defined in n-to-one and one-to-n matching nested relations respectively. After word encoding by introducing tagged letters, Multi-matching Nested Words (MNWs) are obtained over a tagged alphabet. Then Multi-matching Nested Expression (MNE) and Multi-matching Nested Traceable Automaton (MNTA) are defined over MNWs. The closure properties of languages over MNWs are studied, including union, intersection, concatenation, Kleene-* and complementation. Moreover, nondeterministic MNTAs are as expressive as deterministic ones. Further, a transformation method from MNTAs to MNEs is proposed, where three kinds of labeled arcs are created for different transitions in order for the specific merging strategies. To specify the requirements of multi-matching nested calls and returns, we propose a temporal logic of Multi-matching Nested CAlls and RETurns (MNCARET). The abstract and matched-abstract versions of modalities are considered. For example, abstract-next operator allows a path to jump from a call to the first matched non-internal, which is the inner-call, inner-return or return, in a one-to-n or n-to-one matching relation while matched-abstract-next operator from a call directly to the matched return. We also present an approach to model check MNCARET formulas for the MNTA model, a subset of pushdown automata. This problem is reduced to the emptiness problem of Büchi MNTAs.

Authors

• Jin Liu
• Zhenhua Duan Xidian University
• Cong Tian Xidian University

Keywords

• Multi-matching nested relation
• Multi-matching nested traceable automata
• MNCARET formula
• Model checking