Symbolic model checking

structure is not specified explicitly

defined in a symbolic way:

• set of variables
• their initial values
• how they change over time

Computational tree logic (CTL)

similar to LTL, but:

allows conditions over traces

evaluation directly on structures, not on a single trace

Examples

AFx

in all traces, x will be true at some point

EGx

in at least a trace, x is true and stays so

Evaluation

statements over traces ⇒ cannot evaluate on a single trace

evaluation is on a whole structure

ex: AFx true in s if:

• for all traces [s₀, s₁,…] in the structure where s₀=s
• there exists a state s_i
• such that x is true in s_i

Constraint

A or E only applied to formulae whose main connective is X, F, G and U

disallowed, for example: Xa, A(x∨y)

NuSMV

the structure is defined in terms of variables

• their initial value
• how they change

next: example (stoppable clock)

NuSMV: example

a clock: out goes to true to false and back at every step

input run starts and stops (freezes out) it

NuSMV: code

MODULE main
VAR
  run: boolean;
  out: boolean;
ASSIGN
  init(run) := FALSE;
-- no next(run), so run can now take arbitrary values;
-- init necessary so that E = exists input sequence
-- (check is in every initial state)

  init(out) := FALSE;
  next(out) :=
    case
      !run: out;
      TRUE: !out;
    esac;

SPEC
  AG (!run | AF out)
SPEC
  EG (!out)
SPEC
  AG (!out)

NuSMV: output

*** This is NuSMV 2.5.4 ...

-- specification AG (!run | AF out)  is true
-- specification EG !out  is true
-- specification AG !out  is false
-- as demonstrated by the following execution sequence
Trace Description: CTL Counterexample 
Trace Type: Counterexample 
-> State: 1.1 <-
  run = FALSE
  out = FALSE
-> State: 1.2 <-
  run = TRUE
-> State: 1.3 <-
  run = FALSE
  out = TRUE

Exponential set of states

with n boolean variables, 2ⁿ states

explicit labeling impossible

use an OBDD to represent the set of states where a subformula is true

Bounded model checking

alternative solution

employs a sat solver