Doctoral dissertation, Helsinki University of Technology, Department of Computer Science and Engineering, Digital Systems Laboratory, Research Report A51, 105 pages, May 1998.
Abstract: Reachability analysis is a powerful formal method for analysis of concurrent and distributed finite state systems. It suffers from the state space explosion problem, however, i.e. the state space of a system can be far too large to be completely generated. This thesis is concentrated on the application and theory of the stubborn set method which is one of the methods that try to relieve the state space explosion problem. A central topic in the thesis is the verification of nexttime-less LTL (linear time temporal logic) formulas. It is shown how the structure of a formula can be utilized when there is no fairness assumption. Another central topic is the basic problem how stubborn sets should be computed in order to get the best possible result w.r.t. the total time and space consumed in the state search. An algorithm for computing cardinality minimal or almost cardinality minimal (w.r.t. the number of enabled transitions) stubborn sets is presented, together with experiments that indicate that the algorithm is worth of consideration whenever one wants to get proper advantage of the stubborn set method. The thesis also considers how to cut down on space consumption in the stubborn set method and how well the method can be combined with another reduction technique, the sleep set method.
Keywords: reachability analysis; reduced state space generation; stubborn sets; verification of LTL formulas.