# SMPT: A Testbed for Reachability Methods in Generalized Petri Nets

## TL;DR

SMPT is a versatile and extendable model checker for Petri net reachability problems that leverages structural reductions and generates certificates, showing competitive performance in the Model Checking Contest.

## Contribution

It introduces SMPT, a new, extendable tool for Petri net reachability analysis that incorporates structural reductions and certificate generation.

## Key findings

- SMPT performs well against state-of-the-art tools.
- It benefits from structural reductions for efficiency.
- The tool is mature and versatile.

## 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.