Obtaining memory-efficient reachability graph representations using the sweep-line method

T. Mailund, M. Westergaard

    Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

    10 Citations (Scopus)


    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.
    Original languageEnglish
    Title of host publicationProceedings 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
    EditorsK. Jensen, A. Podelski
    Place of PublicationBerlin
    ISBN (Print)3-540-21299-X
    Publication statusPublished - 2004

    Publication series

    NameLecture Notes in Computer Science
    ISSN (Print)0302-9743


    Dive into the research topics of 'Obtaining memory-efficient reachability graph representations using the sweep-line method'. Together they form a unique fingerprint.

    Cite this