Academics working with timed Petri nets should look at this mathematical research paper. It shows how nets “implement” temporal (TRIO) logics. The theorems of the implemented logic are properties that the net satisfies. The paper defines refinement between nets. Refinement preserves the theorems of the implemented logics. Therefore, these properties do not need proof. The paper presents simple, intuitive, and correct refinements. Using these should simplify the proofs of some properties of real-time systems.