Extending Visibly Pushdown Automata over Multi-matching Nested Relations

Visibly Pushdown Automata (VPAs) are a subclass of pushdown automata, which can be well applied as specification formalism for verification and the model for XML streams process. The input alphabet is partitioned into three disjoint sets: call, internal and return symbols, which can determine a push, pop or no stack operation taken by VPAs respectively. Hence, the matchings of push (call) and pop (return) make languages with matching nested relations accepted. Nevertheless, it is limited to one-to-one matching. In this paper, we extend the model of VPAs over multi-matching nested relations. By a subdivision for call and return symbols, inner-calls and inner-returns are obatined to discriminate a one-to-n or n-to-one matching relation. Then, Multi-matching Visibly Pushdown Automata (MVPA) are formally defined whose stack behavior is achieved by setting a guard in the stack, which can guarantee whether a one-to-n or n-to-one matching nested relation is read without confusion. Each nondeterministic multi-matching visibly pushdown automaton is demonstrated to be transformed into a deterministic one. Moreover, the symbolic version of multi-matching visibly pushdown automata is proposed when the input alphabet is given by a Boolean algebra where there is an infinite domain.