@inproceedings{
    Vrp94d,
    editor = "Czaja, Ludwik and Burkhard, Hans-Dieter and Starke, Peter H.",
    author = "Varpaaniemi, Kimmo",
    publisher = {Informatik-Bericht Nr. 36, Institut f{\"{u}}r Informatik, Humboldt-Universit{\"{a}}t zu Berlin, Germany},
    title = "{T}he Sleep Set Method Revisited",
    booktitle = "{W}orkshop: {C}oncurrency, Specification \& Programming, {O}ctober 12--15, 1994",
    ps = "kvacsp94.ps",
    errata = "http://users.tkk.fi/~kvarpaan/kvacsp94e.html",
    flags = "public",
    year = "1994",
    keywords = "labelled transition systems, reachability analysis, local state properties, infinite transition sequences, stubborn set method, sleep set method",
    pdf = "kvacsp94.pdf",
    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."
}