Marking and Covering Graphs
The marking graph G of a system net N has already been introduced in Section 2.8. Its nodes are the reachable states, its edges the reachable steps of N. We will specify a series of properties of N that are mirrored in G.
However, G is generally infinitely large. We therefore construct the finite covering graph H, which approximates G. A series of necessary or sufficient conditions for some properties of N can be specified by means of H.
KeywordsReachable State Covering Graph Marking Graph Temporal Logic Formula Reachable Marking
Unable to display preview. Download preview PDF.