CTL model checker (CSP)

From LiteratePrograms

This article describes a simple Computational Tree Logic (CTL) model checker, written in the machine-readable version of CSP and intended to be evaluated using the Formal Systems Europe Ltd. FDR tool. See Huth and Ryan, "Logic in Computer Science" for details of the algorithm.

Note that this model-checker does not apply CTL formulas to CSP processes! It is a hack that tricks FDR into performing CTL model-checking of a user-defined finite state machine expressed as several different sets (not a labelled transition system, or a CSP process expression).

Contents 1 Inputs 1.1 Refinement assertions 2 Implementation 2.1 Temporal operators 2.2 Auxiliary functions 2.3 Complete script

Inputs

The model-checker takes as input a finite state machine expressed as sets of states, possible transitions between, and labels consisting of atomic propositions that are true in each state. For example, the finite state machine shown in the figure to the right can be represented as the sets:

<<inputs>>=
const_MaxState = 10
datatype STATE = S.{0..const_MaxState}
-- A set of states
States = { S.0, S.1, S.2, S.3 }
-- A set of transitions
Trans = { (S.0, S.2), 
          (S.0, S.3),
          (S.1, S.0),
          (S.2, S.3),
          (S.3, S.0),
          (S.3, S.1) }
-- A labeling function
Labels = { (S.0, {Atom.A, Atom.C}),
           (S.1, {Atom.C}),
           (S.2, {Atom.A, Atom.B}),
           (S.3, {Atom.B}) }

CTL formulas are expressed using a datatype that provides an abstract syntax for combining atomic propositions using various logical and temporal operators:

<<ctl syntax>>=
datatype ATOM = A | B | C | D
datatype CTL_FORMULA 
    = Top
    | Bottom
    | Atom.ATOM
    | Not.CTL_FORMULA    
    | And.(CTL_FORMULA, CTL_FORMULA)
    | Or.(CTL_FORMULA, CTL_FORMULA)
    | Implic.(CTL_FORMULA, CTL_FORMULA)
    | AX.CTL_FORMULA
    | EX.CTL_FORMULA
    | AU.(CTL_FORMULA, CTL_FORMULA)
    | EU.(CTL_FORMULA, CTL_FORMULA)
    | EF.CTL_FORMULA
    | EG.CTL_FORMULA
    | AF.CTL_FORMULA
    | AG.CTL_FORMULA

Here are a few examples of CTL formulas expressed using the syntax defined above:

<<example ctl formulas>>=
Spec1 = EX.Atom.B
Spec2 = EU.(And.(Atom.A, Atom.B), Atom.C)
Spec3 = AF.Not.Atom.C
Spec4 = EX.Atom.C
Spec5 = AU.(Atom.C, And.(Atom.A, Atom.B))

Refinement assertions

FDR requires some kind of assertion about a process to be made in order to trigger the evaluation of a function. In the case of this script, evaluation of the model-checking function is triggered by performing a trace refinement (i.e language containment) check to see if the distinguished initial state (S.0 by convention) is a member of the set of states returned by the model-checking function. If the initial state is in the returned set of states then the model satisifes the spec, and the corresponding FDR assertion will succeed.

<<example refinement checks>>=
channel state: STATE
SAT_States1 = SAT(Spec1)
assert state?s:SAT_States1 -> STOP [T= state!S.0 -> STOP 
SAT_States2 = SAT(Spec2)
assert state?s:SAT_States2 -> STOP [T= state!S.0 -> STOP 
SAT_States3 = SAT(Spec3)
assert state?s:SAT_States3 -> STOP [T= state!S.0 -> STOP 
SAT_States4 = SAT(Spec4)
assert not state?s:SAT_States4 -> STOP [T= state!S.0 -> STOP
SAT_States5 = SAT(Spec5)
assert not state?s:SAT_States5 -> STOP [T= state!S.0 -> STOP

Implementation

The core of the model-checker is a boolean satisfaction algorithm that examines a CTL formula, and returns the set of states in the input finite state machine that satisfy the formula. We define the SAT function using a recursive pattern-match on the syntax of CTL formulas. The return value of the function is a set containing the states which satisfy the given CTL formula.

<<SAT>>=
SAT(Top) = States
SAT(Bottom) = {}
SAT(Atom.p) = { s | (s, L) <- Labels, member(Atom.p, L) }
SAT(Not.p) = diff(States, SAT(p))
SAT(And.(p, q)) = inter(SAT(p), SAT(q))
SAT(Or.(p, q)) = union(SAT(p), SAT(q))
SAT(Implic.(p, q)) = SAT(Or.(Not.p, q))
SAT(AX.p) = SAT(Not.EX.Not.p)
SAT(EX.p) = SAT_EX(p)
SAT(AU.(p, q)) = SAT(Not.Or.(EU.(Not.p, And.(Not.p, Not.q)), EG.Not.q))
SAT(EU.(p, q)) = SAT_EU(p, q)
SAT(EF.p) = SAT(EU.(Top, p))
SAT(EG.p) = SAT(Not.AF.Not.p)
SAT(AF.p) = SAT_AF(p)
SAT(AG.p) = SAT(Not.EF.Not.p)

Temporal operators

The definitions of the SAT function for the temporal operators EX, EU, and AF are a little more complex than those required for the other operators:

<<temporal operators>>=
SAT_EX(p) = 
    let
        X = SAT(p)
    within
        pre_E(X)
SAT_AF(p) = 
    let
        Y = SAT(p)
        f(X) = union(X, pre_A(X))
    within
        if Y == States
        then Y
        else Fixpoint(f, Y)
SAT_EU(p,q) = 
    let
        W = SAT(p)
        Y = SAT(q)
        f(X) = union(X, inter(W, pre_E(X)))
    within
        if Y == States
        then Y
        else Fixpoint(f, Y)

Auxiliary functions

The SAT_EX, SAT_AF and SAT_EU functions rely on three auxiliary functions. The first computes a "preimage" consisting of the set of all states that can transition to any state in the set X.

<<preimage E>>=
pre_E(X) = { s0 | (s0, s1) <- Trans, member(s1, X) }

The second auxiliary function computes a "preimage" consisting of the set of all states which transition to states in X, and do not transition to any state outside of X. This is easily expressed in terms of set differences and the pre_E function.

<<preimage A>>=
pre_A(X) = diff( pre_E(X), pre_E( diff(States, X) ) )

The third auxiliary function computes a fixpoint for the application of a function from sets of states to sets of states.

<<fixpoint>>=
Fixpoint(f, X) = 
    let
        X' = f(X)
    within
        if X == X'
        then X
        else Fixpoint(f, X')

Complete script

The complete CSP script combines the inputs, refinement checks, datatypes, and SAT functions into a single file, suitable for loading into FDR.

<<ctl_model_checker.csp>>=
inputs
example ctl formulas
example refinement checks
ctl syntax
SAT
temporal operators
preimage E
preimage A
fixpoint

Download code