Automatic Structures: Part 2 -- Buchi-Bruyer Theorem

We now concentrate on the proof of Buchi-Bruyer Theorem, probably the most important theorem concerning automatic structures, which says that the set of regular relations coincides with the set of relations definable in M_univ (defined below). By the way, this theorem is folklore in the sense that its proof is unpublished, but well-known to everybody in the community.

We first need some definitions. Suppose that s := (s₁, ...,s_n) ∈ (Σ*)ⁿ. Then, define a string [s] over the alphabet (Σ∪ {#})ⁿ whose length is max{s₁,...,s_n}, and whose ith symbol is (a₁,...,a_n) where a_j is the ith symbol of s_j, if i ≤ |s_j|, and a_j is #, otherwise. One might visualize [s] as the string obtained by placing s₁,...,s_n in a left-aligned column and pad each string s_i with # so that each of the resulting rows is of equal length. After that, we consider this matrix as a string [s] whose jth position is the jth column of the string. A subset S of (Σ*)ⁿ is said to be regular if the set { [s] : s ∈ S } is regular.

Fix an alphabet of size at least two. Consider the infinite structure M_univ := (Σ*, ≤, (L_a)_{a ∈ Σ}, el) where

1. the universe is the set of all Σ-strings,
   
2. x ≤ y iff x is a prefix of y,
   
3. L_a(x) is true iff the rightmost symbol of x is a, and
   
4. el(x,y) is true iff |x| = |y| (|x| denotes the length of x).
   

What properties are (first-order) definable in M_univ? Here are some simple ones:

1. |x| ≤ |y| (i.e. the string x is no longer than the string y),
   
2. |x| = |y| + k for some fixed constant k,
   
3. im-pref(x,y) (i.e. x = y.a for some letter a ∈ Σ), and
   
4. the kth symbol of x is a (where k is fixed and a ∈ Σ).
   

Apologize for the overloading of the symbol '≤' because of the lack of HTML symbols. For example, the first property above can be expressed as

∃ s( s ≤ y ∧ el(x,s) ).

The second property is also easily expressible, but you might need more quantifiers and make use of the relation im-pref. The third property can be expressed by saying that |x| ≤ |y| and there is no z with x < z < y (here '<' is the irreflexive version of the prefix relation ≤).

Now, a subset S of (Σ*)ⁿ is said to be definable in M_univ if there exists a first-order formula φ(x₁,...,x_n) in the vocabulary of M_univ such that

S = { s : M_univ |= φ(s) }.


Theorem (Buchi-Bruyer): A subset S of (Σ*)ⁿ is definable in M_univ iff S is regular.

Proof sketch:
(<=) Suppose that S is recognized by the automaton A = (Q,q₀,F,δ: Q x Σ -> Q), where Q = {q₀,...,q_l} is a finite set of states, q₀ ∈ Q is the initial state, F ⊆ Q is the set of final states, and δ the transition function. So, for all s ∈ (Σ*)ⁿ, s ∈ S iff the string s₁...s_k = [s] is accepted by A,i.e., there exists a run p₀...p_k such that p₀ = q₀, p_k ∈ F, and δ(p_i,s_i+1) = p_i+1. The defining formula for S is

φ(x₁,...,x_n) = ∃v₀,...,v_l( ψ_len ∧ ψ_char ∧ ψ_start ∧ ψ_end ∧ ψ_trans )

where:

1. ψ_len asserts that |v_i| = max{|x_j| : 1 ≤ j ≤ n} + 1.
   
2. ψ_char asserts that [(v₁,...,v_l)] = w₀...w_k is a characteristic sequence, i.e., each v_i is a string of 0s and 1s, and that, for each position h, exactly one of the strings v_is have value 1. [Intuitively, we want each w_j to represent the state p_j in our accepting run.]
   
3. ψ_start asserts that the first position of v₀ has value 1.
   
4. ψ_end asserts that the last position of some v_j, where q_j ∈ F, has value 1.
   
5. ψ_trans asserts that the transition from w_j to w_j+1 respects δ. [This will be a huge table, quite tedious to write down.]
   

The reader should convince herself that all of the above sentences are definable in M_univ.

(=>) The proof is by induction on the formula φ(x₁,...,x_n) defining S. The base case (i.e. atomic formulas) is very easy (left to the reader). Further, the case where φ is of the form ψ₁ ∨ ψ₂ or ¬ ψ follows immediately from the properties that regular languages are closed under union and complementation. What remains is to prove this for the case where φ is of the form ∃x_n+1 ψ(x₁,...,x_n+1). Suppose that the n+1-ary regular relation R defined by ψ is recognized by the automaton A = (Q,q₀,F,δ). To construct an automaton A' for S, one first applies the pumping lemma to show that: there exists a number K such that if (s₁,...,s_n+1) ∈ R, where |s_n+1| > |s_j| for 1 ≤ j ≤ n, then there exists another string s'_n+1 such that (s₁,...,s'_n+1) ∈ R and |s'_n+1| ≤ max{|s_j| : 1 ≤ j ≤ n} + K. We construct A' as follows. First, make K+1 isomorphic copies of A (with different labels), where the ith copy is denoted by Aⁱ = (Qⁱ = {q₀ⁱ,...,q_lⁱ},q₀ⁱ,Fⁱ,δⁱ). The states of A' are the union of the Qⁱs. The start states consist of all the q₀ⁱs. The final states are the union of the Fⁱs. The transition function δ' works as follows: whenever δⁱ(q_jⁱ,(c₁,...,c_n+1)) = q_hⁱ, where c_m ∈ (Σ &cup {#}), we put δ'(q_jⁱ,(c₁,...,c_n) = q_hⁱ. Note that A' is non-deterministic. It is easy to check that A' recognizes S. (QED)

Automatic Structures: Part 1

Several weeks ago, my supervisor Leonid Libkin gave a presentation about automatic structures in our reading group meeting. I would like to talk about these nice animals in some details. This is the first part in the series of posts giving a flavor of automatic structures and sketching some important proofs. If there are interests, I will also talk about how one might apply automatic structures to program verification (this line of research is still under intense development).

Finite model theory primarily concerns finite structures, and has been successfully applied to database theory, and logical approaches to verification (i.e. model checking). On the other hand, finite structures are often too restrictive. For example, when modeling C programs, the use of infinite structures is often inevitable. For this reason, a lot of effort has been put into extending the framework of finite model theory to infinite structures. Several such approaches include metafinite model theory, embedded finite model theory, and automatic structures. In the sequel, we are primarily interested in automatic structures.

Roughly speaking, automatic structures are structures whose universe, and relations can each be represented by a finite automaton. A simple example of automatic structures is Presburger arithmetic (N,+), where N is the set of natural numbers. Here is how one might represent (N,+) using finite automata. Represent the universe N in binary in reverse order (e.g. 4 = 001, 2 = 01); call such a representation bin(N). So, bin(N) is a language over Σ = {0,1}. It is simple to devise a finite automaton that recognizes precisely bin(N). Now, how do we represent the 3-ary relation

+ = { (bin(i),bin(j),bin(k)) : i + j = k, i,j,k ∈ N }

with an automaton? First, it is possible to represent the relation + as a language L over the alphabet {0,1,#}³ defined in the following way. For i,j,k ∈ bin(N), concatenate i,j,k with the padding symbol # so that the resulting strings i',j',k' are of the same length. For example, if i = 001, j = 01, and k = 00001, then i' = 001##, j' = 01###, and k' = 00001. Now, we may treat the tuple (i',j',k') as a string over the alphabet {0,1,#}³, e.g., for i',j',k' in the above example, the resulting string is (0,0,0)(0,1,0)(1,#,0)(#,#,0)(#,#,1). Then, if i + j = k, put the string (i',j',k') in L. Having defined L, it is not hard to exhibit an automaton that recognizes precisely L. [This automaton resembles the commonplace algorithm for addition.]

What is so cool about automatic structures? First, it is somewhat immediate that automatic structures have decidable FO theories. Second, there exists a universal automatic structure M_univ, which is a structure in which all other automatic structures can be interpreted with FO translation (or reduction). Furthermore, the set of all relations definable in M_univ captures precisely all regular relations, which gives an easy way to prove properties about regular languages. By the way, automatic structures also give a nice way of proving that model checking some types of infinite transition systems be decidable.

Anyway, this post was merely intended to whet the reader's appetite. I hope this was enticing enough. In the next post, I will give a precise definition of automatic structures and prove the Buchi-Bruyer theorem that the set of relations definable in M_univ coincides with all regular relations.

Reading Group

I am at present organizing a reading group on "Model Checking on Nice Infinite Structures". Its purpose is to help the participants get a big picture of the area, know which problems are presently open, and understand proof ideas without having to read every paper. In sum, if you want to get up to speed with the state of the art, attend the meetings!

Two upcoming meetings are as follows:

1. My supervisor Leonid Libkin will give an introduction to Automatic Structures on Thursday, March 23, from 2pm-3pm, UofT St. George Campus, PT378.
   
2. Pablo Barcelo will give the first part of his presentation on Walukiewicz's proof of Muchnik's theorem on Friday, March 24, from 3pm-4pm, UofT St. George Campus, PT378.
   

Feel free to stop by if you are in Toronto.

I've tried to give a flavor of the area before. I will say a little bit more. The main concern of the area is to come up with nice infinite structures on which model checking L-formulas (for some nice logic L) is computationally effective. For example, Buchi's theorem and Rabin's theorem give effective procedures for model-checking MSO formulas on, respectively, the infinite one-way successor S1S = (N,‹) and the infinite binary tree S2S = ({0,1}*,S0,S1) where

1. N is the set of natural numbers, and ‹ the graph of the usual successor function on N.
   
2. {0,1}* stands for bit strings (including the empty string),
   
   S0 = { (w,w0) : w ∈ {0,1}* },
   
   and
   
   S1 = { (w,w1) : w ∈ {0,1}* }.
   
   

It turns out that one can obtain a large number of decidability results via interpretation to S2S. As I mention previously, one can show that model checking MSO formulas on pushdown graphs is effective. In fact, using the same technique, one can show that the MSO theory of ordered rational numbers (Q,<) is decidable.

There is more to "Model Checking on Nice Infinite Structures" than what I just mentioned. For example, one of the most important research directions is to come up with "ways of transforming structures" that preserve decidability of L-theories. Examples of such transformations include unfoldings, and iterations. The latter transformation is the main concern of Muchnik's theorem, which will be presented by Pablo Barcelo some time this week. These decidability-preserving transformations are so powerful that one can obtain the decidability of S2S by reducing it to a trivial edge-labeled graph with one node and two self-loops of different labels. It turns out that one can obtain a rich theory by, for example, applying MSO-interpretations and the unfolding operation in alternation. This is the subject of Caucal's hierarchy. For more, see for the link to Thomas's survey in my previous post.

Another hot topic includes "Automatic Structures". Roughly speaking, automatic structures are logical structures that can be presented by finite automata. For example, one can obtain a characterization of regular languages using this technique. For more, see this paper.

403 Forbidden

Some of you have informed me of not being able to access this blog recently. In fact, I am aware of this problem when trying to publish some of my recent posts.

I recently learned that is caused by problems with some of the Blogger's servers (for more, read this). This affects some, but not all, blogs from Blogger (unfortunately, including Logicomp). But, this problem goes away usually within 24 hours. So, if your computer fails to access this blog next time, please be patient and come back the following morning :-)

Model-checking on infinite transition systems

"Program testing can be used to show the presence of bugs, but never to show their absence!", said Edsger Dijkstra. Model-checking is one well-known approach to automatic verification of programs. The framework of model-checking can be described as follows. Given a representation of a program P as a finite transition system (a.k.a. Kripke Structures) M(P) and given a formal specification f in a specification language L, check whether f is true in M(P), in symbols M(P) |= f. The specification language can be any of your favorite logics; but, the most frequently used ones include LTL, CTL, CTL*, and μ-calculus. Recently, a lot of effort has been made to extend the framework to suitable classes of infinite structures. In this post, I will mostly talk about model-checking on infinite transition systems. The logic that we frequently use in this case is monadic second-order logic (MSO) as

1. It subsumes most modal logics that we use in verification including all the afore-mentioned logics, and
   
2. MSO is a well-behaved and well-studied logic.
   

Here is a quick memory refresher: MSO is first-order logic (FO) that is extended by quantification over sets and atomic formulas of the form "x ∈ X" with the meaning that the element x of the domain D of given interpretation belongs to the set X, which is interpreted as a subset of D.

I will talk about one simple kind of infinite transition systems that goes by the name of pushdown graphs. A pushdown graph is nothing but the transition graph of a pushdown automaton. Here, a pushdown automaton is a tuple (Q,A,Γ, q₀, Z₀, Δ), where Q is a finite set of states, A the input alphabet, Γ the stack alphabet, Z₀ ∈ Γ the initial stack symbol, and the transition relation Δ is a finite subset of Q x A x Γ x Γ^* x Q, where (q,a,v,&alpha,q') is to be interpreted as "Whenever I am on a state q, see the letter a on the input tape, and see the letter v on the stack tape, I will replace v by the word α and move to a new state q'". Further, for a technical reason, it is usually wise to assume that there is no transition rule that pops the stack symbol Z₀. Now a pushdown graph for this automaton is the infinite graph G = (V,(E_a)_{a ∈ A}) where:

• V is the set of configurations of the automaton (i.e. words from QΓ^*, a product of the current state and the stack configurations) that are reachable from q₀Z₀ by a finite number of applications of Δ,
  
• E_a is the set of all pairs (qvw,q'αw) from V² for which there is a transition (q,a,v,α,q').
  

A result of Muller-Schupp is that MSO model-checking problem on pushdown graphs is decidable. The proof of this result is by direct MSO-interpretation to S2S (MSO theory of 2-successors), and uses Rabin's deep result that S2S be decidable. I recommend

W. Thomas. Constructing Infinite Graphs with a Decidable MSO-theory

for a nice presentation of this proof.

Now comes the most important question. What sort of queries can you ask in MSO regarding pushdown graphs? The most useful one is reachability, i.e., given two configurations C and C', determine whether C' is reachable from C. This is how you write it in MSO:

REACH(x,x') ≡ ∀ X( x∈X and ∀y,z( y∈X and E(y,z) --> z∈X) --> x'∈X)

As usual, E(x,y) is an abbreviation for "OR_{a ∈ A} E(x,y)". It turns out that there are lots of fancy infinite graphs on which MSO model-checking are decidable. But, this is a subject of future posts.