Stochastic bisimulation and performance evaluation in discrete time stochastic and deterministic Petri box calculus dtsdPBC
Igor V. Tarasyuk · HAL (Le Centre pour la Communication Scientifique Directe) · 2020
We propose dtsdPBC, an extension with deterministically timed multiactions of discrete time stochasticand immediate Petri box calculus (dtsiPBC), previously presented by I.V. Tarasyuk, H. Maci`a and V. Valero.In dtsdPBC, non-negative integers specify deterministic multiactions with fixed (including zero) time delays.The step operational semantics is constructed via labeled probabilistic transition systems. The Petri netdenotational semantics is defined via dtsd-boxes, a subclass of labeled discrete time stochastic Petri netswith deterministic transitions. We also define step stochastic bisimulation equivalence of the process expres-sions, which is used to compare the qualitative and quantitative behaviour of the specified processes. Theconsistency of the operational and denotational semantics of dtsdPBC up to that equivalence is established.In order to evaluate performance in dtsdPBC, the underlying semi-Markov chains (SMCs) and (reduced)discrete time Markov chains (DTMCs and RDTMCs) of the process expressions are analyzed. We explainhow step stochastic bisimulation equivalence of the expressions can be used for quotienting their transitionsystems and Markov chains, as well as to compare the stationary behaviour and residence time properties.We prove that the equivalence guarantees coincidence of the functional and performance characteristics andtherefore can be used to simplify performance analysis of the algebraic processes. In a case study, a methodof modeling, performance evaluation and behaviour reduction for concurrent systems with discrete fixed andstochastic delays is applied to the generalized shared memory system with maintenance. We also determinethe main advantages of dtsdPBC by comparing it with other well-known or similar SPAs.