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?

  • 4
    $\begingroup$ 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. $\endgroup$ Feb 10, 2017 at 9:44
  • $\begingroup$ 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. $\endgroup$ Apr 25, 2019 at 13:02

1 Answer 1


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.

  • $\begingroup$ 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. $\endgroup$ Feb 10, 2017 at 9:49

Not the answer you're looking for? Browse other questions tagged or ask your own question.