Petri nets are widely used for modeling and analysis of concurrent processing systems. In l985, Suzuki introduced a new class of Petri nets, called the temporal Petri nets, in which certain restrictions on the firings of transitions are represented by formulas containing temporal operators and showed that they are quite useful in specifying and proving fundamental properties of concurrent systems such as eventuality and fairness. The goal of the research is to further investigate the potential of temporal Petri nets and develop new analysis and synthesis methods of concurrent systems based on them.
