A Sweep-Line Method for State Space Exploration

Research output: Contribution to book/anthology/report/proceedingArticle in proceedingsResearchpeer-review

  • Søren Christensen
  • Lars Michael Kristensen, Denmark
  • Thomas Mailund, Denmark
  • Tiziana Margaria, Denmark
  • Wang Yi, Denmark
  • Department of Computer Science
We present a state space exploration method for on-the-fly verification. The method is aimed at systems for which it is possible to define a measure of progress based on the states of the system. The measure of progress makes it possible to delete certain states on-the-fly during state space generation, since these states can never be reached again. This in turn reduces the memory used for state space storage during the task of verification. Examples of progress measures are sequence numbers in communication protocols and time in certain models with time. We illustrate the application of the method on a number of Coloured Petri Net models, and give a first evaluation of its practicality by means of an implementation based on the Design/CPN state space tool. Our experiments show significant reductions in both space and time used during state space exploration. The method is not specific to Coloured Petri Nets but applicable to a wide range of modelling languages.
Original languageEnglish
Title of host publicationLecture Notes in Computer Science
Number of pages15
Publication year2001
EditionLecture Notes in Computer Science 2031
ISBN (print)978-3-540-41865-8
Publication statusPublished - 2001
EventTools and Algorithms for the Construction and Analysis of Systems (TACAS 2001) - Genova, Italy
Duration: 2 Apr 20016 Apr 2001
Conference number: 7


ConferenceTools and Algorithms for the Construction and Analysis of Systems (TACAS 2001)

See relations at Aarhus University Citationformats

ID: 281183