MSO = 正则语言（逻辑与自动机之桥）
正则语言恰好就是那些能够用一种逻辑描述出来的语言——这是所有巧合中最深刻的一个，也是模型检测（model checking）的基础。
一元二阶逻辑（MSO）这个阶梯的划分标准是你被允许对什么量化：
- 一阶逻辑（FOL）——对元素量化（
∀x, ∃x）；- 二阶逻辑（SO）——对任意元数的关系量化（
∀R、∀f）——非常强，一般不可判定；- MSO——将二阶逻辑限制到一元关系，也就是集合：对子集做
∀X, ∃X，配合成员关系x ∈ X。所以MSO = 一阶逻辑 + 对集合的量化，严格介于一阶逻辑和完整二阶逻辑之间。在字符串、树，以及
⟨ℕ,<⟩上它仍然可判定（可转译为自动机）——这一点与完整二阶逻辑不同——而在无限二叉树上，它就是 Rabin 的 S2S。
将其实例化到字符串上：
字符串上的 MSO把一个字符串看作一个结构：位置
1…n、顺序关系<，以及谓词Qₐ(x)= "位置x上的字母是a"。一元二阶逻辑（MSO）在一阶逻辑的基础上，加入了对位置集合的量化（∃X. …）。
Büchi–Elgot–Trakhtenbrot 定理（1960）一个语言是正则的，当且仅当它是 MSO 可定义的。
为什么（简述）。 一个 k 状态自动机的一次运行，就是把各个位置按状态染色；"存在一次接受的运行"就等价于"存在若干集合 X₁…Xₖ（把位置 i 放进它在该次运行中所处状态 q 对应的那个集合里），满足局部的转移约束，并且以接受状态结束。"这正是一句 MSO 语句（集合量化词承担了全部工作）。反过来，MSO 的每一个连接词/量化词，都对应着一种自动机操作（并、积、投影、补），由此可以从任意公式构造出一个自动机。
为什么重要
这就是逻辑 ↔ 自动机的对应关系：一份规格说明（公式）可以被编译成一台机器（自动机）并加以检验。将其推广到无限长的词上，就得到了 Büchi 自动机与时序逻辑（LTL）——这正是模型检测背后的理论。与 Curry–Howard 的"证明=程序"是同一个主题：在这里，规格说明 = 机器。