Unfolding Based Algorithms for the Reachability Problem

Issue title: Concurrency Specification and Programming (CS&P'2000)

Article type: Research Article

Authors: Esparza, Javier | Schröter, Claus

Affiliations: Technische Universität München, Arcisstrasse 21, 80333 München, Germany

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 O(n^k), where $n$ is the size of the prefix of the unfolding containing all reachable states, and $k$ 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.

Keywords:

Journal: Fundamenta Informaticae, vol. 47, no. 3-4, pp. 231-245, 2001