tag:blogger.com,1999:blog-129324582024-03-14T01:15:18.802-05:00LogicompLogic and Complexity ... among othersanthonywlinhttp://www.blogger.com/profile/07618509800342861247noreply@blogger.comBlogger62125tag:blogger.com,1999:blog-12932458.post-76486166395527293152017-06-04T17:19:00.000-05:002017-06-04T17:19:17.124-05:00Correctness by design vs. formal verification<div dir="ltr" style="text-align: left;" trbidi="on">
<div>
One common debate in the programming language community is the notion of correctness by design vs. verifying the correctness of your program. After all, if you can guarantee that all the programs that you write to be correct by construction, then there is no need to separately prove its correctness (using program analysis, formal verification, you name it), which is arguably non-trivial in general. How might you ensure correctness by construction? One easy way is to design a programming language that *rules out* certain bugs. For example, back in the 2001 when I started learning programming in C and then C++, I had to learn how to debug segmentation faults. A switch to higher-level programming languages like Java and Python ensures that I don't have to deal with segmentation faults anymore (assuming the correctness of JVM and Python interpreters). Can you do the same with other kinds of errors?</div>
<div>
<br /></div>
<div>
An interesting CACM article that I recently read (<a href="https://cacm.acm.org/magazines/2017/5/216322-ending-null-pointer-crashes/fulltext">https://cacm.acm.org/magazines/2017/5/216322-ending-null-pointer-crashes/fulltext</a>) discusses how the programming language Eiffel eliminates the problem of null pointer crashes (which could cause serious security vulnerabilities). A null pointer dereferencing happens when you invoke <i>x.f</i> in an object-oriented programming language, where <i>x</i> is a variable pointing to null and <i>f</i> is a field. It turns out that eliminating null pointer dereferencing by language design in a way that does <i>not severely limit the expressiveness and convenience</i> of the language is not straightforward, as discussed in the article. Eiffel instead relies on sophisticated use of type checking and static analysis to ensure that a program that passes an Eiffel compiler cannot exhibit null pointer crashes. So, the case study of Eiffel seems to suggest that correctness should be achieved not only by only language design or software verification alone, but by <i>both</i> of them simultaneously.</div>
<div>
<br /></div>
<div>
What about other kinds of programming errors, e.g., cross-site scripting in HTML5, data race condition in concurrent programming?</div>
</div>
anthonywlinhttp://www.blogger.com/profile/07618509800342861247noreply@blogger.com0tag:blogger.com,1999:blog-12932458.post-31320384642571833122008-10-27T06:10:00.000-05:002008-10-27T06:18:57.662-05:00When does Bob deserve to be a co-author?I have recently been reading Bill Gasarch's <a href="http://weblog.fortnow.com/2008/10/when-does-alice-deserve-to-be-co-author.html">post</a> about when Alice deserves to be a co-author. This is definitely a sensitive issue; just check the number of ANONYMOUS comments. I have recently found some <span style="font-style:italic;">advice</span> that is more oriented towards faculty-student type of collaborations, but is perhaps also suitable in general. Check this <a href="http://www.acsp.org/Documents/Credit_for_collab_faculty-student_work.html">link</a>. Interestingly, it was a document written by Department of City and Regional Planning, University of Berkeley ...anthonywlinhttp://www.blogger.com/profile/07618509800342861247noreply@blogger.com27tag:blogger.com,1999:blog-12932458.post-58414304158858582802008-07-16T14:35:00.002-05:002008-10-26T06:50:22.771-05:00Highland workshop on XML, Logic, and AutomataI'll be attending <a href="http://homepages.inf.ed.ac.uk/libkin/highlandsworkshop.html">Highlands Workshop</a> on XML, Logic, and Automata organized by Leonid from tomorrow until this Sunday. The venue is actually quite interesting: a small town in the Highlands called <a href="http://en.wikipedia.org/wiki/Grantown-on-Spey">Grantown-on-spey</a>. I'm just hoping that they have a grocery store :) I will give a presentation on recurrent reachability in regular model checking based on <a href="http://homepages.inf.ed.ac.uk/s0673998/papers/lpar08_full.pdf">this paper</a>. Anyway, I'll post a summary of the workshop later on this week.anthonywlinhttp://www.blogger.com/profile/07618509800342861247noreply@blogger.com28tag:blogger.com,1999:blog-12932458.post-23853507850442744592008-07-14T10:30:00.001-05:002008-07-14T10:35:44.658-05:00Rahul Santhanam has joined EdinburghRahul Santhanam, <a href="http://lance.fortnow.com/">Lance Fortnow's</a> ex PhD student, has recently <a href="http://homepages.inf.ed.ac.uk/mfourman/blogs/news/2007/06/rahul-santhanam.html">joined</a> Edinburgh's School of Informatics. Warm welcome to him!anthonywlinhttp://www.blogger.com/profile/07618509800342861247noreply@blogger.com27tag:blogger.com,1999:blog-12932458.post-51010306886606580392008-07-02T08:47:00.001-05:002008-07-02T09:00:22.108-05:00Finite-variable hierarchy conjectureIt seems that <a href="http://www.mit.edu/~brossman/">Ben Rossman</a> has resolved another long-standing open problem in finite model theory: finite-variable hierarchy conjecture. Loosely speaking, the conjecture is that over ordered graphs first-order logic with k+1 variable is more powerful than first-order logic with k variable. The problem is nicely summarized in <a href="http://www.cl.cam.ac.uk/~ad260/papers/gabbay60.ps">Anuj Dawar's survey</a>. Ben has <a href="http://www.mit.edu/~brossman/k-clique-stoc.pdf">shown</a> that this hierarchy is strict. What was previously known is that (over ordered graphs) first-order logic with 3 variables is strictly more expressive than first-order logic with 2 variables, but it was not known whether first-order logic with 3 variables is less expressive than first-order logic with k variables, for every k > 3. Worse yet, it wasn't even known whether this hierarchy is strict. See Anuj Dawar's survey for further details.<br /><br />I believe this is the third big open problems that Ben has resolved in this decade. Go Ben!anthonywlinhttp://www.blogger.com/profile/07618509800342861247noreply@blogger.com29tag:blogger.com,1999:blog-12932458.post-60614147028146309262008-06-30T09:03:00.000-05:002008-06-30T09:19:26.779-05:00Restructuring logicompI'm thinking of restructuring my blogs. I've recently found that things have changed a lot since I started my break a year or so ago: Lance has retired from blogging, Andy D has started his <a href="http://andysresearch.blogspot.com/">new cool blog</a>, and Luca Aceto has his <a href="http://processalgebra.blogspot.com/">blog</a>. Ah ... also I'm having a lot of difficulty deciphering blogger's word verification mechanism. <br /><br />Unfortunately, I've become really rusty with HTML and will have to start getting used to it again. Shocked with what a long break can do to one's dexterity ;) Anyway, I'll put all the new links some time soon.anthonywlinhttp://www.blogger.com/profile/07618509800342861247noreply@blogger.com25tag:blogger.com,1999:blog-12932458.post-89200977525614730842008-06-26T08:08:00.002-05:002008-06-27T10:30:39.704-05:00Pushdown systems: reachability via saturationsFinally, I have some time to resume blogging again after finishing several papers (and now with something with more content). Before I continue, I'd like to apologize for not replying some comments because by mistake I had them forwarded to an expired email address. How careless I was!<br /><br />Anyway, I'm intending to cover a simple basic topic in the verification of infinite-state systems. Reachability is probably the most basic question when you do verification and we would like to see how to solve this problem <em>efficiently</em> for pushdown systems, which are the simplest well-behaved class of infinite-state systems. For those practically-minded, pushdown systems can naturally be used to model sequential programs and algorithms for pushdown systems have been implemented and used for doing program analysis <em>for real</em>. By the way, the saturation technique also extends to other (more powerful) classes of infinite-state systems and so it's really worth knowing. Anyway, please review the definition of pushdown systems <a href="http://logicomp.blogspot.com/2006/03/model-checking-on-infinite-transition.html">here</a> before you continue.<br /><br />Roughly speaking, the reachability problem for pushdown systems asks the following question: given a pushdown system P and two configurations C<sub>1</sub> and C<sub>2</sub> of P, is it possible to reach C<sub>2</sub> from C<sub>1</sub> in P? There are other variants of the problem that take sets of configurations instead of just single configurations, and they can be solved using exactly the same saturation technique.<br /><br />In <a href="http://logicomp.blogspot.com/2006/03/model-checking-on-infinite-transition.html">here</a> I have mentioned that the MSO theory of pushdown systems is decidable and this implies that reachability is also decidable. However, the algorithm that you obtain in this way runs in exponential time.<br /><br />The idea of saturation construction is to construct a finite automaton A that recognizes the set of configurations that can reach C<sub>2</sub> and then check whether C<sub>1</sub> is in the language of A; recall that membership checking for finite automata is solvable in linear time. First, observe that C<sub>2</sub> is a single word and is obviously regular. We start with an automaton for C<sub>2</sub> and introduce several extra states, each corresponding to a state of the pushdown system P. Call this automaton A. We shall <em>iteratively</em> add transitions to A by the following rules: if there is a transition (p,a,c,v,p') in P, and in the automaton A the state p' can reach a state q via the word v, then we shall add a transition (p,c,q) in A. The intuitive idea is that if a configuration p'vw is accepted by A, then the configuration paw must also be accepted by A because you can apply the transition (p,a,c,v,p'). By the way, notice that we don't add any states in the iteration and so the algorithm can only add polynomially many transitions to A. Hence, the algorithm terminates in polynomial time.<br /><br />As far as I remember, the idea was first proposed in the paper by Bouajjani, Esparza, and Maler for pushdown systems:<br /><br /><blockquote>Reachability analysis of pushdown automata: Application to model-checking. CONCUR 1997.</blockquote><br /><br />It seems that similar ideas were already proposed earlier for ground tree rewrite systems, a more general class of systems, in:<br /><br /><blockquote>Coquide, Dauchet, and Gilleron. Bottom-up tree pushdown automata: classification and connection with rewrite systems. Theoretical Computer Science 127, 1994.</blockquote><br /><br />By the way, it is worth noticing that simple fixpoint computations might not terminate for pushdown systems, as the state space is infinite. So, the saturation construction is necessary after all.anthonywlinhttp://www.blogger.com/profile/07618509800342861247noreply@blogger.com25tag:blogger.com,1999:blog-12932458.post-32855916535396940412008-01-14T07:12:00.000-05:002008-01-14T07:56:45.412-05:00Happy New Year 2008!It was exactly a year ago that I wrote my last post. I guess I have been really busy doing research (yes, this is an excuse that always works for us researchers). I am planning on writing a few things on what research I have been doing recently in some details (as I used to do); partly to help me understand more stuff, and partly to spread around some good news about the area of logic and verification (and computation as well, of course).<br /><br />Without further ado, here are some plans for my posts for the next two to three weeks:<br /><ol><br /><li><span style="font-style:italic;">Some extensions of pushdown systems and how to do model checking on these structures</span>. I covered the definitions of pushdown systems already in <a href="http://logicomp.blogspot.com/2006/03/model-checking-on-infinite-transition.html">here</a>, but not how to do model checking on these structures. So, I'll start there. Extensions that I will consider including prefix-recognizable systems, ground tree rewrite systems, and some probabilistic extensions.</li><br /><li><span style="font-style:italic;">Well-structured transition systems</span>. The theory of WSTS, which rely heavily on the theory of well-ordered quasi ordering, give general decidability results for reachability checking for large classes of infinite-state transition systems (eg, Petri Nets, lossy counter systems, etc). <br /></li></ol>anthonywlinhttp://www.blogger.com/profile/07618509800342861247noreply@blogger.com25tag:blogger.com,1999:blog-12932458.post-1168451644648466942007-01-10T12:53:00.000-05:002007-01-11T22:05:57.916-05:00I have moved again ...It seems like ages since I last wrote for this blog. Last September, I moved with my advisor to the University of Edinburgh to begin my PhD. It took me longer than I thought to settle in Edinburgh as the atmosphere of the city, ESPECIALLY the gloomy weather, is quite different to that which I am accustomed to. Folklore has it that there are only sixty sunny days in Edinburgh in a year on average. I presume that forty of these days are in the summer. The other peculiarity that you can find in Edinburgh is the wind and rain. If you live outside Edinburgh and think that your city is windy, then I suggest that you come to visit Edinburgh. Actually, you'll find that the combination of wind and rain makes umbrella pretty much useless! <br /><br />Anyway, apologies to my avid readers that I was silent for so long. Provided there is time and interest, I will blog again on a weekly basis.anthonywlinhttp://www.blogger.com/profile/07618509800342861247noreply@blogger.com32tag:blogger.com,1999:blog-12932458.post-1151011210746103932006-06-22T16:06:00.000-05:002006-06-22T16:20:11.026-05:00Australia qualifies for round of 16<img src="http://us.news1.yimg.com/us.yimg.com/i/fifa/gen/xp/20060622/i/1238960103.jpg" width=352 height=400 border=0><br /><br />After losing 2 - 0 to Brazil, The Socceroos had to at least draw against Croatia. What a nerve-racking (and controversial) game that was! In the end, <a href="http://fifaworldcup.yahoo.com/06/en/060622/1/83ql.html">Australia managed to draw 2 - 2 against Croatia</a>. Although I am supporting Australia through and through, I think that The Socceroos didn't secure the desired result convincingly. In a way, we were lucky to get a draw! Next: Italy vs. Australia.anthonywlinhttp://www.blogger.com/profile/07618509800342861247noreply@blogger.com26tag:blogger.com,1999:blog-12932458.post-1148708259687487692006-06-14T15:57:00.000-05:002006-06-15T12:38:02.930-05:00Linear Temporal Logic (1)As their name suggests, <a href="http://en.wikipedia.org/wiki/Temporal_logic">temporal logics</a> 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.<br /><br />As we mentioned, temporal logic comes in a number of flavors. At present we deal only with <i>Linear Temporal Logic (LTL)</i>. It is <i>linear</i> because we evaluate each LTL formula with respect to a vertex-labeled infinite path p<sub>0</sub>p<sub>1</sub>..., where each vertex p<sub>i</sub> in the path corresponds to a point in time. "Present" is p<sub>0</sub>. "Future" is any of p<sub>i</sub> with i ≥ 0. Each vertex is labeled by a subset of 2<sup>Σ</sup> where Σ is a set of <i>atomic propositions</i>. In other words, the label of a vertex indicates which atomic propositions are <i>true</i> in that vertex. Here is a somewhat contrived example. Suppose that Σ = {a,b}. As an example, take the path {a}<sup>2000</sup>{a,b}<sup>ω</sup>, 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.<br /><br />More formally, the syntax of LTL formulas can be defined in Backus-Naur form as follows:<br /><center><br /> φ, ψ := p (p ∈ Σ) | φ ∧ ψ | ¬ φ | X φ | φ U ψ<br /></center><br />Given a 2<sup>Σ</sup>-labeled (infinite) path w, we write w<sup>i</sup> 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:<br /><ol><br /> <li> w |= p (p ∈ Σ) if the label of the initial vertex of w contains p<br /> <li> w |= φ ∧ ψ if w |= φ and w |= ψ<br /> <li> w |= ¬ φ if it is not the case that w |= φ<br /> <li> w |= X φ if w<sup>1</sup> |= φ<br /> <li> w |= φ U ψ if there exists j ≥ 0 such that w<sup>j</sup> |= ψ and for all 0 ≤ i < j, we have w<sup>i</sup> |= φ<br /></ol><br />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., <em>globally</em>. Finally, note that {¬,∧} captures all other boolean connectives, which allows us to freely use any boolean connectives when we write formulas.<br /><br />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 <i>Kripke Structures</i>. A <i>Kripke structure</i> K over a finite alphabet Σ is a tuple (S,E,λ: S -> 2<sup>Σ</sup>), where S is a set of vertices (or <i>states</i>)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 <a href="http://en.wikipedia.org/wiki/Dining_philosophers_problem">Dijkstra's algorithm for the dining philosopher problem</a>.<br /><br />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.]<br /><br />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<sup>O(|φ|)</sup> 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.anthonywlinhttp://www.blogger.com/profile/07618509800342861247noreply@blogger.com24tag:blogger.com,1999:blog-12932458.post-1150137217036105472006-06-12T13:30:00.000-05:002006-06-12T13:33:37.490-05:00Australia vs. Japan: 3 - 1<a href="http://fifaworldcup.yahoo.com/06/en/w/match/template.html?id=12">Go Aussie</a>!anthonywlinhttp://www.blogger.com/profile/07618509800342861247noreply@blogger.com2tag:blogger.com,1999:blog-12932458.post-1146590101187166162006-05-02T10:42:00.000-05:002006-05-11T23:09:55.620-05:00Game theoretic characterization of treewidthThere is no doubt that the notion of <a href="http://en.wikipedia.org/wiki/Treewidth">treewidth</a> 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.<br /><br />Some of the readers might not be aware of an intuitive way of understanding the concept of treewidths that is provided by the <i>cops-and-robber games</i>, 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 <i>cops</i> and the <i>robber</i>. The game goes as follows:<br /><ol><br /> <li> In round 0, the cops choose a subset X<sub>0</sub> of V of size at most k. The robber chooses a vertex v<sub>0</sub> of V - X<sub>0</sub>. <br /> <li> In round i+1, the cops choose a subset X<sub>i+1</sub> of V of size at most k. If possible, the robber chooses a vertex v<sub>i+1</sub> of V - X<sub>i+1</sub> such that there is a (possibly empty) path from v<sub>i</sub> to v<sub>i+1</sub> which does not pass through X<sub>i</sub> ∩ X<sub>i+1</sub>. Otherwise, the cops win the game right there.<br /></ol><br />If this game has no end (i.e. the robber can evade capture), then the robber wins. The cops are said to <i>have a winning strategy</i> 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 <i>has a winning strategy</i> on this game.<br /><br />It is helpful to think of the set X<sub>i+1</sub> - X<sub>i</sub> 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<sub>i+1</sub> ∩ X<sub>i</sub> 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.<br /><br /><b>Theorem</b> (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.<br /><br />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.<br /><br />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:<br /><ol><br /> <li>Gottlob, Leone, and Scarcello. <i>Robbers, marshals, and guards: game theoretic and logical characterization of hypertree width</i>, JCSS 66, 2003.<br /> <li>Berwanger, Dawar, Hunter, and Kreutzer. <i>DAG-width and Parity Games</i>, STACS 2006.<br /></ol>anthonywlinhttp://www.blogger.com/profile/07618509800342861247noreply@blogger.com7tag:blogger.com,1999:blog-12932458.post-1145988149685204232006-04-25T12:53:00.000-05:002006-04-27T16:17:35.973-05:00Automatic Structures: Part 2 -- Buchi-Bruyer TheoremWe 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<sub>univ</sub> (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.<br /><br />We first need some definitions. Suppose that <b>s</b> := (s<sub>1</sub>, ...,s<sub>n</sub>) ∈ (Σ*)<sup>n</sup>. Then, define a string [<b>s</b>] over the alphabet (Σ∪ {#})<sup>n</sup> whose length is max{s<sub>1</sub>,...,s<sub>n</sub>}, and whose ith symbol is (a<sub>1</sub>,...,a<sub>n</sub>) where a<sub>j</sub> is the ith symbol of s<sub>j</sub>, if i ≤ |s<sub>j</sub>|, and a<sub>j</sub> is #, otherwise. One might visualize [<b>s</b>] as the string obtained by placing s<sub>1</sub>,...,s<sub>n</sub> in a left-aligned column and pad each string s<sub>i</sub> with # so that each of the resulting rows is of equal length. After that, we consider this matrix as a string [<b>s</b>] whose jth position is the jth column of the string. A subset S of (Σ*)<sup>n</sup> is said to be <i>regular</i> if the set { [<b>s</b>] : <b>s</b> ∈ S } is regular.<br /><br />Fix an alphabet of size at least two. Consider the infinite structure M<sub>univ</sub> := (Σ*, ≤, (L<sub>a</sub>)<sub>a ∈ Σ</sub>, el) where<br /><ol><br /> <li>the universe is the set of all Σ-strings,<br /> <li>x ≤ y iff x is a prefix of y,<br /> <li>L<sub>a</sub>(x) is true iff the rightmost symbol of x is a, and<br /> <li>el(x,y) is true iff |x| = |y| (|x| denotes the length of x).<br /></ol><br />What properties are (first-order) definable in M<sub>univ</sub>? Here are some simple ones:<br /><ol><br /> <li>|x| ≤ |y| (i.e. the string x is no longer than the string y),<br /> <li>|x| = |y| + k for some fixed constant k, <br /> <li>im-pref(x,y) (i.e. x = y.a for some letter a ∈ Σ), and<br /> <li>the kth symbol of x is a (where k is fixed and a ∈ Σ).<br /></ol><br />Apologize for the overloading of the symbol '≤' because of the lack of HTML symbols. For example, the first property above can be expressed as<br /><center><br /> ∃ s( s ≤ y ∧ el(x,s) ).<br /></center><br />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 ≤).<br /><br />Now, a subset S of (Σ*)<sup>n</sup> is said to be definable in M<sub>univ</sub> if there exists a first-order formula φ(x<sub>1</sub>,...,x<sub>n</sub>) in the vocabulary of M<sub>univ</sub> such that <br /><center><br /> S = { <b>s</b> : M<sub>univ</sub> |= φ(<b>s</b>) }.<br /></center><br /><br /><b>Theorem</b> (Buchi-Bruyer): A subset S of (Σ*)<sup>n</sup> is definable in M<sub>univ</sub> iff S is regular.<br /><br /><i>Proof sketch</i>:<br />(<=) Suppose that S is recognized by the automaton A = (Q,q<sub>0</sub>,F,δ: Q x Σ -> Q), where Q = {q<sub>0</sub>,...,q<sub>l</sub>} is a finite set of states, q<sub>0</sub> ∈ Q is the initial state, F ⊆ Q is the set of final states, and δ the transition function. So, for all <b>s</b> ∈ (Σ*)<sup>n</sup>, <b>s</b> ∈ S iff the string s<sub>1</sub>...s<sub>k</sub> = [<b>s</b>] is accepted by A,i.e., there exists a run p<sub>0</sub>...p<sub>k</sub> such that p<sub>0</sub> = q<sub>0</sub>, p<sub>k</sub> ∈ F, and δ(p<sub>i</sub>,s<sub>i+1</sub>) = p<sub>i+1</sub>. The defining formula for S is <br /><center><br /> φ(x<sub>1</sub>,...,x<sub>n</sub>) = ∃v<sub>0</sub>,...,v<sub>l</sub>( ψ<sub>len</sub> ∧ ψ<sub>char</sub> ∧ ψ<sub>start</sub> ∧ ψ<sub>end</sub> ∧ ψ<sub>trans</sub> )<br /></center><br />where:<br /><ol><br /> <li> ψ<sub>len</sub> asserts that |v<sub>i</sub>| = max{|x<sub>j</sub>| : 1 ≤ j ≤ n} + 1.<br /> <li> ψ<sub>char</sub> asserts that [(v<sub>1</sub>,...,v<sub>l</sub>)] = w<sub>0</sub>...w<sub>k</sub> is a <i>characteristic sequence</i>, i.e., each v<sub>i</sub> is a string of 0s and 1s, and that, for each position h, exactly one of the strings v<sub>i</sub>s have value 1. [Intuitively, we want each w<sub>j</sub> to represent the state p<sub>j</sub> in our accepting run.]<br /> <li> ψ<sub>start</sub> asserts that the first position of v<sub>0</sub> has value 1.<br /> <li> ψ<sub>end</sub> asserts that the last position of some v<sub>j</sub>, where q<sub>j</sub> ∈ F, has value 1.<br /> <li> ψ<sub>trans</sub> asserts that the transition from w<sub>j</sub> to w<sub>j+1</sub> respects δ. [This will be a huge table, quite tedious to write down.]<br /></ol><br />The reader should convince herself that all of the above sentences are definable in M<sub>univ</sub>.<br /><br />(=>) The proof is by induction on the formula φ(x<sub>1</sub>,...,x<sub>n</sub>) defining S. The base case (i.e. atomic formulas) is very easy (left to the reader). Further, the case where φ is of the form ψ<sub>1</sub> ∨ ψ<sub>2</sub> 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<sub>n+1</sub> ψ(x<sub>1</sub>,...,x<sub>n+1</sub>). Suppose that the n+1-ary regular relation R defined by ψ is recognized by the automaton A = (Q,q<sub>0</sub>,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<sub>1</sub>,...,s<sub>n+1</sub>) ∈ R, where |s<sub>n+1</sub>| > |s<sub>j</sub>| for 1 ≤ j ≤ n, then there exists another string s'<sub>n+1</sub> such that (s<sub>1</sub>,...,s'<sub>n+1</sub>) ∈ R and |s'<sub>n+1</sub>| ≤ max{|s<sub>j</sub>| : 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<sup>i</sup> = (Q<sup>i</sup> = {q<sub>0</sub><sup>i</sup>,...,q<sub>l</sub><sup>i</sup>},q<sub>0</sub><sup>i</sup>,F<sup>i</sup>,δ<sup>i</sup>). The states of A' are the union of the Q<sup>i</sup>s. The start states consist of all the q<sub>0</sub><sup>i</sup>s. The final states are the union of the F<sup>i</sup>s. The transition function δ' works as follows: whenever δ<sup>i</sup>(q<sub>j</sub><sup>i</sup>,(c<sub>1</sub>,...,c<sub>n+1</sub>)) = q<sub>h</sub><sup>i</sup>, where c<sub>m</sub> ∈ (Σ &cup {#}), we put δ'(q<sub>j</sub><sup>i</sup>,(c<sub>1</sub>,...,c<sub>n</sub>) = q<sub>h</sub><sup>i</sup>. Note that A' is non-deterministic. It is easy to check that A' recognizes S. (QED)anthonywlinhttp://www.blogger.com/profile/07618509800342861247noreply@blogger.com0tag:blogger.com,1999:blog-12932458.post-1143058850211732492006-04-20T11:42:00.000-05:002006-04-20T12:48:26.736-05:00Automatic Structures: Part 1Several weeks ago, my supervisor Leonid Libkin gave a presentation about <i>automatic structures</i> 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).<br /><br />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.<br /><br />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 <em>in reverse order</em> (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 <br /><center><br /> + = { (bin(i),bin(j),bin(k)) : i + j = k, i,j,k ∈ N }<br /></center><br />with an automaton? First, it is possible to represent the relation + as a language L over the alphabet {0,1,#}<sup>3</sup> 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,#}<sup>3</sup>, 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.]<br /><br />What is so cool about automatic structures? First, it is somewhat immediate that automatic structures have decidable FO theories. Second, there exists a <i>universal automatic structure</i> M<sub>univ</sub>, 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<sub>univ</sub> 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 <a href="http://logicomp.blogspot.com/2006/03/model-checking-on-infinite-transition.html">infinite transition systems</a> be decidable.<br /><br />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<sub>univ</sub> coincides with all regular relations.anthonywlinhttp://www.blogger.com/profile/07618509800342861247noreply@blogger.com3tag:blogger.com,1999:blog-12932458.post-1143057492627683672006-03-22T14:04:00.000-05:002006-03-22T15:05:09.530-05:00Reading GroupI 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!<br /><br />Two upcoming meetings are as follows:<br /><ol><br /> <li> My supervisor Leonid Libkin will give an introduction to Automatic Structures on Thursday, March 23, from 2pm-3pm, UofT St. George Campus, PT378.<br /> <li> 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.<br /></ol><br />Feel free to stop by if you are in Toronto.<br /><br />I've <a href="http://logicomp.blogspot.com/2006/03/model-checking-on-infinite-transition.html">tried to give a flavor of the area</a> 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<br /><ol><br /> <li> N is the set of natural numbers, and ‹ the graph of the usual successor function on N.<br /> <li> {0,1}* stands for bit strings (including the empty string), <br /><center><br /> S0 = { (w,w0) : w ∈ {0,1}* },<br /></center><br />and<br /><center><br />S1 = { (w,w1) : w ∈ {0,1}* }.<br /></center><br /></ol><br />It turns out that one can obtain a large number of decidability results via <i>interpretation</i> to S2S. As I mention <a href="http://logicomp.blogspot.com/2006/03/model-checking-on-infinite-transition.html">previously</a>, 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.<br /><br />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 <i>in alternation</i>. This is the subject of Caucal's hierarchy. For more, see for the link to Thomas's survey in my previous post.<br /><br />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 <a href="http://www.mathematik.tu-darmstadt.de/~blumensath/Publications/LICS-2000.ps.gz">this paper</a>.anthonywlinhttp://www.blogger.com/profile/07618509800342861247noreply@blogger.com0tag:blogger.com,1999:blog-12932458.post-1142617125788757002006-03-17T12:38:00.000-05:002006-03-17T14:28:06.556-05:00403 ForbiddenSome 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. <br /><br />I recently learned that is caused by problems with some of the Blogger's servers (for more, read <a href="http://status.blogger.com/2006/03/some-users-are-currently-getting-403_08.html">this</a>). 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 :-)anthonywlinhttp://www.blogger.com/profile/07618509800342861247noreply@blogger.com2tag:blogger.com,1999:blog-12932458.post-1141940032316906882006-03-09T13:56:00.000-05:002006-03-17T09:51:07.196-05:00Model-checking on infinite transition systems"Program testing can be used to show the presence of bugs, but never to show their absence!", said <a href="http://en.wikipedia.org/wiki/Dijkstra">Edsger Dijkstra</a>. <a href="http://en.wikipedia.org/wiki/Model_checking">Model-checking</a> 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. <a href="http://en.wikipedia.org/wiki/Kripke_structure">Kripke Structures</a>) 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 <a href="http://logicomp.blogspot.com/2005/10/favorite-logic-of-october-2005-monadic.html">monadic second-order logic</a> (MSO) as <br /><ol><br /> <li> It subsumes most modal logics that we use in verification including all the afore-mentioned logics, and<br /> <li> MSO is a well-behaved and well-studied logic.<br /></ol><br />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.<br /><br />I will talk about one simple kind of infinite transition systems that goes by the name of <i>pushdown graphs</i>. A pushdown graph is nothing but the transition graph of a pushdown automaton. Here, a pushdown automaton is a tuple (Q,A,Γ, q<sub>0</sub>, Z<sub>0</sub>, Δ), where Q is a finite set of states, A the input alphabet, Γ the stack alphabet, Z<sub>0</sub> ∈ Γ the initial stack symbol, and the transition relation Δ is a finite subset of Q x A x Γ x Γ<sup>*</sup> 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<sub>0</sub>. Now a pushdown graph for this automaton is the infinite graph G = (V,(E<sub>a</sub>)<sub>a ∈ A</sub>) where:<br /><ul><br /> <li> V is the set of configurations of the automaton (i.e. words from QΓ<sup>*</sup>, a product of the current state and the stack configurations) that are reachable from q<sub>0</sub>Z<sub>0</sub> by a finite number of applications of Δ,<br /> <li> E<sub>a</sub> is the set of all pairs (qvw,q'αw) from V<sup>2</sup> for which there is a transition (q,a,v,α,q').<br /></ul><br /><br />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 <br /><center><br />W. Thomas. <a href="http://www-i7.informatik.rwth-aachen.de/d/publications/pub-Thomas.html">Constructing Infinite Graphs with a Decidable MSO-theory</a><br /></center><br />for a nice presentation of this proof.<br /><br />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:<br /><center><br /> REACH(x,x') ≡ ∀ X( x∈X and ∀y,z( y∈X and E(y,z) --> z∈X) --> x'∈X)<br /></center><br />As usual, E(x,y) is an abbreviation for "OR<sub>a ∈ A</sub> 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.anthonywlinhttp://www.blogger.com/profile/07618509800342861247noreply@blogger.com0tag:blogger.com,1999:blog-12932458.post-1141782845022881072006-03-07T20:36:00.000-05:002006-03-07T20:54:05.043-05:00Slides from Logic and Databases Workshop at CambridgeLast week I was attending a <a href="http://www.newton.cam.ac.uk/programmes/LAA/laaw02.html">logic and databases workshop</a> at Cambridge, UK, as part of a special programme on logic and algorithms at <a href="http://www.newton.cam.ac.uk/">Newton Institute</a>. As there were some excellent talks, I want to point out that there the slides are available <a href="http://www.newton.cam.ac.uk/webseminars/pg+ws/2006/laa/laaw02/">online</a>. I personally recommend the following slides: Neven's, Lynch's, Segoufin's, Schweikardt's, Libkin's, Szeider's, and Koch's.anthonywlinhttp://www.blogger.com/profile/07618509800342861247noreply@blogger.com1tag:blogger.com,1999:blog-12932458.post-1141778931604717342006-03-07T18:07:00.000-05:002006-03-07T20:56:33.900-05:00Resuming to BlogApologies for being silent for a long time. Thanks for those who for the last few months left comments on my blog or emailing me directly, and apologies if I did not reply. Until very recently, I was not so sure of which research track in finite model theory I wanted to pursue for my graduate studies, even though I have a general overview of the area. It is a difficult, but crucial, task for a new researcher in finite model theory (I believe even for 1st year graduate students like myself) to pin down exactly where (s)he should start, as the area is both deep and diverse. Realizing that this is extremely important, I desperately tried to read more and talk more with my advisor and others (yes, at the expense of blogging and replying emails). I am glad to say that I have found something that I really like and am confident that I can contribute to; which also implies that I may resume blogging.<br /><br />I realize that it will take some time for my blog readers to resume reading this blog (I certainly hope they will), and so I will start slow. Just in case you are in Toronto, I am planning to start a reading group focusing on "monadic theory of tree-like structures" and applications to computer verification (e.g. see <a href="http://www.amazon.com/gp/product/3540003886/qid=1141777736/sr=2-2/ref=pd_bbs_b_2_2/102-9572347-4812138?s=books&v=glance&n=283155">this book</a>). If you're curious but not sure of what it is, don't worry as I will give you a flavor of the area in the next few posts. The goal is to get a big picture of the area, know which problems are open, and understand important proof ideas without having to read each paper. [Each participant will take turn to present one result each time we meet.] Everyone is warmly welcome to participate. [I will make a more detailed announcement in a week.]anthonywlinhttp://www.blogger.com/profile/07618509800342861247noreply@blogger.com0tag:blogger.com,1999:blog-12932458.post-1139684419613543132006-02-11T13:47:00.000-05:002006-02-11T14:00:19.626-05:00New Book on Parameterized ComplexityJorg Flum and Martin Grohe just published their <a href="http://www.springer.com/sgw/cda/frontpage/0,11855,1-156-22-141358322-detailsPage%253Dppmmedia%257CaboutThisBook%257CaboutThisBook,00.html">new book</a> titled Parameterized Complexity Theory. Flum and Grohe are two giants in finite model theory who have contributed so much towards the development of parameterized complexity theory, especially logical characterizations of parameterized complexity classes. At this moment, one can only purchase the book from Springer as they just appeared some time this week.<br /><br />I can't compare this book with <a href="http://www.springer.com/sgw/cda/frontpage/0,11855,1-40109-22-1519914-0,00.html">Downey and Fellow's book</a> as I haven't read Flum and Grohe's. However, I heard from several people who proof-read the book before publications that Flum and Grohe's book is much more well-written and readable than Downey and Fellow's.anthonywlinhttp://www.blogger.com/profile/07618509800342861247noreply@blogger.com0tag:blogger.com,1999:blog-12932458.post-1137949696512735442006-01-22T12:02:00.000-05:002006-01-22T12:08:16.526-05:00How much damage can be caused by a peer reviewer having a bad day?Check out <a href="http://www.computer.org/portal/site/computer/menuitem.5d61c1d591162e4b0ef1bd108bcd45f3/index.jsp?&pName=computer_level1_article&TheCat=1015&path=computer/homepage/1205&file=profession.xml&xsl=article.xsl&">this cool article</a>! You will find some hilarious reviews for award-winning papers authored by Dijkstra, Codd, Shannon, etc.anthonywlinhttp://www.blogger.com/profile/07618509800342861247noreply@blogger.com4tag:blogger.com,1999:blog-12932458.post-1137639661863610382006-01-21T22:01:00.000-05:002006-01-21T22:03:06.196-05:00Almost sure theoryWe all know that the Hilbert's <a href="http://en.wikipedia.org/wiki/Entscheidungsproblem">Enstceidungsproblem</a>, i.e. deciding whether a first-order sentence is true, is undecidable. Church, Turing, and others proved it. Recall that first-order logic admits <a href="http://logicomp.blogspot.com/2006/01/0-1-law.html">the 0-1 law</a>, i.e., every FO sentence is <i>almost surely true</i> (AST) or <i>almost surely false</i> (ASF). So, what about the problem of deciding whether an FO sentence be AST? It turns out that this is decidable. I shall outline some important ideas for proving this statement.<br /><br />Let us restrict ourselves to graphs as before. In proving that FO admits the 0-1 law, we mentioned the extension axioms EA = {P<sub>k</sub>}<sub>k ∈ N</sub>, where N is the set of all natural numbers. Extension axioms are nothing more than graph properties. In our case, P<sub>k</sub>s are FO-expressible. Although for the purpose of this post we need not understand what our extension axioms are, I will just define it for future reference:<br /><center><br />∀x<sub>1</sub>, ..., x<sub>2k</sub>( ∧<sub>i ≠ j</sub> x<sub>i</sub> &ne x<sub>j</sub> -> <br /><br />∃z( ∧<sub>1 ≤ i ≤ 2k</sub> z ≠ x<sub>i</sub> <br /><br />∧<sub>i ≤ k</sub> E(z,x<sub>i</sub>) <br /><br />∧<sub>i > k</sub> ¬E(z,x<sub>i</sub>)))<br /></center><br />Recall that a <i>theory</i> T is a set of sentences. A <i>model</i> of T is a structure that satisfies all sentences of T. The theory T is <i>consistent</i> if it has a model, and it is <i>complete</i> iff for each sentence f (of the same vocabulary), we have either T |= f, i.e. every model of T is a model of f, or T |= ¬ f. A consistent and complete theory T is <i>decidable</i> if it is possible to decide whether T |= f, for any given sentence f.<br /><br />Theorem: EA is consistent (and has a unique countable model), complete, and decidable<br /><br />We will not prove the first two statements, as we will need more model theory (see Libkin's "Elements of Finite Model Theory" for more details). To prove that EA is decidable, we need only invoke an old result from recursive theory that every recursively axiomatizable theory is decidable. The above definition of P<sub>k</sub> gives us a recursive enumeration of the axioms. <br /><br />The unique countable model for EA, denoted RG, is called the <i>random graph</i>, as its probabilistic construction is often emphasized in the literature. Using the above theorem, we derive an easy corollary:<br /><br />Corollary: For any FO sentence f, RG |= f iff μ(f) = 1.<br /><br />With these results, it is a breeze to conclude that deciding whether an FO sentence be AST is computable. To determine the exact complexity of the problem, one needs a more hairy analysis, which we will not do here. It turns out that the problem is PSPACE-complete, the proof of which can be found in<br /><center><br />E. Granjean. <i>Complexity of the first-order theory of almost all finite structures</i>, Information and Control, Volume 57, 1983.<br /></center><br />Recent work in this area mostly deals with determining fragments of second-order logic that admits the 0-1 law, and whether the almost sure theory with respect to the fragment be decidable. [It is easy to see that SO in its full power does not admit the 0-1 law.] This, however, lies outside the scope of our current discussion.anthonywlinhttp://www.blogger.com/profile/07618509800342861247noreply@blogger.com0tag:blogger.com,1999:blog-12932458.post-1136697916933863352006-01-07T23:03:00.000-05:002006-01-13T17:00:03.390-05:00The 0-1 LawTo start off the year 2006, I want to talk about the 0-1 law, which is an extremely important and elegant topic in finite model theory. A logic L (over a fixed vocabulary σ) is said to admit the 0-1 law if, for any sentence f of L, the fraction of σ-structures with universe {0,...,n-1} that satisfy the sentence f converges to either 0 or 1 as n approaches infinity. We denote this fraction by μ<sub>n</sub>(f) and the limit, if exists, by μ(f). [Of course, this means that μ and μ<sub>n</sub> ranges between 0 and 1.] In other words, every sentence f is <i>almost surely false</i> or <i>almost surely true</i>. For simplicity, let us restrict our attention to undirected loopless graphs, i.e., σ contains only one binary relation E which is both symmetric and irreflexive. Below is perhaps the most fundamental theorem about the 0-1 law.<br /><br />Theorem (Fagin 1976, Glebskii et al. 1969): First-order logic admits the 0-1 law<br /><br />Most finite model theorists equate the admission of 0-1 law with the inability to do "counting". Consider the following properties EVEN = { G : G has even number of vertices }. We see that μ<sub>n</sub>(EVEN) = 1 iff n is even, and hence μ(EVEN) does not exist. I am yet to see a property whose asymptotic probability μ converges to something other than 0 or 1, or diverges, but has nothing to do with counting. Consider the following properties:<br /><ol><br /> <li> μ(BIPARTITE) = 0<br /> <li> μ(HAMILTONIAN) = 1<br /> <li> μ(CONNECTED) = 1<br /> <li> μ(TREE) = 0<br /></ol><br />On the other hand, if you admit constant or function symbols, it is possible to have first-order properties whose asymptotic probability converges to something other than 0 or 1. So, it is crucial to assume that our vocabulary σ be purely relational.<br /><br />What is the use of 0-1 law in finite model theory apart from the amusement of some theoreticians? [I will have to confess many proofs about the 0-1 law, including Fagin's proof of the above theorem, are usually of great beauty.] Well, a primary concern of finite model theory is to determine how expressive a logic is over a given class of finite structures. By proving that a logic admits the 0-1 law, we show that <strong>any</strong> property whose asymptotic probability does not converge to either 0 or 1 is not expressible in the logic. For example, an immediate corollary of the above theorem is that first-order logic cannot express EVEN.<br /><br />Let me briefly outline the proof ideas of the above theorem which recurs in 0-1 law proofs. We only need to show that, for each natural number k, there exists a property P<sub>k</sub> of graphs such that<br /><ol><br /> <li> μ(P<sub>k</sub>) = 1, and<br /> <li> Any two models of P<sub>k</sub> cannot be distinguished by a first-order sentence of quantifier rank k. [Recall that the quantifier rank of a first-order sentence is the maximum depth of any nesting of quantifiers of the sentence.]<br /></ol><br />Why is this sufficient? Let f be a first-order sentence of quantifier rank k. There are two cases. First, there exists a model of P<sub>k</sub> that is also a model of f. In this case, it is not hard to show that <em>any</em> model of P<sub>k</sub> is also a model of f, which implies that μ(f) ≥ μ(P<sub>k</sub>) = 1. The second case is that all models of P<sub>k</sub> are not models of f, i.e., they are models of "not f". Therefore, μ("not f") ≥ μ(P<sub>k</sub>) = 1. That is, we have μ(f) = 0.<br /><br />The property P<sub>k</sub> is commonly referred to as an <i>extension axiom</i>. Note that P<sub>k</sub> does not have to be L-definable (where L is the logic that is to admit 0-1 law). <br /><br />Two excellent expositions of the basics of 0-1 laws include Leonid Libkin's Elements of Finite Model Theory chapter 12, and James Lynch DIMACS 1995-1996 Tutorial notes on "Random Finite Models".anthonywlinhttp://www.blogger.com/profile/07618509800342861247noreply@blogger.com5tag:blogger.com,1999:blog-12932458.post-1136683265066894152006-01-07T20:08:00.000-05:002006-01-07T20:29:30.843-05:00Starting the year 2006Sorry for having been silent for quite a while. This winter "break" turned out to be quite a busy one for me, with quite a bit of homework and research to do. Anyway, belated happy new year! I hope that this will be a great and productive year for all of us.<br /><br />I just resumed reading the lattest on the blogsphere, with still quite a bit of catching up to do. For now, I will mention mention a couple of noteworthy things that happened:<br /><ol><br /> <li> <a href="http://www.antimeta.org/blog/">Kenny Easwaran</a> wrote an <a href="http://www.antimeta.org/blog/archives/2005/12/forcing.html">introductory article</a> on "forcing", a well-known technique in set theory for proving independence results. I will write more on it when I finish reading the article.<br /> <li> <a href="http://www.cs.toronto.edu/~igor">Igor Naverniouk</a>, a PhD student from University of Toronto, just started a new blog on True Artificial Intelligence. The first couple of entries look quite interesting.<br /></ol>anthonywlinhttp://www.blogger.com/profile/07618509800342861247noreply@blogger.com0