Discrete Time Stochastic Petri Box Calculus with Immediate Multiactions dtsiPBC

We propose discrete time stochastic Petri box calculus extended with immediate multiactions, called dt-siPBC. The step operational semantics is constructed via labeled probabilistic transition systems. The denotational semantics is defined via labeled discrete time stochastic Petri nets with immediate transitions (LDTSIPNs). A consistency of both semantics is demonstrated. In order to evaluate performance, the corresponding semi-Markov chains are analyzed. In a case study, performance of the shared memory system is evaluated.