Automatic Decomposition of Petri Nets into Automata Networks – A Synthetic Account
- 30 June 2020
- book chapter
- conference paper
- Published by Springer Science and Business Media LLC
- Vol. 12152, 3-23
- https://doi.org/10.1007/978-3-030-51831-8_1
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.Keywords
This publication has 21 references indexed in Scilit:
- Nested-unit Petri netsJournal of Logical and Algebraic Methods in Programming, 2019
- Gradient-Based Variable Ordering of Decision Diagrams for Systems with Structural UnitsLecture Notes in Computer Science, 2017
- A concurrency-preserving translation from time Petri nets to networks of timed automataFormal Methods in System Design, 2012
- Petri Net DistributabilityLecture Notes in Computer Science, 2012
- On Distributability of Petri NetsLecture Notes in Computer Science, 2012
- Translating Safe Petri Nets to Statecharts in a Structure-Preserving WayLecture Notes in Computer Science, 2009
- State space reduction for process algebra specificationsTheoretical Computer Science, 2005
- Distributing Finite Automata Through Petri Net SynthesisFormal Aspects of Computing, 2002
- Free Choice Petri NetsPublished by Cambridge University Press (CUP) ,1995
- A survey of basic net models and modular net classesPublished by Springer Science and Business Media LLC ,1992