Accelerating the computation of dead and concurrent places using reductions

DOI10.1007/978-3-030-84629-9_3MaRDI QIDQ832013zbMATH OpenOpenAlexFDO

Authors Nicolas Amat, Silvano Dal Zilio, Didier Le Botlan

Publication date 24 March 2022

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

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)

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.

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

Cites work

• scientific article; zbMATH DE number 4033100 (Why is no real title available?)
• scientific article; zbMATH DE number 1302046 (Why is no real title available?)
• Algebraic Methodology and Software Technology
• Automatic decomposition of Petri nets into automata networks -- a synthetic account
• Efficient algorithms for three reachability problems in safe Petri nets
• Nested-unit Petri nets
• Nets, sequential components and concurrency relations
• On the combination of polyhedral abstraction and SMT-based model checking for Petri nets
• Petri Net Reductions for Counting Markings
• Reduction
• Structural reductions revisited
• Stubborn versus structural reductions for Petri nets
• The tool TINA – Construction of abstract state spaces for petri nets and time petri nets

Cited in

(2)

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

Describes a project that uses

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)