Skip to Main content Skip to Navigation
Conference papers

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

Pierre Bouvier 1 Hubert Garavel 1 Hernan Ponce de León 2
1 CONVECS - Construction of verified concurrent systems
Inria Grenoble - Rhône-Alpes, LIG - Laboratoire d'Informatique de Grenoble [2007-2015]
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 reformu-late 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.
Document type :
Conference papers
Complete list of metadatas

Cited literature [28 references]  Display  Hide  Download

https://hal.inria.fr/hal-02875957
Contributor : Hubert Garavel <>
Submitted on : Friday, June 19, 2020 - 9:47:30 PM
Last modification on : Thursday, July 9, 2020 - 9:44:53 AM

File

Bouvier-Garavel-PonceDeLeon-20...
Files produced by the author(s)

Identifiers

  • HAL Id : hal-02875957, version 1

Collections

Citation

Pierre Bouvier, Hubert Garavel, Hernan Ponce de León. Automatic Decomposition of Petri Nets into Automata Networks - A Synthetic Account. 41st International Conference on Application and Theory of Petri Nets and Concurrency (PETRI NETS 2020), Jun 2020, Paris, France. ⟨hal-02875957⟩

Share

Metrics

Record views

51

Files downloads

70