2013/04/10 by Julian Rathke, Rathke, Julian, Paweł Sobociński +3
Business, Management and Accounting · Computer Science · #Business Process Modeling and Analysis #D.2.2 #F.1.1 #F.3.2 #FOS: Computer and information sciences #Formal Methods in Verification #Logic in Computer Science (cs.LO) #Petri Nets in System Modeling
paper · pdf · doi:10.48550/arxiv.1304.3121
openalex publication_date 2013/04/10 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
In recent work, the second and third authors introduced a technique for reachability checking in 1-bounded Petri nets, based on wiring decompositions, which are expressions in a fragment of the compositional algebra of nets with boundaries. Here we extend the technique to the full algebra and introduce the related structural property of decomposition width on directed hypergraphs. Small decomposition width is necessary for the applicability of the reachability checking algorithm. We give examples of families of nets with constant decomposition width and develop the underlying theory of decompositions.