Title: The Sleep Set Method Revisited

Appears in: Czaja, L., Burkhard, H.-D., and Starke, P.H. (Eds.), Proceedings of the 3rd International Workshop on Concurrency, Specification, and Programming, Berlin, October 1994. Humboldt Universität zu Berlin, Institut für Informatik, Informatik-Bericht 36, Berlin 1994.

10 pages

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.