7July_22_2008 Symbolic Model Checking without BDDs
http://citeseer.ist.psu.edu/155235.html
abstract
 stalmarck method or davis and putnam can replace BDDs to avoid blowup and generate counter-examples
 bounded model checking for LTL reduces to propositional satisfiability
 bounded LTL model checking w/o table construction
 implemented BMC model checker
1. INTRODUCTION
 m.c. finds subtle errors in designs
 compared to theorem proving it is automatic for the most part
 temporal logic specification
 system as FSM
 symbolic model checking w/ boolean encoding of FSM > 10^20 states
 BDDs-can handle system w/ hundreds of vars but can get too big too fast
 SAT operates on boolean expression
    no canonical forms, no blow up
 SAT procedure
  counter-example length k
 bound is maximal length of counter-example
 bounded model checking LTL reduce to propositional satisfiability in poly time
advantages
 1. bounded model checking counter-example is fast due to depth first nature
 2. counter-example of minimal length
 3. bounded model checking less space than BDD
 4. no manually selected vars
uses BMC tool

2.EXAMPLE
 machine M w/ 3 bit shifter, predicate T(x,x') as transition

LTL F(x=0) AF(x=0) => EG(x!=0) so look for G(x!=0), restrict to paths of length k+1 states
unroll the transition, need loops so x2 loops back to x1 or x0 or itself

then the formulas

Li is T(x2,xi) equivalent to

So to make sure G(x!=0), Si defined as xi!=0 must hold at each state

(those are = signs), one of the positions of the xi must be 1 for each i.
altogether:

is satisfiable iff counter-ex of length 2 for F(x=0)
in this example set xi[j] = 1 for all  i,j=0,1,2 is a satisfying assignment

3. SEMANTICS     
ACTL* is CTL NNF w/ only universal path quantifier
ECTL* is CTL NNF w/ only existential path quantifier
LTL has no E or A, is used in this paper, but could extend to ACTL* or ECTL*

Kripke structure M(S,I,T,l) states, initial states, transitions and labels l.
use Kripke structure to ge semantics of the logic--restricted to those with boolean encoding S={0,1}^n
 thus each state represented as a vector of state variables s=(s(1),...,s(n)), s(i) are propositional vars.
propositional formulas fI(s),fT(s,t) and fP(s). fI(s) iff s in I, fT(s,t) iff (s,t) in T, fP(s) iff p in l(s)
 pi(s0,s1,...) define pi(i)=si and pi^i=(si,si+1,...)  infinite sequence of states pi is a path if pi(i)->pi(i+1)
LTL valid universally
 existental model checking, universal model checking
bounded modeling checking considers only a finite prefix of a path (might still be infinite if back loop to previous states)
...(more not summarized)

4. TRANSLATION
reduce bounded model checking to propositional satisfiability => use efficient propositional decision procedures to do model checking
K.S. M, LTL f and bound k, [| M,f |]k.
...(more not summarized)

5. DETERMINING THE BOUND
section 3 proved unbounded semantics same as looking at bounded w/ all possible bounds,
LTL model checking procedure
set k and look for witness of length k M |= k EF, if not M|= Ef, increment k indefinitely, so here we bound k

diameter of M minimal number d  such that if v is reachable from a state u, then v is reachable from u in length d or less.

recurrence diameter minimal number d, then there is  d+1 loops back to a j<=d

LTL is PSPACE-complete.
bounded LTL reduces to propositional sat, thus NP.

...

6. EXPERIMENTAL RESULTS
BMC used SMV lang outpus SMV program or propositional formula
SATO(DP) uses DIMACS format
here use input format of PROVE(stalmarck)
BDDs poor performance
CMU model checker SMV
barrel shifter

7. CONCLUSION
sat symbolic m.c.
believe it can handle larger designs
need new techniques to determine diameter of a system

...