Linear time algorithms for liveness and boundedness in conflict-free Petri nets

Petri nets have been widely used to design and modeling concurrent systems, as well as certain kinds of time-dependent systems. This is due not only to their neat graphical representation but also to the fact that a great quantity of theoretical studies have been done on their mathematical properties. In this paper, in order to capture some interesting structural properties of conflict-free Petri nets we consider directed hypergraph. This representation allows us to obtain very efficient algorithms and data structures to handle conflict-free Petri nets. More precisely, we propose linear time Mgorithms for determining potentially firable and live transitions and boundedness of the net. Moreover, we mantain the set of potentially firable transitions on-line, that is, while the net is modified: an important feature when we speak about interactive design of a system. In other words, our algorithms and data structures allow us to decide if a transition is potentially firable while the net is been built, with no additional cost.