Reachability and Coverability

The reachable markings of a Petri net can be represented as the vertices of a directed graph whose edges are labelled by transitions and whose paths correspond to firing sequences. This graph can be infinite for unbounded nets. Coverability trees and graphs are also defined for every net. They can be understood as finite approximations of the potentially infinite reachability graph. These objects are distinguished in terms of the Petri net properties, such as boundedness and liveness, that can be tested on them.