An algebraic approach to MSO-definability on countable linear orderings

关系归纳分离逻辑的树宽有界模型的有效MSO可定义性

Effective MSO-Definability for Tree-width Bounded Models of an Inductive Separation Logic of Relations

本文研究关系分离逻辑SLR的MSO可定义性，提出一个可描述有界树宽图集合并能有效翻译为MSO的表达性片段，从而保证可满足性与蕴含问题的可判定性。

Logic and Rational Languages of Scattered and Countable Series-Parallel Posets

Let $A$ be an alphabet and $SP^\diamond(A)$ denote the class of all countable N-free partially ordered sets labeled by $A$, in which chains are scattered linear orderings and antichains are finite. We characterize the rational languages of $SP^\diamond(A)$ by means of logic. We define an extension of monadic second-order logic by Presburger arithmetic, named P-MSO, such that a language $L$ of $SP^\diamond(A)$ is rational if and only if $L$ is the language of a sentence of P-MSO, with effective constructions from one formalism to the other. As a corollary, the P-MSO theory of $SP^\diamond(A)$ i…

Characterizing Weighted MSO for Trees by Branching Transitive Closure Logics

We introduce the branching transitive closure operator on weighted monadic second-order logic formulas where the branching corresponds in a natural way to the branching inherent in trees. For arbitrary commutative semirings, we prove that weighted monadic second order logics on trees is equivalent to the definability by formulas which start with one of the following operators: (i) a branching transitive closure or (ii) an existential second-order quantifier followed by one universal first-order quantifier; in both cases the operator is applied to step-formulas over (a) Boolean first-order logi…

可数链上MSO重参数化的可判定性

Decidability of MSO Reparameterization over Countable Chains

本文研究了如何通过降低表示维度来简化MSO多维点解释，证明在可数标记线性序类上，给定的MSO公式是否允许d维重参数化是可判定的。

Order Invariance on Decomposable Structures

Order-invariant formulas access an ordering on a structure's universe, but the model relation is independent of the used ordering. Order invariance is frequently used for logic-based approaches in computer science. Order-invariant formulas capture unordered problems of complexity classes and they model the independence of the answer to a database query from low-level aspects of databases. We study the expressive power of order-invariant monadic second-order (MSO) and first-order (FO) logic on restricted classes of structures that admit certain forms of tree decompositions (not necessarily of b…

与Parikh和Muller的可判定（计）数：将Presburger算术添加到树可解释结构上的单子二阶逻辑中

Decidable (Ac)counting with Parikh and Muller: Adding Presburger Arithmetic to Monadic Second-Order Logic over Tree-Interpretable Structures

提出$ω$MSO$\Join$BAPA逻辑，通过Parikh-Muller树自动机证明其在树可解释结构上的可满足性可判定，并推广至带高级计数的双变量逻辑与$μ$-演算。