When does Bob deserve to be a co-author?

I have recently been reading Bill Gasarch's post 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 advice that is more oriented towards faculty-student type of collaborations, but is perhaps also suitable in general. Check this link. Interestingly, it was a document written by Department of City and Regional Planning, University of Berkeley ...

Highland workshop on XML, Logic, and Automata

I'll be attending Highlands Workshop 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 Grantown-on-spey. I'm just hoping that they have a grocery store :) I will give a presentation on recurrent reachability in regular model checking based on this paper. Anyway, I'll post a summary of the workshop later on this week.

Rahul Santhanam has joined Edinburgh

Rahul Santhanam, Lance Fortnow's ex PhD student, has recently joined Edinburgh's School of Informatics. Warm welcome to him!

Finite-variable hierarchy conjecture

It seems that Ben Rossman 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 Anuj Dawar's survey. Ben has shown 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.

I believe this is the third big open problems that Ben has resolved in this decade. Go Ben!

Restructuring logicomp

I'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 new cool blog, and Luca Aceto has his blog. Ah ... also I'm having a lot of difficulty deciphering blogger's word verification mechanism.

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.

Pushdown systems: reachability via saturations

Finally, 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!

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 efficiently 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 for real. 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 here before you continue.

Roughly speaking, the reachability problem for pushdown systems asks the following question: given a pushdown system P and two configurations C₁ and C₂ of P, is it possible to reach C₂ from C₁ 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.

In here 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.

The idea of saturation construction is to construct a finite automaton A that recognizes the set of configurations that can reach C₂ and then check whether C₁ is in the language of A; recall that membership checking for finite automata is solvable in linear time. First, observe that C₂ is a single word and is obviously regular. We start with an automaton for C₂ and introduce several extra states, each corresponding to a state of the pushdown system P. Call this automaton A. We shall iteratively 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.

As far as I remember, the idea was first proposed in the paper by Bouajjani, Esparza, and Maler for pushdown systems:

Reachability analysis of pushdown automata: Application to model-checking. CONCUR 1997.

It seems that similar ideas were already proposed earlier for ground tree rewrite systems, a more general class of systems, in:

Coquide, Dauchet, and Gilleron. Bottom-up tree pushdown automata: classification and connection with rewrite systems. Theoretical Computer Science 127, 1994.

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.

Happy 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).

Without further ado, here are some plans for my posts for the next two to three weeks:

1. Some extensions of pushdown systems and how to do model checking on these structures. I covered the definitions of pushdown systems already in here, 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.


2. Well-structured transition systems. 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).