Discrete time stochastic and deterministic Petri box calculus dtsdPBC

We propose dtsdPBC, an extension with deterministically timed multiactions of discrete time stochastic and immediate Petri box calculus (dtsiPBC), previously presented by I.V. Tarasyuk, H. Macià and V. Valero. dtsdPBC enhances the expressiveness of dtsiPBC and extends the application area of the associated specification and analysis techniques. In dtsdPBC, non-negative integers are used to specify fixed (including zero) time delays of deterministic multiactions. The step operational semantics of the calculus is constructed via labeled probabilistic transition systems. The Petri net denotational semantics of the calculus is defined on the basis of dtsd-boxes, a subclass of novel labeled discrete time stochastic Petri nets with deterministic transitions (LDTSDPNs).
We also define step stochastic bisimulation equivalence of the algebraic expressions, used to compare the qualitative and quantitative behaviour of the specified processes. The consistency of the operational and denotational semantics of dtsdPBC up to that bisimulation equivalence is established. The interrelations of the mentioned equivalence with other behavioural notions of the calculus are investigated. A series of examples that construct the transition systems and dtsd-boxes for the expressions with different types of multiactions and operations demonstrates both the specification capabilities and semantic features of the new calculus.