Timed petri nets and temporal linear logic

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 t~-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.