Without further ado, here are some plans for my posts for the next two to three weeks:
- 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.
- 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).