2020/06/09 by Thomas Hujsa, Bernard Berthomieu, Hujsa, Thomas +5
Biochemistry, Genetics and Molecular Biology · Business, Management and Accounting · Computer Science · #Business Process Modeling and Analysis #FOS: Computer and information sciences #Formal Methods in Verification #Gene Regulatory Network Analysis #Logic in Computer Science (cs.LO) #Petri Nets in System Modeling
paper · pdf · doi:10.48550/arxiv.2006.05600
openalex publication_date 2020/06/10 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
Although decidable, the marking reachability problem for Petri nets is well-known to be intractable in general, and a non-elementary lower bound has been recently uncovered. In order to alleviate this difficulty, various structural and behavioral restrictions have been considered, allowing to relate reachability to properties that are easier to check. For a given initial marking, the set of potentially reachable markings is described by the state equation solutions and over-approximates the set of reachable markings. In this paper, we delineate several subclasses of weighted Petri nets in which the set of reachable markings equals the set of potentially reachable ones, a property we call the PR-R equality. When fulfilled, this property allows to use linear algebra to answer the reachability questions, avoiding a brute-force analysis of the state space. Notably, we provide conditions under which this equality holds in classes much more expressive than marked graphs, adding places with several ingoing and outgoing transitions, which allows to model real applications with shared buffers. To achieve it, we investigate the relationship between liveness, reversibility, boundedness and potential reachability in Petri nets. We also show that this equality does not hold in classes with close modeling capability when the conditions are relaxed.