Symbolic analysis of timed Petri nets

Zuberek, W.M.

in: Theory and Engineering of Complex Systems and Dependability (Advances in Intelligent Systems and Computing 365), Proc. of the 10-th Int. Conf. on Dependability and Complex Systems (DepCoS-RELCOMEX'15), June 29 \ndash; July 3, 2015, Brunow, Poland, ed. W. Zamojski, J. Mazurkiewicz, J. Sugier, T. Walkowiak, J. Kacprzyk, Springer-Verlag 2015, pp.595-604 (DOI 10.1007/978-3-319-19216-1_57).


In timed Petri nets temporal properties are associated with transitions as transition firing times (or occurrence times). Specific properties of timed nets, such as boundedness or absence of deadlocks, can depend upon temporal properties and sometimes even a small change of these properties has a significant effect on the net's behavior (e.g., a bounded net becomes unbounded or vice versa). The objective of symbolic analysis of timed nets is to provide information about the net's behavior which is independent of specific temporal properties, i.e., which describes preperties of the whole class of timed nets with the same structure.


timed Petri nets, symbolic analysis, boundedness, absence of deadlocks, producer-consumer model


Available in pdf.