  Brute-force model-checking consists in exhaustive exploration of the
state-space of a Petri net, and meets the dreaded state-space explosion
problem.
  In contrast, this paper shows how to solve model-checking problems using a
combination of techniques that stay in complexity proportional to the size of
the net structure rather than to the state-space size.
  We combine an SMT based over-approximation to prove that some behaviors are
unfeasible, an under-approximation using memory-less sampling of runs to find
witness traces or counter-examples, and a set of structural reduction rules
that can simplify both the system and the property.
  This approach was able to win by a clear margin the model-checking contest
2020 for reachability queries as well as deadlock detection, thus demonstrating
the practical effectiveness and general applicability of the system of rules
presented in this paper.
