A Compositional Model of Time Petri Nets

This paper presents two related algebras which can be used to specify and analyse concurrent systems with explicit timing information. The first algebra is based on process expressions, called t-expressions, and a system of SOS rules providing their operational semantics. The second algebra is based on a class of time Petri nets, called ct-boxes, and their transition firing rule. The two algebras are related through a mapping which, for a t-expression, returns a corresponding ct-box with behaviourally equivalent transition system. The resulting model, called the Time Petri Box Calculus (tPBC), extends the existing approach of the Petri Box Calculus (PBC).