Automatic Decomposition of Petri Nets into Automata Networks - A Synthetic Account

Pierre Bouvier, Hubert Garavel, and Hernán Ponce de León

Proceedings of the 41st International Conference on Application and Theory of Petri Nets and Concurrency (PETRI NETS'20), Paris, France, June 2020

Abstract:

This article revisits the problem of decomposing a Petri net into a network of automata, a problem that has been around since the early 70s. We reformulate this problem as the transformation of an ordinary, one-safe Petri net into a flat, unit-safe NUPN (Nested-Unit Petri Net) and define a quality criterion based on the number of bits required for the structural encoding of markings. We propose various transformation methods, all of which we implemented in a tool chain that combines NUPN tools with third-party software, such as SAT solvers, SMT solvers, and tools for graph colouring and finding maximal cliques. We perform an extensive evaluation of these methods on a collection of more than 12,000 nets from diverse sources, including nets whose marking graph is too large for being explored exhaustively.

24 pages

PDF

PostScript

Slides of P. Bouvier's video lecture at the Petri Net 2020 conference

PDF