# Petri Net Verifier [closed]

Imagine I can specify a certain process as a Petri Net. Is there any good software, open source or not, that can verify my process against some conditions I declare (or code) in some language?

In case not, is there an open source software that does at least simulations?

## closed as off-topic by Evil, David Richerby, Yuval Filmus, Juho, Rick DeckerFeb 20 '17 at 14:07

• This question does not appear to be about computer science within the scope defined in the help center.
If this question can be reworded to fit the rules in the help center, please edit the question.

• I'm voting to close this question as off-topic because software recommendations are off-topic, here. You could ask at Software Recommendations. You could also try asking in Computer Science Chat, since what you're looking for definitely is related to computer science. – David Richerby Feb 10 '17 at 9:44
• The problem with this advice is that few specialists are likely to be on Software Recommendations. A well-known verification tool for Petri nets (within the community) is LoLA. – reinierpost Apr 25 at 13:02

It's not really a field I know much about, but I doubt it.

Model-checking problems get very hard (sometimes very undecidable) very fast. Whether what you ask is faisable at all depends on the kind of statements you are interested in checking and on what restrictions on the Petri nets structure you are willing to impose.

On general nets, all interesting questions (e.g. marking reachability) are $\text{EXPSPACE}$-hard. General model-checking is undecidable even for very weak branching-time temporal logics; several interesting fragments of linear-time logics are decidable but at least as hard as the reachability problem, i.e. $\text{EXPSPACE}$-hard.

Software recommendations are off-topic here, but I'm sure plenty of simulators are available online.

• I'm sure what you say is true but the theory isn't necessarily a good predictor of real-world behaviour. A trivial example is that SAT is NP-complete but SAT solvers are a completely practical way of solving instances with millions of variables. Many model-checking problems are way harder than even EXPSPACE but can still be solved effectively in practice because the hardness results require deep alternations of quantifiers, but the formulae people want to check tend to have only a few alternations. – David Richerby Feb 10 '17 at 9:49