The Sleep Set Method Revisited

Reference:

Kimmo Varpaaniemi. The sleep set method revisited. In Ludwik Czaja, Hans-Dieter Burkhard, and Peter H. Starke, editors, Workshop: Concurrency, Specification & Programming, October 12–15, 1994. Informatik-Bericht Nr. 36, Institut für Informatik, Humboldt-Universität zu Berlin, Germany, 1994.

Abstract:

State space generation is a powerful formal method for analysis of concurrent and distributed finite state systems. It suffers from the state space explosion problem, however: the state space of a system can be far too large to be completely generated. The sleep set method is one way to try to avoid generating all of the state space when verifying a given property. This paper is concentrated on the transition selection function in the sleep set method applied to a labelled transition system to verify a simple safety property or the existence of enabled infinite transition sequences. The conditions found for the function can be used for combining the sleep set method with other analysis techniques.

Keywords:

labelled transition systems, reachability analysis, local state properties, infinite transition sequences, stubborn set method, sleep set method

Suggested BibTeX entry:

@inproceedings{VarpaaniemiKimmo-Vrp94d,
    author = {Kimmo Varpaaniemi},
    booktitle = {{W}orkshop: {C}oncurrency, Specification \& Programming, {O}ctober 12--15, 1994},
    editor = {Ludwik Czaja and Hans-Dieter Burkhard and Peter H. Starke},
    publisher = {Informatik-Bericht Nr. 36, Institut f{\"{u}}r Informatik, Humboldt-Universit{\"{a}}t zu Berlin, Germany},
    title = {{T}he Sleep Set Method Revisited},
    year = {1994},
}