Linear Temporal Logic (1)

As their name suggests, temporal logics are logics where truth values of formulas may change over time. The significance of temporal logic in computer science is indisputable, especially in verification of safety-critical reactive systems. Model checkers of many flavors of temporal logics have been developed to the extent that they can quickly verify real-world systems with a huge number of states. Furthermore, in contrast to many other tools and techniques of formal methods which are semi-automatic and relatively expensive, model checking is fully-automatic and quite cheap (excellent free model checkers like SPIN exist). Last year these tools and techniques were awarded the ACM Paris Kanellakis Theory and Practice Award. Amir Pnueli, the researcher who introduced the idea of using temporal logic in verification, was awarded the ACM Turing Award in 1996.

As we mentioned, temporal logic comes in a number of flavors. At present we deal only with Linear Temporal Logic (LTL). It is linear because we evaluate each LTL formula with respect to a vertex-labeled infinite path p₀p₁..., where each vertex p_i in the path corresponds to a point in time. "Present" is p₀. "Future" is any of p_i with i ≥ 0. Each vertex is labeled by a subset of 2^Σ where Σ is a set of atomic propositions. In other words, the label of a vertex indicates which atomic propositions are true in that vertex. Here is a somewhat contrived example. Suppose that Σ = {a,b}. As an example, take the path {a}²⁰⁰⁰{a,b}^ω, which is a path whose first 2000 vertices are {a}-labeled and the rest of the vertices are {a,b}-labeled. An example of an LTL formula is "at some point in the future, 'b' holds", which is true. Another example is "a holds until b holds", which is also true.

More formally, the syntax of LTL formulas can be defined in Backus-Naur form as follows:

φ, ψ := p (p ∈ Σ) | φ ∧ ψ | ¬ φ | X φ | φ U ψ

Given a 2^Σ-labeled (infinite) path w, we write wⁱ to refer to the infinite subpath of w starting from the ith vertex (the initial vertex is the 0th vertex). We may now define the semantics of LTL formulas:

1. w |= p (p ∈ Σ) if the label of the initial vertex of w contains p
   
2. w |= φ ∧ ψ if w |= φ and w |= ψ
   
3. w |= ¬ φ if it is not the case that w |= φ
   
4. w |= X φ if w¹ |= φ
   
5. w |= φ U ψ if there exists j ≥ 0 such that w^j |= ψ and for all 0 ≤ i < j, we have wⁱ |= φ
   

We use F φ to abbreviate "true U φ", which says that φ holds in some future. Note that "future" also includes the present. We use G φ to abbreviate ¬ F ¬ φ, which says that φ must hold at all points in the path, i.e., globally. Finally, note that {¬,∧} captures all other boolean connectives, which allows us to freely use any boolean connectives when we write formulas.

How do we use LTL to verify real world systems? The answer requires that we first define the semantics of LTL formulas with respect to Kripke Structures. A Kripke structure K over a finite alphabet Σ is a tuple (S,E,λ: S -> 2^Σ), where S is a set of vertices (or states)and E a set of directed edges on S. It is normally assumed that each vertex in S has at least one outgoing edge. The function λ defines which propositions in Σ are true in a given state. The reader should convince himself that the notion of Kripke structures can be used to model many practical systems. You can first start with traffic lights, in which case &Sigma = {green,red,yellow}, S consists of three states (each corresponding to the event where the light is green, red, or yellow), and E models how traffic lights work (e.g. green -> yellow -> red). A more interesting example includes Dijkstra's algorithm for the dining philosopher problem.

Now, given a state s in structure K, we may define the semantics of LTL formulas: K,s |= φ if for all directed path w in K starting from s, we have w |= φ. For example, if K models traffic lights, then the formulas G( green -> F red ) and G( green -> X yellow ) have to hold in every state of K. [For example, the first formula says that, it is globally true that if the light is presently green, then at some point in the future it will turn red.]

What we are interested in is an algorithm that solves the following model-checking problem: given a Kripke structure K over Σ, a state s in K, and an LTL formula φ over Σ, decide whether K,s |= φ. The problem is PSPACE-complete. The best known algorithm, which runs in 2^O(|φ|) x |K|, was given by Vardi and Wolper by utilizing automata theory on infinite strings. Although the complexity of the algorithm is exponential in the size of the formula, the algorithm runs quite fast in practice because practical specifications are usually short. We shall talk about this algorithm in the near future.

Australia vs. Japan: 3 - 1

Go Aussie!

Game theoretic characterization of treewidth

There is no doubt that the notion of treewidth introduced by Robertson and Seymour is one of the most important concepts in math and computer science introduced in the past thirty years. Roughly speaking, treewidth of a graph G measures how much G looks like a tree. For example, the treewidths of a tree, of a cycle, and of a clique (with n vertices) are respectively 1, 2, and n.

Some of the readers might not be aware of an intuitive way of understanding the concept of treewidths that is provided by the cops-and-robber games, as pointed out by Seymour and Thomas in their paper "Graph searching and a min-max theorem for treewidth", Journal of Combinatorial Theory B, Vol. 58 (1993). The following presentation follows the second paper cited at the bottom. The k-cops-and-robber games, where k > 1, takes a graph G = (V,E) as a parameter. Each game has two players: the cops and the robber. The game goes as follows:

1. In round 0, the cops choose a subset X₀ of V of size at most k. The robber chooses a vertex v₀ of V - X₀.
   
2. In round i+1, the cops choose a subset X_i+1 of V of size at most k. If possible, the robber chooses a vertex v_i+1 of V - X_i+1 such that there is a (possibly empty) path from v_i to v_i+1 which does not pass through X_i ∩ X_i+1. Otherwise, the cops win the game right there.
   

If this game has no end (i.e. the robber can evade capture), then the robber wins. The cops are said to have a winning strategy on the k-cops-and-robber game on G if they can play in such a way that they will eventually win the game. Otherwise, we say that the robber has a winning strategy on this game.

It is helpful to think of the set X_i+1 - X_i as set of vertices above which the cops are hovering in helicopters in round i+1. [This tells us that cops can move from vertices to vertices unrestrictedly.] Also, the set X_i+1 ∩ X_i can be thought of as the vertices where the cops have landed from helicopters. So, it takes two moves for a cop to be at a particular vertex v (i.e. on the ground): she must first ride a helicopter to v, and second land the helicopter at v. On the other hand, a cop may take off to another vertex (but still is in a helicopter) in just one move. In addition, the robber can see the cops in the helicopter, and may elude capture by running at great speed to another vertex as long as he does not run through a cop on the ground during his escape.

Theorem (Seymour and Thomas): A graph G has treewidth ≤ k-1 iff the cops have a winning strategy in the k-cops-and-robber game on G.

Equivalently, a graph G has treewidth k-1 iff k is the smallest number k' such that the cops have a winning strategy in the k'-cops-and-robber game on G. Let's try this game on a tree. The cops can win the game using 2 cops only. The idea is to gradually shrink the set of vertices the robber can go to in the next round by alternately moving the two cops in a "depth-first traversal" manner. On the other hand, it is clear that the robber player has a winning strategy on a tree if he is chased by only a poor lone cop.

In recent years, some researchers in databases and verification have proposed variants of the cops-and-robber games so as to explain some phenomena in those fields. Let me conclude by mentioning two such papers:

1. Gottlob, Leone, and Scarcello. Robbers, marshals, and guards: game theoretic and logical characterization of hypertree width, JCSS 66, 2003.
   
2. Berwanger, Dawar, Hunter, and Kreutzer. DAG-width and Parity Games, STACS 2006.
   

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.