Bisimulation Invariant Monadic-Second Order Logic in the Finite

TL;DR

This paper investigates when bisimulation-invariant monadic second-order logic over finite transition systems has the same expressive power as the modal mu-calculus, providing combinatorial characterizations and specific cases where they coincide.

Contribution

It offers new combinatorial characterizations for the equivalence of bisimulation-invariant MSO and the modal mu-calculus over finite transition systems.

Findings

Over finite systems with Cantor-Bendixson rank at most k, bisimulation-invariant MSO equals L_mu.

Provides conditions under which MSO and mu-calculus are expressively equivalent.

Establishes the relationship between system complexity and logical expressiveness.

Abstract

We consider bisimulation-invariant monadic second-order logic over various classes of finite transition systems. We present several combinatorial characterisations of when the expressive power of this fragment coincides with that of the modal mu-calculus. Using these characterisations we prove for some simple classes of transition systems that this is indeed the case. In particular, we show that, over the class of all finite transition systems with Cantor-Bendixson rank at most k, bisimulation-invariant MSO coincides with L_mu.

Figures