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. © 2006 Elsevier B.V. All rights reserved.
Proceedings title: Proceedings of the Second Workshop on Structural Operational Semantics (SOS 2005)