Patent ID: 7606774

Claim:
A symbolic model checking method of determining the reliability of a transition system described by the tuple (V, I(V), T(V old , V new ), E(V)), where V represents the set of state variables, I(V) is a formula describing the set of initial states, T(V old , V new ) is a formula describing the transition relation between the old values V old and new values V new of the variables in V, and E(V) is a formula describing the set of error states, wherein the formulas I(V) and T(V old , V new ) do not admit existential quantification, the method comprising the steps of: a. computing the set of reachable states CR(V) iteratively from an initial state CR 0 (V)≡I(V), and an i th state CR i (V)≡CR i−1 (V) ( V old : CR i−1 (V old ) T(V old , V)) for i>0, where the expression ( V old : CR i−1 (V old ) T(V old , V)) represents a set of steps that can be reached in one step from the set of steps that can be reached in i−1 steps, and where the i th state CR i (V) is an approximation of the i th state R i−1 (V) (∃V old : R i−1 (V old ) T(V old , V)) for i>0 if the formulas I(V) and T(V old , V new ) admitted existential quantifier elimination; b. determining all sets of error states E(V); c. determining the reliability of the transition system by whether there is an intersection between the reachable states determined in said step (a) and the error states determined in said step (b); and d. reporting the reliability determined in said step (c).