Buchi's Theorem

A language is definable in second-order monadic logic if and only if it is regular.

Proof

Regular → Second-order monadic

Let L be a regular language with associated DFA D = (Q, q1, δ, F). We construct a formula Φ describing an accepting run of D on a string (Φ is true iff there is an accepting run of D on the string).

Let Q = {q1, q2,..., qn).

Φ can be described as: ∃C1∃C2...∃Cn: ∀x: ( should be in some state) ∧ ( can be in only 1 state) ∧ (zero(x) → start at q1) ∧ ( follow the right transitions) ∧ (last(x) → end at a final state)

  • should be in some state: [C1(x) ∨ C2(x) ∨ ... ∨ Cn(x)]
  • can be in only 1 state: for every pair of states qi, qj, add the following: [Ci(x) → Cj(x)]. Connect these together with ∧.
  • start at q1: C1(x)
  • follow the right transitions: for every transition δ(qi, a) = qj, add the following: [(Ci(x) ∧ Ia(x)) → Cj(x+1)]. Connect these together with ∧.
  • end at a final state: for every transition δ(qi, a) = qj such that qj∈F, add the following: [Ia(x) ∧ Ci(x)]. Connect these together with ∨.
zero(x) - x is the beginning of the string, (x+1), and last(x) - x is the end of the string, can be easily described in first-order logic.

Second-order monadic Regular

If we have a formula with variables x, y, A, B, we can mark a string w with them. Each x and y can mark 1 position in w. A and B can mark sets of positions.

Let string w satisfy formula Φ with free variables x, y, A, B.

Assume a DFA MΦ decides (w, x, y, A, B) satisfies Φ.

  • Build an NFA M'Φ that decides (w, y, A, B) satisfies ∃x:Φ. Non-deteministically guess which position is marked by x. Then run MΦ on the input with guessed x.
  • Build an NFA M'Φ that decides (w, x, y, B) satisfies ∃A:Φ. For each position non-deterministically guess if it is marked by A. Then run MΦ on the input with guessed A's.
  • Build a DFA M'Φ that decides (w, y, A, B) satisfies ∀x:Φ. Check each possible marking with x using MΦ.
  • Build a DFA M'Φ that decides (w, x, y, B) satisfies ∀A:Φ. Check each possible marking with A's using MΦ.
Base case: Booleans, (x ≤ y), Ia(x), A(x) are all regular.

-- SvorotnI - 2012-04-22


This topic: H401 > WebHome > DescriptiveComplexity > BuchiSTheorem
Topic revision: r3 - 2012-04-23 - SvorotnI
 
This site is powered by the TWiki collaboration platform Powered by PerlCopyright © 2008-2019 by the contributing authors. All material on this collaboration platform is the property of the contributing authors.
Ideas, requests, problems regarding UMass CS EdLab? Send feedback

mersin escort adana escort izmir escort gaziantep escort