University of Twente Student Theses


Compressed Set Representations and their Effectiveness in Probabilistic Model Checking

Vegt, M. E. M. van der (2019) Compressed Set Representations and their Effectiveness in Probabilistic Model Checking.

[img] PDF
Abstract:Model checking is a technique employed in many areas such as the design of safety critical systems. Designers of such systems can construct models, which can give insight into the behavior of the system when verified by using model checking algorithms. One type of information that could be gained is reachability information (Will the system ever fail?). Model checking does not come without any challenges however: The state space explosion is a well-known phenomenon that plagues many techniques such as model checking. This means that so called exhaustive model checking algorithms have to keep track of very large amounts of states. Most of these algorithms use sets of these states, which can take up a significant amount of memory. This research investigates the effectiveness of using compressed representations of sets in reducing the amount of memory required by these algorithms, and their impact on performance. We find that these set representations are capable of reducing the memory usage of the model checking algorithms by 74% on average, though at quite a high performance hit. Due to the relatively small impact of bit sets on the total memory usage of model checking, these alternative set representations may have limited applicability.
Item Type:Essay (Bachelor)
Faculty:EEMCS: Electrical Engineering, Mathematics and Computer Science
Subject:54 computer science
Programme:Computer Science BSc (56964)
Keywords:Model checking, Memory usage, Bit set, Compression
Link to this item:
Export this item as:BibTeX
HTML Citation
Reference Manager


Repository Staff Only: item control page