The Petri net twist in explicit model checking

The invention of Petri nets was based on a critical analysis of then dominating automata models of systems. Explicit model checking explores the reachable states of a Petri net one by one. Essentially, it transforms a Petri net back to a transition system, that is, an automata-like model. At first glance, this transformation appears to give up on all the specifics of Petri nets. Surveying the most dominant techniques of explicit state space verification, we will, however, work out that even in explicit model checking, the defining features of Petri nets are beneficial and lead to more efficient exploration routines. The findings in this paper are based on practical experience with a Petri net-based explicit model checking tool.