Divide and Congruence Applied to η-Bisimulation

We present congruence formats for η- and rooted η-bisimulation equivalence. These formats are derived using a method for decomposing modal formulas in process algebra. To decide whether a process algebra term satisfies a modal formula, one can check whether its subterms satisfy formulas that are obtained by decomposing the original formula. The decomposition uses the structural operational semantics that underlies the process algebra.