Accelerating the computation of dead and concurrent places using reductions

DOI10.1007/978-3-030-84629-9_3zbMATH Open1490.68137arXiv2106.12813OpenAlexW3176282500MaRDI QIDQ832013FDOQ832013

Authors: Nicolas Amat, Silvano Dal Zilio, Didier Le Botlan 

Publication date: 24 March 2022

Abstract: We propose a new method for accelerating the computation of a concurrency relation, that is all pairs of places in a Petri net that can be marked together. Our approach relies on a state space abstraction, that involves a mix between structural reductions and linear algebra, and a new data-structure that is specifically designed for our task. Our algorithms are implemented in a tool, called Kong, that we test on a large collection of models used during the 2020 edition of the Model Checking Contest. Our experiments show that the approach works well, even when a moderate amount of reductions applies.

Full work available at URL: https://arxiv.org/abs/2106.12813

Recommendations

• Petri Net Reductions for Counting Markings
• Efficient algorithms for three reachability problems in safe Petri nets
• Faster simulation of (coloured) Petri nets using parallel computing
• Computing Petri net languages by reductions
• scientific article; zbMATH DE number 1696467

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Cites Work

• Nested-unit Petri nets
• Algebraic Methodology and Software Technology
• Title not available (Why is that?)
• The tool TINA – Construction of abstract state spaces for petri nets and time petri nets
• Reduction
• Title not available (Why is that?)
• Nets, sequential components and concurrency relations
• Stubborn versus structural reductions for Petri nets
• On the combination of polyhedral abstraction and SMT-based model checking for Petri nets
• Efficient algorithms for three reachability problems in safe Petri nets
• Automatic Decomposition of Petri Nets into Automata Networks – A Synthetic Account
• Structural Reductions Revisited
• Petri Net Reductions for Counting Markings

Cited In (2)

• On the complexity of proving polyhedral reductions
• Automated polyhedral abstraction proving

Uses Software

• PNML
• TINA
• NUPN_INFO
• CAESAR
• caesar.bdd

This page was built for publication: Accelerating the computation of dead and concurrent places using reductions

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q832013)