A Logical Viewpoint on Process-algebraic Quotients

Let ∼ be a process equivalence. A formula φ is preserved by ∼-quotients iff for every process s of a transition system script T sign we have that if s satisfies φ, then also [s] satisfies φ, where [s] is the equivalence class of s in the quotient of script T sign under ∼. We classify all formulae of Hennessy-Milner logic which are preserved by ∼-quotients of image-finite processes. Our result is generic in the sense that it works for a large class of process equivalences which admit a modal characterization in Hennessy-Milner logic satisfying certain closure properties. Practical applicability of the result is demonstrated on equivalences of the linear/branching time spectrum.