Polyhedral Reductions for Petri nets

Nicolas Amat (1) , Bernard Berthomieu (1) , Silvano Dal Zilio (1) , Didier Le Botlan (1)

1 LAAS-VERTICS - Équipe Verification de Systèmes Temporisés Critiques

Polyhedral equivalence defines a linear dependence relation (E) between the reachable markings of two nets; where E is a Presburger formula, or a system of linear Diophantine equations. This equivalence, denoted (N1, m1) ≡E (N2, m2), preserves enough information in E so that we can rebuild the state space of N1 knowing only the one of N2

Mots clés: Petri net; Model-checking

Domaines: Logique en informatique [cs.LO]

Nicolas Amat, Bernard Berthomieu, Silvano Dal Zilio, Didier Le Botlan. Polyhedral Reductions for Petri nets. Modélisation des Systèmes Réactifs (MSR'23), Nov 2023, Toulouse, France. , 2023. ⟨hal-04355257⟩