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:

s and s' satisfy same atoms.
If s →ᵃ t, then ∃t'. s' →ᵃ t' and tRt'.
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.

Symbol	Unicode	Name	Meaning
∼	U+223C	Bisimilar	Bisimulation equivalent
≡_ML	—	Modal equiv	Same modal properties
→ᵃ	—	Transition	Labeled transition
R	—	Bisimulation	Relation
□	U+25A1	Box	All successors
◇	U+25C7	Diamond	Some successor

Metatheory. Bisimulation decidable for finite systems. Partition refinement: polynomial algorithm. Modal characterization of bisimulation. Logical characterization of behavioral equivalence. Extends to probabilistic, timed systems.

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

Limitations. Image-finite requirement for HM theorem. Infinite branching: need infinitary logic. Continuous systems: approximate bisimulation. Weak bisimulation more complex.