II.2.3. Behavioral Properties

For untimed PN models, the behavioral properties (e.g. boundedness, liveness, reversibility, etc.) may be studied based on the coverability tree of the net. Relying on the topology and the initial marking of the net, the PN Toolbox can automatically construct this tree and display it in either text or graphic mode. The coverability tree is built with or without the ω-convention (fig. II.10). The ω-convention means the usage of a generic symbol (herein denoted by "ω”) for referring to unbounded markings. Since the boundedness of a net cannot be a priori known, it is recommended to start the construction of the coverability tree by answering Yes to the question Do you want to use the "ω - convention”?.

Fig II.10. The Coverability Tree dialogue window.