Abstract: The Petri net formalism has been used to model many types of
   systems, in particular, concurrent, distributed and non-deterministic.
   Important system properties, such as liveness and safety, can be
   studied based on the system's net model. A means of analysing its
   behaviour is by examining its net structure.
   
   In Petri net theory, safety or boundedness, in its usual sense, sets a
   bound on the maximum number of tokens that can be assembled in a
   place. In a type of standard Petri nets with simple tokens, the
   Elementary net (EN) system, to be safe is to avoid a phenomenon called
   a contact situation, in which pre- and postconditions of an event are
   satisfied at the same time.
   
   To model real-time systems, we define a time extension of EN system
   called Time EN (TEN) system. By attaching time intervals to
   transitions, one is able to control the flow of tokens, and ensure
   that a system can still be safe even in a contact situation. With this
   notion of time safety and a new definition of free-choice structure,
   the existing liveness theorems for standard Petri nets are modified,
   so that they can be applied to TEN systems.