For the most recent entries see the Petri Nets Newsletter.

A Sweep-Line Method for State Space Exploration.

Christensen, Søren; Kristensen, Lars Michael; Mailund, Thomas

Abstract: 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.

Do you need a refined search? Try our search engine which allows complex field-based queries.

Back to the Petri Nets Bibliography