In: Burkhard, H.-D.; Czaja, L.; Skowron, A.; Starke, P.: Report No. 140: Proceedings of the workhop on Concurrency, Specification and Programming, Oct 9-11, 2000, pages 243-253. Berlin: Humboldt-University, 2000.
Abstract: Given a (possibly partially defined) state, all firing count vectors that correspond to sequences reaching that state are solutions to a corresponding Petri net state equation. We propose a search strategy that first explores sequences corresponding to a minimal solution of the state equation and then step by step relaxes the search space to other solutions of the equation. This heuristics relies on the observation that in many cases a shortest sequence reaching a state corresponds to a minimal solution of the state equation. Should the target state be non-reachable, our algorithm usually does not reduce the state space at all. We study the impact of the state equation on reachability, present an algorithm that exploits information from the state equation and discuss its application in stateless search as well as its combination with stubborn set reduction.