Skip to Main content Skip to Navigation
Conference papers

On the Combination of Polyhedral Abstraction and SMT-based Model Checking for Petri nets

Nicolas Amat 1 Bernard Berthomieu 1 Silvano Dal Zilio 1
1 LAAS-VERTICS - Équipe Verification de Systèmes Temporisés Critiques
LAAS - Laboratoire d'analyse et d'architecture des systèmes
Abstract : We define a method for taking advantage of net reductions in combination with a SMT-based model checker. We prove the correctness of this method using a new notion of equivalence between nets that we call polyhedral abstraction. Our approach has been implemented in a tool, named SMPT, that provides two main procedures: Bounded Model Checking (BMC) and Property Directed Reachability (PDR). Each procedure has been adapted in order to use reductions and to work with arbitrary Petri nets. We tested SMPT on a large collection of queries used during the 2020 edition of the Model Checking Contest. Our experimental results show that our approach works well, even when we only have a moderate amount of reductions.
Complete list of metadata

https://hal.laas.fr/hal-03202111
Contributor : Silvano Dal Zilio <>
Submitted on : Monday, April 19, 2021 - 3:21:40 PM
Last modification on : Tuesday, May 4, 2021 - 3:41:44 PM

Files

paper.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-03202111, version 1

Citation

Nicolas Amat, Bernard Berthomieu, Silvano Dal Zilio. On the Combination of Polyhedral Abstraction and SMT-based Model Checking for Petri nets. 42rd International Conference on Application and Theory of Petri Nets and Concurrency (Petri Nets 2021), Jun 2021, Paris (virtual), France. ⟨hal-03202111⟩

Share

Metrics

Record views

35

Files downloads

17