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 speedups 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 "highdimensionality" 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: 
[AmatDalZilioLeBotlan21]
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. 4562. Springer Verlag, July 2021.
Available online at: https://arxiv.org/pdf/2106.12813 or from the CADP Web site in PDF or PostScript 
Contact:  Silvano Dal Zilio LAASCNRS, Vertics team 7, avenue du Colonel Roche F31031 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 