Un mod\`ele bool\'een pour l'\'enum\'eration des siphons et des pi\`eges minimaux dans les r\'eseaux de Petri

TL;DR

This paper introduces two efficient boolean-based methods for enumerating minimal siphons and traps in Petri-nets, which are crucial for analyzing the persistence of molecular species in biochemical networks.

Contribution

It presents novel SAT and CLP(B) based algorithms for minimal siphons and traps enumeration, outperforming existing dedicated algorithms in speed.

Findings

SAT and CLP(B) methods are faster than traditional algorithms

The methods perform well on biological Petri-net models

Proposed hard instances challenge minimal siphons enumeration

Abstract

Petri-nets are a simple formalism for modeling concurrent computation. Recently, they have emerged as a powerful tool for the modeling and analysis of biochemical reaction networks, bridging the gap between purely qualitative and quantitative models. These networks can be large and complex, which makes their study difficult and computationally challenging. In this paper, we focus on two structural properties of Petri-nets, siphons and traps, that bring us information about the persistence of some molecular species. We present two methods for enumerating all minimal siphons and traps of a Petri-net by iterating the resolution of a boolean model interpreted as either a SAT or a CLP(B) program. We compare the performance of these methods with a state-of-the-art dedicated algorithm of the Petri-net community. We show that the SAT and CLP(B) programs are both faster. We analyze why these programs perform so well on the models of the repository of biological models biomodels.net, and propose some hard instances for the problem of minimal siphons enumeration.