Model Checking Dynamic States in GROOVE

H. Kastenberg, Arend Rensink

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

    78 Citations (Scopus)
    1 Downloads (Pure)


    Much research has been done in the field of model-checking complex systems (either hardware or software). Approaches that use explicit state modelling mostly use bit vectors to represent the states of such systems. Unfortunately, that kind of representation does not extend smoothly to systems in which the states contain values from a domain other than primitive types, such as reference values commonly used in object-oriented systems. In this paper we report preliminary results on applying CTL model checking on state spaces generated using graph transformations. The states of such state spaces have an internal graph structure which makes it possible to represent complex system states without the need to know the exact structure beforehand as when using bit vectors.
    Original languageUndefined
    Title of host publicationModel Checking Software (SPIN)
    EditorsA. Valmari
    Place of PublicationBerlin
    Number of pages7
    ISBN (Print)3-540-33102-6
    Publication statusPublished - 2006
    EventModel Checking Software (SPIN) - Vienna, Austria
    Duration: 30 Mar 20061 Apr 2006

    Publication series

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


    ConferenceModel Checking Software (SPIN)
    Other30 Mar - 1 Apr 2006


    • IR-62876
    • EWI-2793
    • METIS-238019

    Cite this