English

SMPT: A Testbed for Reachability Methods in Generalized Petri Nets

Logic in Computer Science 2023-03-01 v1

Abstract

SMPT (for Satisfiability Modulo Petri Net) is a model checker for reachability problems in Petri nets. It started as a portfolio of methods to experiment with symbolic model checking, and was designed to be easily extended. Some distinctive features are its ability to benefit from structural reductions and to generate verdict certificates. Our tool is quite mature and performed well compared to other state-of-the-art tools in the Model Checking Contest.

Keywords

Cite

@article{arxiv.2302.14741,
  title  = {SMPT: A Testbed for Reachability Methods in Generalized Petri Nets},
  author = {Nicolas Amat and Silvano Dal Zilio},
  journal= {arXiv preprint arXiv:2302.14741},
  year   = {2023}
}

Comments

FM 2023 - 25th International Symposium on Formal Methods,, Mar 2023, L{\"u}beck, Germany

R2 v1 2026-06-28T08:52:06.257Z