Finding a Forest in a Tree: the matching problem for wide reactive systems

Wide reactive systems are rewriting systems specified by wide reaction rules, where redex and reactum are lists of terms (forests), i.e. rules of the form ⟨l1(x1),…,ln(xn)⟩⇒⟨r1(y1),…,rn(yn)⟩ such that ∪iyi⊆∪ixi. Wide reaction rules are particularly useful for process calculi for mobile and global computations, because they allow one to connect processes which can be at different places in the system, possibly crossing boundaries and firewalls. For instances, remote procedure calls can be modeled as a process in place i activating a reaction in a different place j; code mobility can be modeled by instantiating variables in yi with terms using variables from xj, for a different j; etc.
In order to apply a wide reaction rule, we have to find a matching of the rule redex within the global state. This problem can be restated as follows: how to match a given forest (the redex) inside an unordered tree (the system), possibly finding the subtrees to be grafted at the forest’s leaves (i.e., instantiating the variables)? We show that, although the problem is NP-complete in general, the exponential explosion depends only on the number n of roots of the forest (the width of the redex), and not on the size of the global tree (the system state). In most practical cases, the width is constant and small (i.e., ≤3), hence our results show that the wide reaction systems can be actually used for process calculi.