Symbolic Traversal of Finite State Machines

Question 1

Definition of Existential Quantification:

Answer 1

Let f be a Boolean function. The disjunction of the cofactors of f with respect to (w.r.t.) x is called existential quantification of f w.r.t. x:
∃xf = f|x=1 + f|x=0

Question 2

What is symbolic model checking?

Answer 2

Use boolean variable to represent sets and relation of states to avoid state explosion.

Question 3

Explain the steps of Image computation.

Answer 3

• Create the characteristic function of the states Cs(s).
• Create the transition function T(s,x,s’) based on the state transition function δ(s,x) and the states.
• Calculate the existential of the state variables and existential of the input variables.

Question 4

How can we calculate invariants based on inverse reachability analysis? Relation between W and Q.

Answer 4

Start with states Z0 and compute all states Q, from which the states Z0 can be
reached. Q and W are complement of each other.

Question 5

Which model is used in bounded model checking??

Answer 5

Iterative circuit model.