Model-checking on infinite transition systems

"Program testing can be used to show the presence of bugs, but never to show their absence!", said Edsger Dijkstra. Model-checking 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. Kripke Structures) 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 monadic second-order logic (MSO) as

1. It subsumes most modal logics that we use in verification including all the afore-mentioned logics, and
   
2. MSO is a well-behaved and well-studied logic.
   

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.

I will talk about one simple kind of infinite transition systems that goes by the name of pushdown graphs. A pushdown graph is nothing but the transition graph of a pushdown automaton. Here, a pushdown automaton is a tuple (Q,A,Γ, q₀, Z₀, Δ), where Q is a finite set of states, A the input alphabet, Γ the stack alphabet, Z₀ ∈ Γ the initial stack symbol, and the transition relation Δ is a finite subset of Q x A x Γ x Γ^* 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₀. Now a pushdown graph for this automaton is the infinite graph G = (V,(E_a)_{a ∈ A}) where:

• V is the set of configurations of the automaton (i.e. words from QΓ^*, a product of the current state and the stack configurations) that are reachable from q₀Z₀ by a finite number of applications of Δ,
  
• E_a is the set of all pairs (qvw,q'αw) from V² for which there is a transition (q,a,v,α,q').
  

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

W. Thomas. Constructing Infinite Graphs with a Decidable MSO-theory

for a nice presentation of this proof.

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:

REACH(x,x') ≡ ∀ X( x∈X and ∀y,z( y∈X and E(y,z) --> z∈X) --> x'∈X)

As usual, E(x,y) is an abbreviation for "OR_{a ∈ A} 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.