Discrete time phased Petri box calculus dtphPBC

We propose discrete time phased Petri box calculus (dtphPBC), an extension with phase type distributed multiaction delays of discrete time stochastic and deterministic Petri box calculus (dtsdPBC), previously presented by I.V. Tarasyuk. In dtphPBC, transition probability matrices (TPMs) of finite absorbing discrete time Markov chains (DTMCs) with a single absorbing state specify discrete phase type (DPH) distributed delays (including zero delay) of the phased multiactions that generalize stochastic and deterministic multiactions 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. The transition systems incorporate the absorbing DTMCs of the DPH delays of the executed phased multiactions via the structural operational semantics (SOS) rules. The SOS rules define a labeling with the empty set on the transitions among transient states of the absorbing DTMC and on the self-loop in the absorbing state of it. The transitions going from the transient states (positive phases) to the absorbing state (zero phase) are labeled with the executions, being the positive phases-superscribed timed multiactions whose (positive) delays are defined by the absorbing DTMC. A series of examples demonstrates how to construct the transition systems of the dynamic expressions, combined from timed and immediate multiactions with different operations of the calculus.