Accelerating the Computation of Dead and Concurrent Places using Reductions

Organisation:	LAAS/CNRS, Toulouse (FRANCE)
Functionality:	Analysis of Concurrent Systems
Tools used:	Kong CADP (Construction and Analysis of Distributed Processes)
Domain:	Concurrent Systems
Period:	2021
Description:	The problem of computing the concurrency relation of a Petri net amounts to determine all pairs of places that can be marked together in some reachable states. This has practical applications, e.g., for decomposing a Petri net into the product of concurrent processes. It also provides an example of safety property extending the notion of dead places. The idea is to compute reductions from an initial Petri net N1 (subject to analysis) to a residual net N2 (hopefully simpler than N1) using a system E of linear equations. The system E should contain enough information so as to enable the reconstruction of the reachable markings of N1 knowing only those of N2. This work shows how to reconstruct the concurrency relation of N1 from the one of N2 by means of a new efficient "inverse transform" depending only on E and not involving the computation of reachable markings. The main goal is not to compute the concurrency relation of N2, but to accelerate the computation of the concurrency relation of N1. The approach proposed introduces token flow graphs (TFGs) and exploits them to define an algorithm implementing the inverse transform. The approach has been implemented in the Kong tool, and applied on a set of 588 safe Petri nets available from the MCC'2020 contest. The concurrency relation of the reduced Petri nets was computed using the CAESAR.BDD tool of CADP. Even if the amount of reduction was moderate (removal of around 25% of the places), the results were computed much faster with reductions than without (often with speed-ups greater than x100).
Conclusions:	Computing the concurrent relation of a Petri net is a difficult problem, especially when it is not possible to compute the complete state space of the net. The proposed method moves this problem from an initial "high-dimensionality" domain (the set of places in the net) into a smaller one (the set of places in the residual net). The experiments confirm that the concurrency relation is much easier to compute after reductions.
Publications:	[Amat-DalZilio-LeBotlan-21] Nicolas Amat, Silvano Dal Zilio, and Didier Le Botlan. "Accelerating the Computation of Dead and Concurrent Places Using Reductions". Proc. of the 27th International Symposium on Model Checking Software (SPIN'2021), Lecture Notes in Computer Science vol. 12864, pp. 45-62. Springer Verlag, July 2021. Available on-line at: https://arxiv.org/pdf/2106.12813 or from the CADP Web site in PDF or PostScript [Amat-Bouvier-Garavel-23] Nicolas Amat, Pierre Bouvier, and Hubert Garavel. "A Toolchain to Compute Concurrent Places of Petri Nets". Transactions on Petri Nets and Other Models of Concurrency XVII, Lecture Notes in Computer Science 14150:1-26. Springer Verlag, 2023. Available on-line at: http://hal.inria.fr/hal-04392784/en
Contact:	Silvano Dal Zilio LAAS-CNRS, Vertics team 7, avenue du Colonel Roche F-31031 Toulouse FRANCE Email: dalzilio@laas.fr Tel: +33 (0)5 61 33 78 20
Further remarks:	This tool, amongst others, is described on the CADP Web site: http://cadp.inria.fr/software

Back to the CADP research tools page