Geração do Grafo de Atingibilidade

Prévia do material em texto

27 
Generation of the reachability graph 
By properly identifying the frontier nodes, the generation 
of the reachability graph involves a finite number of 
steps, even if the PN is unbounded. 
 
Three type of frontier nodes: 
Ø  terminal (dead) nodes: no transition is enabled; 
Ø  duplicate nodes: already generated; 
Ø  infinitely reproducible nodes.