Loading
May 2001
Abstract:One of the major problems when applying model checkers to industrial-size system 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 real-life 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.
Available as compressed Postscript (219 kB), PDF (299 kB), and Postscript (624 kB)
Download BibTeX entry.