Accelerating the Computation of Dead and Concurrent Places using Reductions
Logic in Computer Science
2021-06-25 v1
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.
Cite
@article{arxiv.2106.12813,
title = {Accelerating the Computation of Dead and Concurrent Places using Reductions},
author = {Nicolas Amat and Silvano Dal Zilio and Didier Le Botlan},
journal= {arXiv preprint arXiv:2106.12813},
year = {2021}
}