Reference: J. Esparza and C. Schröter. Unfolding Based Algorithms for the Reachability Problem. Fundamenta Informaticae, 47(3,4):231–245, 2001. Abstract: We study four solutions to the reachability problem for 1-safe Petri nets, all of them based on the unfolding technique. We define the problem as follows: given a set of places of the net, determine if some reachable marking puts a token in all of them. Three of the solutions to the problem are taken from the literature (McM92,Mel98,Hel99), while the fourth one is first introduced here. The new solution shows that the problem can be solved in time , where is the size of the prefix of the unfolding containing all reachable states, and is the number of places which should hold a token. We compare all four solutions on a set of examples, and extract a recommendation on which algorithms should be used and which ones not. Suggested BibTeX entry: @article{ES01a,     author = {J. Esparza and C. Schr{\"o}ter},     journal = {Fundamenta Informaticae},     pages = {231--245},     publisher = {IOS Press},     title = {{Unfolding Based Algorithms for the Reachability Problem}},     volume = {47(3,4)},     year = {2001} }

GZipped PostScript (150 kB)