Study, Research and Note: Model Checking Evolution

Explicit-State Model Checking (EMC)

State space can be viewed as graph
Exhaustively enumerates all states of the system and traverses each edge of the graph
Problem
- Huge state space and difficult to enumerate all (computer capability CPU and memory consumption)
Depth-First Search or Breadth-First Search
- BFS: the shortest counterexample available
- BFS: more memory required since it needs to store back-pointers to predecessor state
States: 10^5

Manipulate set of states and transitions, rather than individual state and transition
Set of states and transitions is represented Boolean formula (boolean encoding)
BDD: boolean formula as Binary Decision Diagram

describes how to determine a Boolean value output based on some logical calculation from Boolean inputs
for a set A, each element of f(A) is called a Boolean function generated by A.
each boolean function is a unique representation
for example, for two binary variables (x and y), it has (2^2^(card(A)) = 16) boolean function. Here f1 = x AND y, and f2 = x OR y

x | y | f1 | f2 | …
0 | 0 | 0 | 0 | …
0 | 1 | 0 | 1 | …
1 | 0 | 0 | 1 | …
1 | 1 | 1 | 1 | …

Each element in the set of states is encoded as bit-string
- for a variable vector V={v1,v2,…vn}. A bit-string can represent 2^n states. For example, if n = 3, the set of states can be {000, 001, 010, 011, 100, 101, 110, 11}. Here bit-string 000 is a representation of bits vector {v1=0,v2=0,v3=0}.
Characteristic boolean function
- represents a subset of states which makes the function is true.
- for instance, if characteristic function is v1 AND v2, it means v1 and v2 should be both true. So the set will be {110,111}.
Current state of a vector of variable is symbolised as a bit-string
Transition is a state pair (s,s’), a combined bit-string
States: 10^100
SMV: Symbolic Model Verifier

Bounded in user-supplied time k
For transition system M, temporal logic formula f, construct a propositional formula Omega(k) that is satisfiable if f is valid along the path of length k
Path of length k is expressed as: I(s0) AND R(s0,s1) AND R(s1,s2) … AND R(sk-1, sk)
For example, if k = 2, and f = EF p, then Omega(2)=I(s0) AND R(s0,s1) AND R(s1,s2) AND (p0 OR p1 OR p2), which means from initial states, after up to 2 steps (transition), at least one p is true (exactly the same meaning as EF - exists a path finally p holds)
- not Omega(2) = I(s0) AND R(s0,s1) AND R(s1,s2) AND (not p0 AND not p1 AND not p2) - counterexample, all p does not hold.
For example, if k = 2, and f = AG p, then Omega(2)=I(s0) AND R(s0,s1) AND R(s1,s2) AND (p0 AND p1 AND p2), which means from initial states, after up to 2 steps (transition), each p is true (exactly the same meaning as AG - for all paths p always holds)
- not Omega(2) = I(s0) AND R(s0,s1) AND R(s1,s2) AND (not p0 OR not p1 OR not p2) - counterexample, at least one p does not hold.
- Safety-checking becomes not Omega(k) is not satisfiable. If it is satisfied, a satisfying assignment is given and that is the counterexample.
Using SAT
States: 10^1000

given a propositional formula, find if there exists an assignment to Boolean variables that make the formula true.
- for example, two boolean variables x and y. Formula p = not x AND not y. To make p true, A={x=0,y=0} is the only SATisfying assignment.

SAT solvers do not require exponential space and large designs can be checked very fast. BDDs based model checking uses DFS or BFS which does require a large memory.