From Propositional SAT to CTL Properties on Transition Systems

One of the most fundamental questions we can ask in logic is that of satisfiability: given a logical formula, is there an assignment of the formula's variables under which the formula evaluates to true? It's one of the first problems any student of formal logic will encounter after being introduced to propositional logic, but it has deep and interesting consequences in several areas of Computer Science.

One thing that I find particularly interesting is that we can use propositional satisfiability (or SAT) to answer questions about formulas from other, seemingly more complicated logics: in this case, Computation Tree Logic (CTL).

CTL

CTL is a logic commonly used for specifying properties of systems to be checked with formal verification techniques. In this case, I'm going to talk about checking properties of this transition system:

-> !TS <-

The CTL property we want to check that this system satisfies is going to be {% m %}\forall \square (p \vee q){% em %}. I'll explain what that formula is saying:

CTL is a logic for describing states, and the paths that branch from them. The {% m %}\forall{% em %} above specifies that what follows should apply to all paths beginning at the current state. The {% m %}\square{% em %} means 'globally', or 'at every state' (you'll see different symbols used for CTL in other sources -- this symbol is often written as G). This specifies that every state in a sequence should satisfy some property. Then, finally, {% m %}(p \vee q){% em %} specifies that either {% m %}p{% em %} or {% m %}q{% em %} should hold at a particular state.

So the whole formula, {% m %}\forall \square (p \vee q){% em %}, states that for all paths from the initial state {% m %}s0{% em %}, _at every point on the path, either {% m %}p{% em %} or {% m %}q{% em %} holds.

It's clear that the property doesn't hold for the above transition system (for example, a path beginning {% m %}s0s1s3{% em %} doesn't satisfy the property, as neither {% m %}p{% em %} nor {% m %}q{% em %} holds in {% m %}s3{% em %}). But with more complicated systems and more complicated properties, we don't have to have to rely on finding counter-examples by hand.

Bounded model checking

There are loads of good ways to check CTL properties like this, and I'm just going to talk about one called bounded model checking.

The cool thing about this is that we can reduce the complicated problem of verifying a CTL property against a transition system to a much-studied and well-understood problem: SAT. Although SAT is NP-complete, there have been advances in the past decade or so which have led to very efficient SAT-solvers in many cases.

The first thing we need to do is translate our problem to the language of propositional logic. First, we can represent the states of our transition system using propositional variables {% m %}x1, x2{% em %}:

{% math %} \begin{array}[c | c | c] \text{state} & x1 & x2 \ \hline s0 & 1 & 1 \ s1 & 1 & 0 \ s2 & 0 & 1 \ s3 & 0 & 0 \end{array} {% endmath %}

We can then represent the transition relation {% m %}[\rightarrow]{% em %} as follows:

{% math %} \begin{align} & (x_1 \wedge x_2 \wedge x_1' \wedge \neg x_2') \vee & (s_0 \rightarrow s_1) \ & (x_1 \wedge x_2 \wedge \neg x_1' \wedge x_2') \vee & (s_0 \rightarrow s_2) \ & (x_1 \wedge \neg x_2 \wedge \neg x_1' \wedge \neg x_2') \vee & (s_1 \rightarrow s_3) \ & (\neg x_1 \wedge x_2 \wedge \neg x_1' \wedge \neg x_2') \vee & (s_2 \rightarrow s_3) \ & (\neg x_1 \wedge \neg x_2 \wedge \neg x_1' \wedge x_2') \vee & (s_3 \rightarrow s_2) \ & (\neg x_1 \wedge \neg x_2 \wedge x_1' \wedge \neg x_2') & (s_3 \rightarrow s_1) \end{align} {% endmath %}

The above propositional formula will be satisfied by precisely those assignments representing a valid transition in our transition system.

Now we can describe the set of initial states as a propositional formula {% m %}[I]{% em %} (which is easy, as there is only one initial state):

{% math %} x1 \wedge x2
{% endmath %}

Now we're starting to be in a position to make meaningful formulas that tell us things about our transition system. For example, consider the formula {% m %}[\rightarrow] \wedge [I]{% em %}. If we run a SAT-solver on this and look at the values assigned to {% m %}x1'{% em %} and {% m %}x2'{% em %} in satisfying assignments, this will tell us precisely those states that can be reached in a single transition from the initial state.

Now let's try evaluating our property from earlier against the transition system. Let's try creating a boolean formula representing a counterexample for the property of length 1. If it's satisfiable, then the property doesn't hold for the transition. If not, we'll try again for counterexamples of length 2, and so on.

So, what would a counter-example of length 1 look like? Since any path must begin at an initial state, this would just consist of an inital state at which neither {% m %}p{% em %} nor {% m %}q{% em %} holds. The only state where neither {% m %}p{% em %} nor {% m %}q{% em %} holds is {% m %}s_3{% em %}, so we can express counterexamples of length 1 as:

{% math %} [I] \wedge \neg x1 \wedge \neg x2 = x1 \wedge x2 \wedge \neg x1 \wedge \neg x2 {% endmath %}

As a SAT-solver would tell you (or you can see easily for yourself), this is not satisfiable, so there are no counter-examples of length 1.

Now let's think about what a counter-example of length 2 would look like. It would have to start in an initial state, with one transition, with either the first state or the second state being {% m %}s_3{% em %}:

{% math %} [I] \wedge [\rightarrow] \wedge ((\neg x1 \wedge \neg x2)\vee(\neg x1' \wedge \neg x2')) {% endmath %}

This is also unsatisfiable, so now let's look at potential counter-examples of length 3! Now we need two transitions, and we have three states to potentially fail the property:

{% math %} \begin{align} &[I][x^0_0/x_0][x^0_1/x_1] \wedge \ &[\rightarrow][x^0_0/x_0][x^0_1/x_1][x^1_0/x_0'][x^1_1/x_1'] \wedge \ &[\rightarrow][x^1_0/x_0][x^1_1/x_1][x^2_0/x_0'][x^2_1/x_1'] \wedge \ &((\neg x^0_1 \wedge \neg x^0_2)\vee(\neg x^1_1 \wedge \neg x^1_2)\vee(\neg x^2_1 \wedge \neg x^2_2)) \end{align} {% endmath %}

(In the above formula, we have three copies of our propositional variables, one for each of the states in our potential counter-example. So the values of {% m %}x^00{% em %} and {% m %}x^01{% em %} will give us the first (initial) state, the values of {% m %}x^10{% em %} and {% m %}x^11{% em %} will tell us the second state, and so on -- with corresponding copies of the transition relation formula).

This time, the formula is satisfiable. For example, by the assignment:
{% math %} \begin{align} &x^0_0 = 1,\ x^0_1 = 1\ &x^1_0 = 1,\ x^1_1 = 0\ &x^2_0 = 0,\ x^2_1 = 0\ \end{align} {% endmath %}

This corresponds to the path {% m %}s0s1s3{% em %}, which is a counter-example as {% m %}p \vee q{% em %} doesn't hold in {% m %}s3{% em %}.

And that's an example of bounded model checking of CTL using propositional SAT!

There's a lot more to this topic than toy examples like this, but when I learned about this kind of thing I was impressed that such a basic problem as satisfiability of propositional formulas could be applied so directly and usefully to more elaborate problems like CTL problem checking. SAT is a deep problem, and there are loads more interesting uses for it out there if you look for them!