Discrete time phased Petri box calculus dtphPBC

We propose discrete time phased Petri box calculus (dtphPBC), an extension with phase type delays of discrete time stochastic and deterministic Petri box calculus (dtsdPBC). In dtphPBC, transition probability matrices (TPMs) of finite absorbing discrete time Markov chains with a single absorbing state specify discrete phase type (DPH) delays (including zero delay) of the phased multiactions that generalize stochastic and deterministic ones from dtsdPBC. The positively phased (timed) multiactions have positive DPH delays represented by the non-empty TPM matrices over transient states (transient TPMs). The zero phased (immediate) multiactions have zero DPH delay represented by the empty transient TPM. The step operational semantics of dtphPBC is constructed via labeled probabilistic transition systems.