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