Detalle: |
|
We propose an extension of discrete time stochastic Petri box calculus (dtsPBC) presented by I.V. Tarasyuk with immediate multiactions, called dtsiPBC. dtsiPBC is a discrete time analogue of stochastic Petri box calculus (sPBC) with immediate multiactions proposed by H. Maci`a, V. Valero and others within a continuous time domain. The step operational semantics is constructed via labeled probabilistic transition systems. The denotational semantics is defined on the basis of a subclass of labeled discrete time stochastic Petri nets with immediate transitions. A consistency of both semantics is demonstrated. In order to evaluate performance, the corresponding semi-Markov chains are analyzed. We define step stochastic bisimulation equivalence of expressions and explain how it can be used to reduce their transition systems and underlying semi-Markov chains, as well as to compare the stationary behaviour. We prove that the introduced equivalence guarantees a coincidence of performance characteristics and can be used for performance analysis simplification. In a case study, a method of modeling, performance evaluation and behaviour preserving reduction of concurrent systems is outlined and applied to the shared memory system.
|