Monadic Second-Order Logic of Permutations
Fuente:
arXiv
Guardado en:
| Autores principales: | , |
|---|---|
| Formato: | Preprint |
| Publicado: |
2025
|
| Materias: | |
| Acceso en línea: | |
| Etiquetas: |
Agregar Etiqueta
Sin Etiquetas, Sea el primero en etiquetar este registro!
|
| _version_ | 1866909886079565824 |
|---|---|
| author | Jelínek, Vít Opler, Michal |
| author_facet | Jelínek, Vít Opler, Michal |
| contents | 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éray, 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 $π$ satisfies a given monadic second-order sentence $φ$ in time $f(|φ|, \operatorname{tw}(π)) \cdot n$ for some computable function $f$ where $n = |π|$ and $\operatorname{tw}(π)$ is the tree-width of $π$. On the other hand, we prove that the problem remains hard even when we restrict the permutation $π$ to a fixed hereditary class $\mathcal{C}$ with mild assumptions on $\mathcal{C}$. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2511_02386 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Monadic Second-Order Logic of Permutations Jelínek, Vít Opler, Michal Combinatorics Logic in Computer Science Logic 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éray, 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 $π$ satisfies a given monadic second-order sentence $φ$ in time $f(|φ|, \operatorname{tw}(π)) \cdot n$ for some computable function $f$ where $n = |π|$ and $\operatorname{tw}(π)$ is the tree-width of $π$. On the other hand, we prove that the problem remains hard even when we restrict the permutation $π$ to a fixed hereditary class $\mathcal{C}$ with mild assumptions on $\mathcal{C}$. |
| title | Monadic Second-Order Logic of Permutations |
| topic | Combinatorics Logic in Computer Science Logic |
| url | https://arxiv.org/abs/2511.02386 |