Bisimulation Modal Logic

Origin. Hennessy and Milner (1980) connected modal logic and bisimulation. Park coined "bisimulation." Modal logic is bisimulation-invariant fragment of FOL (van Benthem). Foundation for process algebra and model theory.

Models. Modal formulas and bisimulation equivalence. Bisimulation: two states are equivalent if they make same observations. Modal logic: cannot distinguish bisimilar states. Hennessy-Milner theorem: modal equivalence = bisimulation (finitely branching).

Formalism.

Bisimulation: Relation R ⊆ S × S' is bisimulation if sRs' implies:

1. s and s' satisfy same atoms.
2. If s →ᵃ t, then ∃t'. s' →ᵃ t' and tRt'.
3. If s' →ᵃ t', then ∃t. s →ᵃ t and tRt'.

Bisimilar states: s ∼ s' iff exists bisimulation R with sRs'.

Modal equivalence: s ≡_ML s' iff for all modal formulas φ: s ⊨ φ ↔ s' ⊨ φ.

Hennessy-Milner theorem: For image-finite systems: s ∼ s' iff s ≡_ML s'. Modal formulas characterize bisimulation.

Van Benthem theorem: Modal logic = bisimulation-invariant fragment of first-order logic. If FOL formula φ(x) is invariant under bisimulation, then φ equivalent to modal formula.

Bisimulation games: Spoiler vs Duplicator game. Spoiler: find distinguishing move. Duplicator: match moves. Bisimilar iff Duplicator has winning strategy.

Largest bisimulation: Union of all bisimulations. Computable for finite systems.

Symbols.

Metatheory. Bisimilarity is the greatest fixed point of the monotone back-and-forth operator on relations, so it exists by Knaster–Tarski and is itself an equivalence relation. Hennessy and Milner (1980) proved that over image-finite transition systems modal equivalence coincides with bisimilarity; the hypothesis can be weakened to modal saturation or ω-saturation, but not dropped. Van Benthem's characterization theorem (1976) is the model-theoretic converse: a first-order formula in one free variable is invariant under bisimulation iff it is equivalent to the standard translation of a modal formula. Rosen (1997) proved the same characterization holds when quantification is restricted to finite models, where the compactness argument is unavailable, and Otto (2004) gave a proof yielding an explicit bound on modal depth. Janin and Walukiewicz (1996) lifted the result one level: the modal μ-calculus is exactly the bisimulation-invariant fragment of monadic second-order logic. Bisimilarity on finite labelled transition systems is computable by partition refinement in O(m log n) time (Paige and Tarjan, 1987) and is P-complete (Balcázar, Gabarró and Sántha, 1992), so it is not parallelizable unless NC = P.

Applies to. Process algebra (CCS, CSP). Model checking. System equivalence. Minimization. Security (observational equivalence). Concurrency theory.

Limitations. Invariance under bisimulation is a hard ceiling on what modal logic can say: irreflexivity, well-foundedness, antisymmetry, the number of successors and the identity of a state are none of them bisimulation-invariant, so none is modally definable, and since every model is bisimilar to its tree unravelling, no modal formula can distinguish a model from a tree. The Hennessy–Milner theorem fails outright without image-finiteness — a state whose branches have every finite length is modally equivalent to one that additionally has an infinite branch, yet the two are not bisimilar — and recovering the correspondence requires infinitary conjunction or a saturation assumption. Bisimilarity is only one point in van Glabbeek's linear-time–branching-time spectrum, strictly finer than trace equivalence and coarser than isomorphism, so its use is a modelling commitment rather than a neutral notion of sameness. Weak bisimilarity, which abstracts from internal actions, is not a congruence for CCS choice and must be replaced by observation congruence. For infinite-state systems decidability breaks down: Jančar (1995) proved bisimilarity undecidable for Petri nets.

© 2026 Lingenic LLC