In: Azéma, P.; Balbo, G.: Lecture Notes in Computer Science, Vol. 1248: 18th International Conference on Application and Theory of Petri Nets, Toulouse, France, June 1997, pages 156-174. Berlin, Germany: Springer-Verlag, June 1997.
Abstract: It is well known that Petri nets constitute the algebraic structure of quantales, which can be models of linear logic. As a timed extension to quantales, Timed R-monoids are defined, which are constructed from timed Petri nets. Next, temporal linear logic is introduced, which has timed Petri nets as its models, i.e., whose formulas can be interpreted as sets of timed markings of a timed Petri net. Soundness of the logic with respect to timed Petri net interpretation is shown. Finally, examples show how to express properties of timed Petri nets by temporal linear logic.
Keywords: timed Petri nets; quantales; temporal linear logic.