ABSTRACT
This paper investigates the symbolic semantics of the weak open congruence on finite π processes with the mismatch operator. The standard definition of weak open congruence gives rise to an ill-defined equivalence in the presence of the mismatch operator. Two alternatives, that is, the symbolic weak late open congruence and symbolic weak early open congruence are proposed. We show that they coincide with the non-symbolic version late and early open congruence respectively. Axiomatization systems for the two weak open congruences are given, which are essentially the symbolic proof system for strong open congruence with the different tau laws. The soundness and completeness of these proof systems are shown. The results can be seen as the basis of automated algorithms and tools to check the weak open bisimulation and give more insights into the symbolic semantics and bisimilation theory.
