Deprecated: The each() function is deprecated. This message will be suppressed on further calls in /home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php on line 456
The magic of symbolic model checking: In symbolic model checking, instead of building a list of reachable states, a predicate forumla, q(s), is constructed that is true iff s is a reachable state. The magic key to the efficiently finding the allowable states during symbolic model checking can be explained as follows \E (a, b, c, ...) . R(q', a, b, c, ...) can be written as \E(b, c, ...) . \E a . R(q', a, b, c, ...) Therefore, instead of performing a search over the exponential set of values defined by the state tupple (a, b, c, ...) we can instead use a linear number of operations. Each operation removes a variable from s and we end up with an explicit expression for q'. However, we can go one better than that: the BDD implementation of `forsome' (the existential quantifier) can easily be implemented to accept a list of variables and to quantify over them all in one operation, and so even the `linear' part is somewhat ameliorated. In the above, R is the next state relation, q is the allowable states predicate and the prime denotes the value in the next state. The state itself, s, is the vector (a, b, c, ...). DJ Greaves.