On the decidability and complexity of the structural congruence for beta-binders

Beta-binders is a recent process calculus developed for modelling and simulating biological systems. As usual for process calculi, the semantic definition heavily relies on a structural congruence. The treatment of the structural congruence is essential for implementation. We present a subset of the calculus for which the structural congruence is decidable and a subset for which it is also efficiently solvable. The obtained results are a first step towards implementations.