Optimized symbolic model checking for component-based systems

Symbolic model checking with BDDs is a very effective model checking technique, which can prove (or disprove) the existence of a counterexample by the symbolic computation of reachable states sets of systems. However, the memory and time are consumed seriously by the symbolic computations for component-based systems. The BDD-based symbolic model checking for component-based systems is considered in this paper. Firstly, a method of partitioned transition relation is given. Then an algorithm is proposed to partition the variables of transitions into separate value-changed and value-unchanged sets. The memory can be reduced and the runtime is also improved and verified by some experiments.