Divide and congruence II

AbstractEarlier we presented a method to decompose modal formulas for processes with the internal action , and congruence formats for branching and -bisimilarity were derived on the basis of this decomposition method. The idea is that a congruence format for a semantics must ensure that the formulas in the modal characterisation of this semantics are always decomposed into formulas that are again in this modal characterisation. In this follow-up paper the decomposition method is enhanced to deal with modal characterisations that contain a modality a, to derive congruence formats for delay and weak bisimilarity.