Safety for bisimulation in monadic second-order logic

Abstract

We characterize those formulas of MSO m(monadic second-order logic) that are safe for bisimulation: formulas defining binary relations such that any bisimulation is also a bisimulation with respect to these defined relations. Every such formula is equivalent to one constructed from μ-calculus tests, atomic actions and the regular operations. The proof uses a characterization of completely additive μ-calculus formulas: formulas ø(p) that distribute over arbitrary unions. It turns out that complete additivity is equivalent to distributivity over countable unions. For FOL (first-order logic) a similar theorem is shown (giving an alternative proof to the original of [4]). Here though distributivity over finite unions is sufficient. This enables us to show that the characterization of safe FOL-formulas carries over to the setting of finite models.