This paper is concerned with a memory-efficient representation of reachability graphs. We describe a technique that enables us to represent each reachable marking in a number of bits close to the theoretical minimum needed for explicit state enumeration. The technique maps each state vector onto a number between zero and the number of reachable states and uses the sweep-line method to delete the state vectors themselves. A prototype of the proposed technique has been implemented and experimental results are reported.
Keywords: Verification; state space methods; state space reduction; memory efficient state representation; the sweep-line method.
|Title of host publication||Proceedings of the 10th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2004), Part of ETAPS 2004, 29 March - 2 April 2004, Barcelona, Spain|
|Editors||K. Jensen, A. Podelski|
|Place of Publication||Berlin|
|Publication status||Published - 2004|
|Name||Lecture Notes in Computer Science|