Reachability graph

Reachability graph --- граф достижимости, граф разметок.

The reachability graph of a Petri net [math]\displaystyle{ N }[/math] is a (not necessary finite) directed graph whose nodes are labeled by markings reacheable for [math]\displaystyle{ N }[/math]. The arcs of the reachability graph are labeled by the transitions of [math]\displaystyle{ N }[/math] in such a way that there is an arc labeled by [math]\displaystyle{ t }[/math] from a node labeled by [math]\displaystyle{ m_1 }[/math] to a node labeled by [math]\displaystyle{ m_2 }[/math] iff the firing of [math]\displaystyle{ t }[/math] changes the marking [math]\displaystyle{ m_1 }[/math] to [math]\displaystyle{ m_2 }[/math].