Reducing Memory Usage in Symbolic State-Space Exploration for Timed Systems
Johan E. Bengtsson · 2001
One of the major problems to scale up model checking techniques to the size of industrial systems is the large memory consumption. This report address the problem in the context of verifiers for timed systems and present a number of techniques that reduce the amount memory used for state space exploration in such a tool. The methods are evaluated and compared by reallife examples and their strengths and weaknesses are described. In particular we adress the memory consumption problem on two fronts, first by reducing the size of each symbolic state by means of compression and second by reducing the size of the stored state space by early inclusion checking and probabilistic methods.