Monadic Second-Order Logic of Permutations

TL;DR

This paper explores the expressive power and computational complexity of monadic second-order logic applied to permutations, revealing properties expressible in MSO but not in FO, and providing algorithms for model checking.

Contribution

It characterizes the expressive limits of monadic second-order logic on permutations and develops an algorithm for model checking based on tree-width.

Findings

Certain permutation properties are MSO-expressible but not FO-expressible.

Model checking MSO properties can be done efficiently using tree-width.

The problem remains hard on fixed hereditary classes under mild conditions.

Abstract

Permutations can be viewed as pairs of linear orders, or more formally as models over a signature consisting of two binary relation symbols. This approach was adopted by Albert, Bouvel and F\'eray, who studied the expressibility of first-order logic in this setting. We focus our attention on monadic second-order logic. Our results go in two directions. First, we investigate the expressive power of monadic second-order logic. We exhibit natural properties of permutations that can be expressed in monadic second-order logic but not in first-order logic. Additionally, we show that the property of having a fixed point is inexpressible even in monadic second-order logic. Secondly, we focus on the complexity of monadic second-order model checking. We show that there is an algorithm deciding if a permutation $\pi$ satisfies a given monadic second-order sentence $\varphi$ in time $f(|\varphi|, \operatorname{tw}(\pi)) \cdot n$ for some computable function $f$ where $n = |\pi|$ and $\operatorname{tw}(\pi)$ is the tree-width of $\pi$. On the other hand, we prove that the problem remains hard even when we restrict the permutation $\pi$ to a fixed hereditary class $\mathcal{C}$ with mild assumptions on $\mathcal{C}$.