Narrowing Petri Net State Spaces Using the State Equation

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

Article type: Research Article

Authors: Schmidt, Karsten

Affiliations: Institut für Informatik, Humboldt-Universität zu Berlin, D-10099 Berlin, Germany

Abstract: Given a (possibly partially defined) state, all count vectors of transition sequences reaching that state are solutions to a corresponding Petri net state equation. We propose a search strategy where sequences corresponding to a minimal solution of the state equation are explored first. Then step by step the search space is relaxed to arbitrary count vectors. This heuristics relies on the observation that in many (though provably not in all) cases, minimal solutions of the state equation can be realized as a firing sequence. If no target state is reachable, either the state equation does not have solutions, or our search method would yield the full state space. 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.

Keywords: computer aided verification, Petri nets, reachability analysis, state equation

Journal: Fundamenta Informaticae, vol. 47, no. 3-4, pp. 325-335, 2001