↓Skip to main content

On the Combination of Polyhedral Abstraction and SMT-Based Model Checking for Petri Nets

Verification Tools SMPT Reductions Petri
Table of Contents

Nicolas Amat, Silvano Dal Zilio, Bernard Berthomieu
In ICATPN 2021 — 42nd International Conference on Application and Theory of Petri Nets and Concurrency, jun 2021.

conference paper

 PDF  DOI〈10.1007/978-3-030-76983-3_9〉  HAL-03202111

Note
#

This paper won best teaser video award.

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.

References
#

  • An extended version of this paper appears in Fundamenta Informaticae, 2022, 187 (2-4).  Link

Citation
#


@InProceedings{DalzilioS:petri2021smpt,
   author    = {Amat, Nicolas and {Dal Zilio}, Silvano and Berthomieu, Bernard},
   title     = {{On the Combination of Polyhedral Abstraction and SMT-Based Model Checking for Petri Nets}},
   booktitle = {ICATPN 2021 -- 42nd International Conference on Application and Theory of Petri Nets and Concurrency},
   series    = {Lecture Notes in Computer Science},
   volume    = {12734},
   publisher = {Springer-Verlag},
   doi = {10.1007/978-3-030-76983-3_9},
   pages     = {164--185},
   month     = jun, 
   year      = 2021
}